{-# 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))