From 67f71ee37649199c20dfed5095dfce662591f4ce Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Mon, 1 Dec 2014 23:12:57 -0500
Subject: [PATCH] feat(library/hott): finish porting of
 natural_transformation.lean

---
 .../category/natural_transformation.lean      | 49 +++++++++++--------
 library/hott/trunc.lean                       |  4 +-
 2 files changed, 30 insertions(+), 23 deletions(-)

diff --git a/library/hott/algebra/category/natural_transformation.lean b/library/hott/algebra/category/natural_transformation.lean
index 5adbc871a0..e633695214 100644
--- a/library/hott/algebra/category/natural_transformation.lean
+++ b/library/hott/algebra/category/natural_transformation.lean
@@ -35,34 +35,41 @@ 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 :=
-  @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] :
       η₃ ∘n (η₂ ∘n η₁) ≈ (η₃ ∘n η₂) ∘n η₁ :=
-  have aux4 [visible] : is_hprop (Π (a b : C) (f : hom a b), I f ∘ (η₃ ∘n η₂) a ∘ η₁ a ≈ ((η₃ ∘n η₂) b ∘ η₁ b) ∘ F f),
-  begin
-    apply trunc_pi, intro a,
-    apply trunc_pi, intro b,
-    apply trunc_pi, intro f,
-    apply (@succ_is_trunc _ -1 _ (I f ∘ (η₃ ∘n η₂) a ∘ η₁ a) (((η₃ ∘n η₂) b ∘ η₁ b) ∘ F f)),
-  end,
-  path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !assoc)) !is_hprop.elim
+  have aux [visible] : is_hprop (Π (a b : C) (f : hom a b), I f ∘ (η₃ ∘n η₂) a ∘ η₁ a ≈ ((η₃ ∘n η₂) b ∘ η₁ b) ∘ F f),
+    begin
+      repeat (apply trunc_pi; intros),
+      apply (succ_is_trunc -1 (I a_2 ∘ (η₃ ∘n η₂) a ∘ η₁ a)),
+    end,
+  dcongr_arg2 mk (funext.path_forall _ _ (λ x, !assoc)) !is_hprop.elim
 
-exit
   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_on η (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_left)) sorry)
+  protected theorem id_left (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
+      id ∘n η ≈ η :=
+  begin
+    apply (rec_on η), intros (f, H),
+    fapply (path.dcongr_arg2 mk),
+      apply (funext.path_forall _ f (λa, !id_left)),
+    assert (H1 : is_hprop (Π {a b : C} (g : hom a b), G g ∘ f a ≈ f b ∘ F g)),
+      repeat (apply trunc_pi; intros),
+      apply (succ_is_trunc -1 (G a_2 ∘ f a) (f a_1 ∘ F a_2)),
+    apply (!is_hprop.elim),
+  end
 
-  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) η
+  protected theorem id_right (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
+      η ∘n id ≈ η :=
+  begin
+    apply (rec_on η), intros (f, H),
+    fapply (path.dcongr_arg2 mk),
+      apply (funext.path_forall _ f (λa, !id_right)),
+    assert (H1 : is_hprop (Π {a b : C} (g : hom a b), G g ∘ f a ≈ f b ∘ F g)),
+      repeat (apply trunc_pi; intros),
+      apply (succ_is_trunc -1 (G a_2 ∘ f a) (f a_1 ∘ F a_2)),
+    apply (!is_hprop.elim),
+  end
 
 end natural_transformation
diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean
index 8fd11254ee..b477d60671 100644
--- a/library/hott/trunc.lean
+++ b/library/hott/trunc.lean
@@ -79,12 +79,12 @@ namespace truncation
   variables {A B : Type}
 
   -- maybe rename to is_trunc_succ.mk
-  definition is_trunc_succ (A : Type) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)]
+  definition is_trunc_succ (A : Type) (n : trunc_index) [H : ∀x y : A, is_trunc n (x ≈ y)]
     : is_trunc n.+1 A :=
   is_trunc.mk (λ x y, !is_trunc.to_internal)
 
   -- maybe rename to is_trunc_succ.elim
-  definition succ_is_trunc {n : trunc_index} [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) :=
+  definition succ_is_trunc (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) :=
   is_trunc.mk (!is_trunc.to_internal x y)
 
   /- contractibility -/