A proof that univalence implies function extensionality

1 files changed, 239 insertions, 0 deletions

diff --git a/Univalence-to-funext.agda b/Univalence-to-funext.agda
new file mode 100644
index 0000000..c2935b2
--- /dev/null
+++ b/Univalence-to-funext.agda
@@ -0,0 +1,239 @@
+{-# OPTIONS --without-K --rewriting #-}
+
+module Univalence-to-funext where
+
+open import lib.Base
+open import lib.Equivalence
+open import lib.Function
+open import lib.PathGroupoid
+open import lib.PathFunctor
+open import lib.NType
+
+--============================================================================--
+--                      Generic paths in Σ types
+
+module _ {i j} {A : Type i} {B : A → Type j} where
+  Σ-path-pair : (v w : Σ A B) → Type (lmax i j)
+  Σ-path-pair v w = Σ (fst v == fst w)
+                      (λ p → transport B p (snd v) == snd w)
+
+  pair→Σ= : {v w : Σ A B} → Σ-path-pair v w → v == w
+  pair→Σ= (idp , idp) = idp
+
+  Σ=→pair : {v w : Σ A B} → v == w → Σ-path-pair v w
+  Σ=→pair idp = (idp , idp)
+
+  Σ=→pair→Σ= : {v w : Σ A B} (p : v == w) → pair→Σ= (Σ=→pair p) == p
+  Σ=→pair→Σ= idp = idp
+
+  pair→Σ=→pair : {v w : Σ A B} (z : Σ-path-pair v w) →
+                 Σ=→pair (pair→Σ= z) == z
+  pair→Σ=→pair (idp , idp) = idp
+
+  Σ=≃pair : {v w : Σ A B} → (v == w) ≃ (Σ-path-pair v w)
+  Σ=≃pair = equiv Σ=→pair pair→Σ= pair→Σ=→pair Σ=→pair→Σ=
+
+               
+--============================================================================--
+--                           Univalence
+
+idtoeqv : ∀ {i} {A B : Type i} → (A == B) → (A ≃ B)
+idtoeqv {A = A} idp = ide A
+
+postulate
+  ua : ∀ {i} {A B : Type i} → (A ≃ B) → (A == B)
+  idtoeqv-ua-β : ∀ {i} {A B : Type i} (e : A ≃ B) → idtoeqv (ua e) == e
+
+eqv-post∘ : ∀ {i} {A B : Type i} {C : Type i} (p : A == B) → 
+            fst (idtoeqv (ap (λ T → (C → T)) p)) == _∘_ (fst (idtoeqv p))
+eqv-post∘ idp = idp
+
+--============================================================================--
+--                         Happly and lemmas
+
+module _ {i j} {A : Type i} {B : A → Type j} {f g : Π A B} where
+  idh : f ∼ f
+  idh a = idp
+
+  happly : f == g → f ∼ g
+  happly p a = ap (λ k → k a) p
+
+  tr-happly-lemma : (p : f == g) →
+                    transport (λ k → f ∼ k) p (idh) == happly p
+  tr-happly-lemma idp = idp
+
+  fib-happly-lemma : (h : f ∼ g) → ((f , idh) == (g , h)) ≃ hfiber happly h
+  fib-happly-lemma h = (equiv from to α β) ∘e Σ=≃pair
+    where
+      to : hfiber happly h → Σ-path-pair (f , idh) (g , h)
+      to (p , q) = (p , tr-happly-lemma p ∙ q)
+
+      from :  Σ-path-pair (f , idh) (g , h) → hfiber happly h
+      from (p , q) = (p , ! (tr-happly-lemma p) ∙ q)
+
+      β : (b : Σ-path-pair (f , idh) (g , h)) → to (from b) == b
+      β (p , q) = pair→Σ= (idp , ! (∙-assoc (tr-happly-lemma p)
+                                            (! (tr-happly-lemma p)) q) ∙
+                                 !-inv-r (tr-happly-lemma p) ∙2 idp)
+
+      α : (a : hfiber happly h) → from (to a) == a
+      α (p , q) = pair→Σ= (idp ,
+                           ! (∙-assoc (! (tr-happly-lemma p))
+                             (tr-happly-lemma p) q) ∙
+                           !-inv-l (tr-happly-lemma p) ∙2 idp)
+
+--============================================================================--
+--                     Equivalences and contractibility
+
+contr-retract : ∀ {i} {A B : Type i}
+                (r : A → B) (s : B → A) →
+                (r ∘ s ∼ (idf B)) →
+                is-contr A → is-contr B
+contr-retract r s h p = has-level-in
+                      ((r (fst c)) , λ y → ap r (snd c (s y)) ∙ h y)
+                      where c = has-level-apply p
+                      
+module _ {i j} {A : Type i} {B : Type j} where
+  is-contr-map : (f : A → B) → Type (lmax i j)
+  is-contr-map f = (y : B) → is-contr (hfiber f y)
+
+  tr-ap-lemma : (f : A → B) {a' a : A} {b : B}
+                (p : a' == a) (q : f a' == b) →
+                transport (λ x → f x == b) p q == ! (ap f p) ∙ q
+  tr-ap-lemma f idp idp = idp
+
+  nat-lemma : {k l : B → B} {a b : B} (p : a == b )(h : k ∼ l) →
+              ap k p ∙ h b == h a ∙ ap l p
+  nat-lemma {a = a} idp h = ! (∙-unit-r (h a))
+
+  contr-map-is-equiv : {f : A → B} → (is-contr-map f → is-equiv f)
+  contr-map-is-equiv {f = f} c = snd (equiv f g α β)
+    where
+      g : B → A
+      g b = fst (fst (has-level-apply (c b)))
+
+      α : f ∘ g ∼ (idf B)
+      α b = snd (fst (has-level-apply (c b)))
+
+      β : g ∘ f ∼ (idf A)
+      β a = fst (Σ=→pair (snd (has-level-apply (c (f a))) (a , idp)))
+
+      
+
+  equiv-is-contr-map : {f : A → B} → (is-equiv f → is-contr-map f)
+  equiv-is-contr-map {f = f} e b =
+                        has-level-in (hf , λ y → pair→Σ= (fc y , sc y))
+    where
+      g : B → A
+      g = is-equiv.g e
+
+      α : g ∘ f ∼ (idf A)
+      α = is-equiv.g-f e
+
+      β : f ∘ g ∼ (idf B)
+      β = is-equiv.f-g e
+      
+      hf : hfiber f b
+      hf = ((g b) , (β b))
+
+      fc : (y : hfiber f b) → (g b) == fst y
+      fc (a , p) = ap (g) (! p) ∙ α a
+
+      sc : (y : hfiber f b) →
+           transport (λ x → f x == b) (fc (fst y , snd y)) (β b) == snd y
+      sc (a , p) =
+        transport (λ x → f x == b) (fc (a , p)) (β b)
+          =⟨ tr-ap-lemma f (fc (a , p)) (β b) ⟩
+        ! (ap f  (fc (a , p))) ∙ (β b)
+          =⟨ ap ! (ap-∙ f (ap g (! p)) (α a)) ∙2 idp ⟩
+        ! (ap f (ap g (! p)) ∙ ap f (α a)) ∙ (β b)
+          =⟨ ap ! (idp ∙2 is-equiv.adj e a) ∙2 idp {a = β b}⟩
+        ! (ap f (ap g (! p)) ∙ (β (f a))) ∙ (β b)
+          =⟨ ap ! (∘-ap f g (! p) ∙2 idp) ∙2 idp ⟩
+        ! (ap (f ∘ g) (! p) ∙ (β (f a))) ∙ (β b)
+          =⟨ !-∙ (ap (f ∘ g) (! p)) (β (f a)) ∙2 idp ⟩
+        (! (β (f a)) ∙ ! (ap (λ x → f (g x)) (! p))) ∙ (β b)
+          =⟨ (idp ∙2 !-ap (f ∘ g) (! p)) ∙2 idp {a = β b}⟩
+        (! (β (f a)) ∙ (ap (f ∘ g) (! (! p)))) ∙ (β b)
+          =⟨ (idp ∙2 ap (ap (f ∘ g)) (!-! p)) ∙2 idp {a = β b} ⟩
+        (! (β (f a)) ∙ (ap (f ∘ g) p)) ∙ (β b)
+          =⟨ ∙-assoc (! (β (f a))) (ap (f ∘ g) p) (β b) ⟩
+        ! (β (f a)) ∙ (ap (f ∘ g) p ∙ (β b))
+          =⟨ idp {a = ! (β (f a))} ∙2 (nat-lemma p β ∙ (idp ∙2 ap-idf p)) ⟩
+        ! (β (f a)) ∙ (β (f a) ∙ p)
+          =⟨ ! (∙-assoc (! (β (f a))) (β (f a)) p) ⟩
+        (! (β (f a)) ∙ β (f a)) ∙ p
+          =⟨ !-inv-l (β (f a)) ∙2 idp ⟩
+        p
+          =∎
+
+      
+
+--============================================================================--
+--                        Univalence implies funext
+
+module _ {i} {A : Type i} {B : A → Type i} {f : Π A B} where
+  image : A → Type i
+  image a = Σ (B a) (λ b → f a == b)
+
+  graphType : Type i
+  graphType = Σ A image
+  
+  prA : graphType → A
+  prA = fst
+
+  prA-is-equiv : graphType ≃ A
+  prA-is-equiv = equiv prA (λ x → (x , f x , idp)) (λ b → idp) β
+    where
+      tr-post-concat : ∀ {i} {X : Type i} {x y z : X} {p : x == y}
+                 (q : z == x) → transport (_==_ z) p q == q ∙ p
+      tr-post-concat {p = idp} idp = idp
+
+      β : (a : graphType) → (fst a , f (fst a), idp) == a
+      β (a , b , p) = pair→Σ= (idp , (pair→Σ= (p , (tr-post-concat idp))))
+                
+  fibreOverId : Type i
+  fibreOverId = hfiber (_∘_ prA) (idf A)
+
+  fibreOverId-is-contr : is-contr fibreOverId
+  fibreOverId-is-contr = prA∘-is-equiv (idf A)
+       where
+        p : graphType == A
+        p = ua prA-is-equiv
+
+        pβ : fst (idtoeqv p) == prA
+        pβ = ap fst (idtoeqv-ua-β prA-is-equiv)
+        
+        prA∘-is-equiv : is-contr-map (λ g → prA ∘ g)
+        prA∘-is-equiv = transport is-contr-map
+                         (eqv-post∘ p ∙ ap (λ x → _∘_ x) pβ)
+                         (equiv-is-contr-map
+                           (snd (idtoeqv (ap (λ T → (A → T)) p))))
+
+  homotopyType : Type i
+  homotopyType = Σ (Π A B) (λ g → f ∼ g)
+
+  -- We crucially make use of the η-rule for functions here
+  s : homotopyType → fibreOverId
+  s (g , h) = ((λ a → (a , g a , h a)) , idp)
+
+  r : fibreOverId → homotopyType
+  r (func , p) = fst ∘ img , snd ∘ img
+               where
+                 img : (a : A) → image a
+                 img a = transport image (happly p a) (snd (func a))
+
+  -- and here
+  var-funext : is-prop homotopyType
+  var-funext = contr-is-prop (contr-retract r s (λ _ → idp)
+                              fibreOverId-is-contr)
+
+module _ {i} {A : Type i} {B : A → Type i} {f g : Π A B} where
+  pre-funext : (h : f ∼ g) → is-contr ((f , idh {g = g}) == (g , h))
+  pre-funext h = has-level-apply var-funext (f , idh {g = g}) (g , h)
+
+  funext : is-equiv (happly {f = f}{g = g})
+  funext = contr-map-is-equiv
+             λ h → equiv-preserves-level
+                     (fib-happly-lemma h)
+                     ⦃ pre-funext h ⦄