From d8e2206bbc356321e2de8b01f34759c43303d3d7 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Mon, 1 Dec 2014 13:37:32 -0500
Subject: [PATCH] feat(library/hott): try to replace the proof irrelevance

---
 .../hott/algebra/category/constructions.lean  |  3 +-
 .../category/natural_transformation.lean      | 23 +++++++++++---
 library/hott/equiv.lean                       |  1 +
 library/hott/path.lean                        | 31 +++++++++++++++++++
 4 files changed, 53 insertions(+), 5 deletions(-)

diff --git a/library/hott/algebra/category/constructions.lean b/library/hott/algebra/category/constructions.lean
index 5697d90b1..0db678962 100644
--- a/library/hott/algebra/category/constructions.lean
+++ b/library/hott/algebra/category/constructions.lean
@@ -8,7 +8,8 @@
 import .natural_transformation
 import data.unit data.sigma data.prod data.empty data.bool
 
-open eq eq.ops prod
+open path prod
+
 namespace category
   namespace opposite
   section
diff --git a/library/hott/algebra/category/natural_transformation.lean b/library/hott/algebra/category/natural_transformation.lean
index 3b488183b..ef4b7df2c 100644
--- a/library/hott/algebra/category/natural_transformation.lean
+++ b/library/hott/algebra/category/natural_transformation.lean
@@ -3,7 +3,7 @@
 -- Author: Floris van Doorn, Jakob von Raumer
 
 import .functor hott.axioms.funext
-open precategory path functor
+open precategory path functor truncation
 
 inductive natural_transformation {C D : Precategory} (F G : C ⇒ D) : Type :=
 mk : Π (η : Π (a : C), hom (F a) (G a))
@@ -35,20 +35,35 @@ namespace natural_transformation
 
   infixr `∘n`:60 := compose
 
-  definition foo (C : Precategory) (a b : C) (f g : hom a b) (p q : f ≈ g) : p ≈ q :=
+  /-definition foo (C : Precategory) (a b : C) (f g : hom a b) (p q : f ≈ g) : p ≈ q :=
   @truncation.is_hset.elim _ !homH f g p q
 
+  definition nt_is_hset {F G : functor C D} : is_hset (F ⟹ G) := sorry
+
+  definition eta_nat_path {η₁ η₂ : F ⟹ G} (H1 : natural_map η₁ ≈ natural_map η₂)
+      (H2 : (H1 ▹ naturality η₁) ≈ naturality η₂) : η₁ ≈ η₂ :=
+  rec_on η₁ (λ eta1 nat1, rec_on η₂ (λ eta2 nat2, sorry))-/
+
   protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) [fext : funext.{l_1 l_4}] :
       η₃ ∘n (η₂ ∘n η₁) ≈ (η₃ ∘n η₂) ∘n η₁ :=
-  dcongr_arg2 mk (funext.path_forall _ _ (λ x, !assoc)) sorry
+  have prir [visible] : is_hset (Π {a b : C} (f : hom a b), I f ∘ (η₃ ∘n η₂) a ∘ η₁ a ≈ ((η₃ ∘n η₂) b ∘ η₁ b) ∘ F f),
+    from sorry,
+  path.dcongr_arg2 mk
+    (funext.path_forall
+      (λ (x : C), η₃ x ∘ (η₂ x ∘ η₁ x))
+      (λ (x : C), (η₃ x ∘ η₂ x) ∘ η₁ x)
+      (λ x, assoc (η₃ x) (η₂ x) (η₁ x))
+    )
+    sorry --(@is_hset.elim _ _ _ _ _ _)
 
   protected definition id {C D : Precategory} {F : functor C D} : natural_transformation F F :=
   mk (λa, id) (λa b f, !id_right ⬝ (!id_left⁻¹))
   protected definition ID {C D : Precategory} (F : functor C D) : natural_transformation F F := id
 
   protected theorem id_left (η : F ⟹ G) [fext : funext] : natural_transformation.compose id η ≈ η :=
-  rec (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_left)) sorry) η
+  rec_on η (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_left)) sorry)
 
   protected theorem id_right (η : F ⟹ G) [fext : funext] : natural_transformation.compose η id ≈ η :=
   rec (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_right)) sorry) η
+
 end natural_transformation
diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index b9a478fee..3afc3fa51 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -16,6 +16,7 @@ structure is_equiv [class] {A B : Type} (f : A → B) :=
   (sect : (inv ∘ f) ∼ id)
   (adj : Πx, retr (f x) ≈ ap f (sect x))
 
+
 -- A more bundled version of equivalence to calculate with
 structure equiv (A B : Type) :=
   (to_fun : A → B)
diff --git a/library/hott/path.lean b/library/hott/path.lean
index 16044d262..dd98bf0ca 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -642,6 +642,36 @@ definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A}
     ⬝ (whiskerR ((transport2_p2p B r1 r2 (f x))⁻¹) (apD f p3)) :=
 rec_on r2 (rec_on r1 (rec_on p1 idp))
 
+section
+variables {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D}
+
+theorem congr_arg2 (f : A → B → C) (Ha : a ≈ a') (Hb : b ≈ b') : f a b ≈ f a' b' :=
+rec_on Ha (rec_on Hb idp)
+
+theorem congr_arg3 (f : A → B → C → D) (Ha : a ≈ a') (Hb : b ≈ b') (Hc : c ≈ c')
+    : f a b c ≈ f a' b' c' :=
+rec_on Ha (congr_arg2 (f a) Hb Hc)
+
+theorem congr_arg4 (f : A → B → C → D → E) (Ha : a ≈ a') (Hb : b ≈ b') (Hc : c ≈ c') (Hd : d ≈ d')
+    : f a b c d ≈ f a' b' c' d' :=
+rec_on Ha (congr_arg3 (f a) Hb Hc Hd)
+
+end
+
+section
+variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
+          {E : Πa b c, D a b c → Type} {F : Type}
+variables {a a' : A}
+          {b : B a} {b' : B a'}
+          {c : C a b} {c' : C a' b'}
+          {d : D a b c} {d' : D a' b' c'}
+
+theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a ≈ a') (Hb : Ha ▹ b ≈ b')
+    : f a b ≈ f a' b' :=
+rec_on Hb (rec_on Ha idp)
+
+end
+
 /- From the Coq version:
 
 -- ** Tactics, hints, and aliases
@@ -694,4 +724,5 @@ Ltac hott_simpl :=
   autorewrite with paths in * |- * ; auto with path_hints.
 
 -/
+
 end path