{-# OPTIONS --without-K #-}

module function.extensionality.nondep where

open import sum
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core using (id; _∘_)
open import function.isomorphism.core
open import function.isomorphism.coherent
open import hott.hlevel.core
open import hott.weak-equivalence.core
open import hott.univalence
open import function.extensionality.core

private
  -- we begin with some preliminaries on path spaces
  -- let's fix a set X
  module Paths {i} (X : Set i) where
    -- Δ is the path space of X, i.e.
    -- the type of triples (x, x', p)
    -- where p : x ≡ x'
    Δ : Set _
    Δ = Σ X λ x₁
       Σ X λ x₂
       x₁  x₂

    -- there are obvious projections π₁ π₂ : Δ → X
    π₁ : Δ  X
    π₁ = proj₁

    π₂ : Δ  X
    π₂ = proj₁  proj₂

    -- X can be embedded into Δ via the "diagonal" function δ
    δ : X  Δ
    δ x = (x , x , refl)

    -- δ is a weak-equivalence between X and Δ
    δ-we : weak-equiv δ
    δ-we (x , .x , refl) = (x , refl)
                         ,  { (x' , p)  lem _ x' p })
      where
        K : (d : Δ)  δ (π₁ d)  d
        K (x , .x , refl) = refl

        lem : (d : Δ)(x : X)(p : δ x  d)
             _≡_ {A = δ ⁻¹ d} (π₁ d , K d) (x , p)
        lem .(x , x , refl) x refl = refl

    Δ-equiv : X  Δ
    Δ-equiv = δ , δ-we

  -- now we use univalence to show that a weak equivalence between X and
  -- Y lifts to a weak equivalence between the exponentials (A → X) and
  -- (A → Y) for any type A
  module Lift {i} j (A : Set i) where
    -- lift a function to the exponentials
    lift : {X Y : Set j}
          (X  Y)  (A  X)  (A  Y)
    lift f g a = f (g a)

    -- lift an equality of types to an equality of exponentials
    lift≡ : {X Y : Set j}
             X  Y  (A  X)  (A  Y)
    lift≡ refl = refl

    -- coerce commutes with lifting
    lift-coherence : {X Y : Set j}(p : X  Y)
                    coerce (lift≡ p)
                    lift (coerce p)
    lift-coherence refl = refl

    -- Using univalence, lift a weak equivalence to the exponentials.
    -- Note that we really need univalence here, as it's not possible to
    -- prove that lift gives an isomorphism, unless we already have
    -- extensionality.
    lift≈ : {X Y : Set j}
           X  Y
           (A  X)  (A  Y)
    lift≈ = ≡⇒≈  lift≡  ≈⇒≡

    -- lift≈ acts like lift
    lift≈-coherence : {X Y : Set j}
                     (f : X  Y)
                     apply≈ (lift≈ f)  lift (apply≈ f)
    lift≈-coherence f = begin
        proj₁ (lift≈ f)
      ≡⟨ refl 
        coerce (lift≡ (≈⇒≡ f))
      ≡⟨ lift-coherence (≈⇒≡ f) 
        lift (coerce (≈⇒≡ f))
      ≡⟨ cong lift (uni-coherence f) 
        lift (proj₁ f)
      
      where open ≡-Reasoning

    -- lift≈ respects inverses
    lift≈-inverse : {X Y : Set j}
                   (f : X  Y)
                   (g : Y  X)
                   g  apply≈ f  id
                   (u : A  Y)
                   lift g u  invert≈ (lift≈ f) u
    lift≈-inverse f g p u = begin
        lift g u
      ≡⟨ cong (lift g) (sym (iso₂ u)) 
        lift g (to (from u))
      ≡⟨ cong  z  lift g (z (from u)))
              (lift≈-coherence f) 
        lift g (lift (apply≈ f) (from u))
      ≡⟨ refl 
        lift (g  apply≈ f) (from u)
      ≡⟨ cong  z  lift z (from u)) p 
        from u
      ≡⟨ refl 
        invert≈ (lift≈ f) u
      
      where
        open ≡-Reasoning
        open _≅_ (≈⇒≅ (lift≈ f))

-- Now, to prove extensionality, we take a pair of extensionally equal
-- functions, and we want to prove that they are propositionally equal
abstract
  ext₀ :  {i j}  Extensionality i j
  ext₀ {i}{j} {X} {Y} {f} {g} h = main
    where
      -- Let Y' be the path space of Y
      open Paths Y renaming (Δ to Y')
      open Lift j X

      -- Since Y and Y' are equivalent, we can lift the equivalence
      -- to the exponentials, and get an isomorphism.
      iso' : (X  Y)  (X  Y')
      iso' = ≈⇒≅ (lift≈ Δ-equiv)

      -- We can now show that composing with δ is a left inverse to
      -- composing with π₁.
      -- Here we make use of the fact that the underlying function of
      -- the equivalence returned by lift≈ is just lift of the base
      -- function.
      lem : (k : X  Y')  δ  π₁  k  k
      lem k = begin
          δ  π₁  k
        ≡⟨ cong  t  t (π₁  k))
                 (sym (lift≈-coherence Δ-equiv)) 
          to (π₁  k)
        ≡⟨ cong to (lift≈-inverse Δ-equiv π₁ refl k) 
          to (from k)
        ≡⟨ iso₂ k 
          k
        
        where
          open ≡-Reasoning
          open _≅_ iso'

      -- Now we can finally show that f and g are equal.
      -- The idea of the proof is that
      --     δ ∘ f ≡ δ ∘ g
      -- since they are both equal to k below, hence they must be equal
      -- by injectivity of δ
      main : f  g
      main = begin
          f
        ≡⟨ refl 
          π₁  k
        ≡⟨ refl 
          π₂  δ  π₁  k
        ≡⟨ cong (_∘_ π₂) (lem k) 
          π₂  k
        ≡⟨ refl 
          g
        
        where
          open ≡-Reasoning
          open _≅_ iso' using (iso₂)

          k : X  Y'
          k x = (f x , (g x , h x))

abstract
  ext :  {i j}  Extensionality i j
  ext h = ext₀ h
         ext₀  _  refl) ⁻¹

  -- computation rule for extensionality
  ext-id :  {i j}{X : Set i}{Y : Set j}
          (f : X  Y)
          ext {f = f} {f}  _  refl)  refl
  ext-id f = left-inverse (ext₀  x  refl))