feat(library/hott) Ported part of UnivalenceImpliesFunext.v

library/hott/funext_from_ua.lean

@@ -0,0 +1,81 @@
+-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jakob von Raumer
+-- Ported from Coq HoTT
+import hott.axioms.ua hott.equiv hott.equiv_precomp
+import data.prod data.sigma
+
+open path function prod sigma
+
+-- First, define an axiom free variant of Univalence
+definition ua_type := Π (A B : Type), IsEquiv (equiv_path A B)
+
+context
+  parameters {ua : ua_type}
+
+  -- TODO base this theorem on UA instead of FunExt.
+  -- IsEquiv.postcompose relies on FunExt!
+  protected theorem ua_isequiv_postcompose {A B C : Type} {w : A → B} {H0 : IsEquiv w}
+      : IsEquiv (@compose C A B w) :=
+    !IsEquiv.postcompose
+
+  -- We are ready to prove functional extensionality,
+  -- starting with the naive non-dependent version.
+  protected definition diagonal [reducible] (B : Type) : Type
+    := Σ xy : B × B, pr₁ xy ≈ pr₂ xy
+
+  protected definition isequiv_src_compose {A B C : Type}
+      : @IsEquiv (A → diagonal B)
+                 (A → B)
+                 (compose (pr₁ ∘ dpr1))
+    := @ua_isequiv_postcompose _ _ _ (pr₁ ∘ dpr1)
+        (IsEquiv.adjointify (pr₁ ∘ dpr1)
+          (λ x, dpair (x , x) idp) (λx, idp)
+          (λ x, sigma.rec_on x
+            (λ xy, prod.rec_on xy
+              (λ b c p, path.rec_on p idp))))
+
+  protected definition isequiv_tgt_compose {A B C : Type}
+      : @IsEquiv (A → diagonal B)
+                 (A → B)
+                 (compose (pr₂ ∘ dpr1))
+    := @ua_isequiv_postcompose _ _ _ (pr2 ∘ dpr1)
+        (IsEquiv.adjointify (pr2 ∘ dpr1)
+          (λ x, dpair (x , x) idp) (λx, idp)
+          (λ x, sigma.rec_on x
+            (λ xy, prod.rec_on xy
+              (λ b c p, path.rec_on p idp))))
+
+  theorem univalence_implies_funext_nondep (A B : Type)
+      : Π (f g : A → B), f ∼ g → f ≈ g
+    := (λ (f g : A → B) (p : f ∼ g),
+          let d := λ (x : A), dpair (f x , f x) idp in
+          let e := λ (x : A), dpair (f x , g x) (p x) in
+          let precomp1 :=  compose (pr₁ ∘ dpr1) in
+          have equiv1 [visible] : IsEquiv precomp1,
+            from @isequiv_src_compose A B (diagonal B),
+          have equiv2 [visible] : Π x y, IsEquiv (ap precomp1),
+            from IsEquiv.ap_closed precomp1,
+          have H' : Π (x y : A → diagonal B),
+              pr₁ ∘ dpr1 ∘ x ≈ pr₁ ∘ dpr1 ∘ y → x ≈ y,
+            from (λ x y, IsEquiv.inv (ap precomp1)),
+          have eq2 : pr₁ ∘ dpr1 ∘ d ≈ pr₁ ∘ dpr1 ∘ e,
+            from idp,
+          have eq0 : d ≈ e,
+            from H' d e eq2,
+          have eq1 : (pr₂ ∘ dpr1) ∘ d ≈ (pr₂ ∘ dpr1) ∘ e,
+            from ap _ eq0,
+          eq1
+       )
+
+end
+
+
+
+
+
+
+-- In the following we will proof function extensionality using the univalence axiom
+definition funext_from_ua {A : Type} {P : A → Type} (f g : Πx, P x)
+    : IsEquiv (@apD10 A P f g) :=
+  sorry