From 7c1b75c8182a681ec54dcd2fe61115cd8af3c282 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 3 Dec 2014 13:54:57 -0500
Subject: [PATCH] feat(library/hott): add proof that the type of nat trafos is
 a set

The characteriszation of nat trafo by sigma types up to equivalence is still to be done (two unsuccessful proof attempts included)
---
 .../algebra/precategory/constructions.lean    | 14 +++----
 library/hott/algebra/precategory/iso.lean     |  4 +-
 .../precategory/natural_transformation.lean   | 39 +++++++++++++++++--
 3 files changed, 42 insertions(+), 15 deletions(-)

diff --git a/library/hott/algebra/precategory/constructions.lean b/library/hott/algebra/precategory/constructions.lean
index 96c021ab8..6ca121b87 100644
--- a/library/hott/algebra/precategory/constructions.lean
+++ b/library/hott/algebra/precategory/constructions.lean
@@ -23,14 +23,6 @@ namespace precategory
      (λ a b f, !id_left)
 
   definition Opposite (C : Precategory) : Precategory := Mk (opposite C)
-  --direct construction:
-  -- MK C
-  --    (λa b, hom b a)
-  --    (λ a b c f g, g ∘ f)
-  --    (λ a, id)
-  --    (λ a b c d f g h, symm !assoc)
-  --    (λ a b f, !id_right)
-  --    (λ a b f, !id_left)
 
   infixr `∘op`:60 := @compose _ (opposite _) _ _ _
 
@@ -38,8 +30,12 @@ namespace precategory
 
   theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g ≈ g ∘ f := idp
 
+  -- TODO: Decide whether just to use funext for this theorem or
+  --       take the trick they use in Coq-HoTT, and introduce a further
+  --       axiom in the definition of precategories that provides thee
+  --       symmetric associativity proof.
   theorem op_op' {ob : Type} (C : precategory ob) : opposite (opposite C) ≈ C :=
-  sorry --precategory.rec (λ hom homH comp id assoc idl idr, idpath (mk _ _ _ _ _ _)) C
+  sorry
 
   theorem op_op : Opposite (Opposite C) ≈ C :=
   (ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.equal
diff --git a/library/hott/algebra/precategory/iso.lean b/library/hott/algebra/precategory/iso.lean
index fd0668296..fc53bbc74 100644
--- a/library/hott/algebra/precategory/iso.lean
+++ b/library/hott/algebra/precategory/iso.lean
@@ -12,7 +12,7 @@ namespace morphism
   variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
 
   -- "is_iso f" is equivalent to a certain sigma type
-  definition sigma_equiv_of_is_iso (f : hom a b) :
+  definition sigma_char (f : hom a b) :
     (Σ (g : hom b a), (g ∘ f ≈ id) × (f ∘ g ≈ id)) ≃ is_iso f :=
   begin
     fapply (equiv.mk),
@@ -44,7 +44,7 @@ namespace morphism
   definition is_hprop_of_is_iso : is_hset (is_iso f) :=
   begin
     apply trunc_equiv,
-      apply (equiv.to_is_equiv (!sigma_equiv_of_is_iso)),
+      apply (equiv.to_is_equiv (!sigma_char)),
     apply sigma_trunc,
       apply (!homH),
     intro g, apply trunc_prod,
diff --git a/library/hott/algebra/precategory/natural_transformation.lean b/library/hott/algebra/precategory/natural_transformation.lean
index e63369521..6b395962e 100644
--- a/library/hott/algebra/precategory/natural_transformation.lean
+++ b/library/hott/algebra/precategory/natural_transformation.lean
@@ -2,8 +2,8 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn, Jakob von Raumer
 
-import .functor hott.axioms.funext hott.types.pi
-open precategory path functor truncation
+import .functor hott.axioms.funext hott.types.pi hott.types.sigma
+open precategory path functor truncation equiv sigma.ops sigma is_equiv function
 
 inductive natural_transformation {C D : Precategory} (F G : C ⇒ D) : Type :=
 mk : Π (η : Π (a : C), hom (F a) (G a))
@@ -21,6 +21,27 @@ namespace natural_transformation
   theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a ≈ η b ∘ F f :=
   rec (λ x y, y) η
 
+  protected definition sigma_char :
+    (Σ (η : Π (a : C), hom (F a) (G a)), Π (a b : C) (f : hom a b), G f ∘ η a ≈ η b ∘ F f) ≃ (F ⟹ G) :=
+  /-equiv.mk (λ S, natural_transformation.mk S.1 S.2)
+    (adjointify (λ S, natural_transformation.mk S.1 S.2)
+      (λ H, natural_transformation.rec_on H (λ η nat, dpair η nat))
+      (λ H, natural_transformation.rec_on H (λ η nat, idpath (natural_transformation.mk η nat)))
+      (λ S, sigma.rec_on S (λ η nat, idpath (dpair η nat))))-/
+
+  /- THE FOLLLOWING CAUSES LEAN TO SEGFAULT?
+  begin
+    fapply equiv.mk,
+      intro S, apply natural_transformation.mk, exact (S.2),
+    fapply adjointify,
+        intro H, apply (natural_transformation.rec_on H), intros (η, natu),
+        exact (dpair η @natu),
+      intro H, apply (natural_transformation.rec_on _ _ _),
+    intros,
+  end
+  check sigma_char-/
+  sorry
+
   protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
   natural_transformation.mk
     (λ a, η a ∘ θ a)
@@ -48,7 +69,7 @@ namespace natural_transformation
   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.{l_1 l_4}] :
+  protected definition id_left (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
       id ∘n η ≈ η :=
   begin
     apply (rec_on η), intros (f, H),
@@ -60,7 +81,7 @@ namespace natural_transformation
     apply (!is_hprop.elim),
   end
 
-  protected theorem id_right (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
+  protected definition id_right (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
       η ∘n id ≈ η :=
   begin
     apply (rec_on η), intros (f, H),
@@ -72,4 +93,14 @@ namespace natural_transformation
     apply (!is_hprop.elim),
   end
 
+  protected definition to_hset : is_hset (F ⟹ G) :=
+  begin
+    apply trunc_equiv, apply (equiv.to_is_equiv sigma_char),
+    apply sigma_trunc,
+      apply trunc_pi, intro a, exact (@homH (objects D) _ (F a) (G a)),
+    intro η, apply trunc_pi, intro a,
+      apply trunc_pi, intro b, apply trunc_pi, intro f,
+      apply succ_is_trunc, apply trunc_succ, exact (@homH (objects D) _ (F a) (G b)),
+  end
+
 end natural_transformation