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