fix(hott/algebra) fix some proofs for functor category

hott/algebra/precategory/functor.hlean

@@ -2,9 +2,10 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Floris van Doorn, Jakob von Raumer
 
-import .basic
+import .basic types.pi
 
-open function precategory eq prod equiv is_equiv sigma sigma.ops
+open function precategory eq prod equiv is_equiv sigma sigma.ops truncation
+open pi
 
 structure functor (C D : Precategory) : Type :=
   (obF : C → D)
@@ -36,20 +37,22 @@ namespace functor
         exact (pr₁ S.2.2), exact (pr₂ S.2.2),
     fapply adjointify,
       intro F, apply (functor.rec_on F), intros (d1, d2, d3, d4),
-      exact (dpair d1 (dpair d2 (pair d3 (@d4)))),
+      exact (sigma.mk d1 (sigma.mk d2 (pair d3 (@d4)))),
     intro F, apply (functor.rec_on F), intros (d1, d2, d3, d4), apply idp,
     intro S, apply (sigma.rec_on S), intros (d1, S2),
     apply (sigma.rec_on S2), intros (d2, P1),
     apply (prod.rec_on P1), intros (d3, d4), apply idp,
   end
 
+  -- The following lemmas will later be used to prove that the type of
+  -- precategories formes a precategory itself
   protected definition compose (G : functor D E) (F : functor C D) : functor C E :=
   functor.mk
-    (λx, G (F x))
+    (λ x, G (F x))
     (λ a b f, G (F f))
     (λ a, calc
-      G (F (ID a)) = G id : {respect_id F a} --not giving the braces explicitly makes the elaborator compute a couple more seconds
+      G (F (ID a)) = G (ID (F a)) : {respect_id F a}
-               ... = id   : respect_id G (F a))
+               ... = ID (G (F a)) : respect_id G (F a))
     (λ a b c g f, calc
       G (F (g ∘ f)) = G (F g ∘ F f)     : respect_comp F g f
                 ... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
@@ -57,38 +60,87 @@ namespace functor
   infixr `∘f`:60 := compose
 
 
+
+  protected theorem congr
+    {C : Precategory} {D : Precategory}
+    (F : C → D)
+    (foo2 : Π ⦃a b : C⦄, hom a b → hom (F a) (F b))
+    (foo3a foo3b : Π (a : C), foo2 (ID a) = ID (F a))
+    (foo4a foo4b : Π {a b c : C} (g : @hom C C b c) (f : @hom C C a b),
+      foo2 (g ∘ f) = foo2 g ∘ foo2 f)
+    (p3 : foo3a = foo3b) (p4 : @foo4a = @foo4b)
+      : functor.mk F foo2 foo3a @foo4a = functor.mk F foo2 foo3b @foo4b
+  :=
+  begin
+    apply (eq.rec_on p3), intros,
+    apply (eq.rec_on p4), intros,
+    apply idp,
+  end
+
   protected theorem assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) :
       H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
-  sorry
+  begin
+    apply (functor.rec_on H), intros (H1, H2, H3, H4),
+    apply (functor.rec_on G), intros (G1, G2, G3, G4),
+    apply (functor.rec_on F), intros (F1, F2, F3, F4),
+    fapply functor.congr,
+      apply funext.path_pi, intro a,
+      apply (@is_hset.elim), apply !homH,
+    apply funext.path_pi, intro a,
+    repeat (apply funext.path_pi; intros),
+    apply (@is_hset.elim), apply !homH,
+  end
 
-  /-protected definition id {C : Precategory} : functor C C :=
+  protected definition id {C : Precategory} : functor C C :=
   mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp)
+
   protected definition ID (C : Precategory) : functor C C := id
 
   protected theorem id_left  (F : functor C D) : id ∘f F = F :=
-  functor.rec (λ obF homF idF compF, dcongr_arg4 mk idp idp !proof_irrel !proof_irrel) F
+  begin
+    apply (functor.rec_on F), intros (F1, F2, F3, F4),
+    fapply functor.congr,
+      apply funext.path_pi, intro a,
+      apply (@is_hset.elim), apply !homH,
+    repeat (apply funext.path_pi; intros),
+    apply (@is_hset.elim), apply !homH,
+  end
+
   protected theorem id_right (F : functor C D) : F ∘f id = F :=
-  functor.rec (λ obF homF idF compF, dcongr_arg4 mk idp idp !proof_irrel !proof_irrel) F-/
+  begin
+    apply (functor.rec_on F), intros (F1, F2, F3, F4),
+    fapply functor.congr,
+      apply funext.path_pi, intro a,
+      apply (@is_hset.elim), apply !homH,
+    repeat (apply funext.path_pi; intros),
+    apply (@is_hset.elim), apply !homH,
+  end
 
 end functor
 
-/-
+
 namespace category
   open functor
-  definition category_of_categories [reducible] : category Category :=
+
+  definition precategory_of_precategories : precategory Precategory :=
   mk (λ a b, functor a b)
+     sorry -- TODO: Show that functors form a set?
      (λ a b c g f, functor.compose g f)
      (λ a, functor.id)
      (λ a b c d h g f, !functor.assoc)
      (λ a b f, !functor.id_left)
      (λ a b f, !functor.id_right)
-  definition Category_of_categories [reducible] := Mk category_of_categories
+
+  definition Precategory_of_categories := Mk precategory_of_precategories
 
   namespace ops
-    notation `Cat`:max := Category_of_categories
+
-    instance [persistent] category_of_categories
+    notation `PreCat`:max := Precategory_of_categories
+    instance [persistent] precategory_of_precategories
+
   end ops
-end category-/
+
+end category
 
 namespace functor
 --  open category.ops

hott/algebra/precategory/natural_transformation.hlean

@@ -15,33 +15,12 @@ infixl `⟹`:25 := natural_transformation -- \==>
 namespace natural_transformation
   variables {C D : Precategory} {F G H I : functor C D}
 
-  definition natural_map [coercion] (η : F ⟹ G) : Π(a : C), F a ⟶ G a :=
+  definition natural_map [coercion] (η : F ⟹ G) : Π (a : C), F a ⟶ G a :=
   rec (λ x y, x) η
 
   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)
@@ -52,64 +31,94 @@ namespace natural_transformation
 		      ... = η b ∘ (G f ∘ θ a) : assoc
 		      ... = η b ∘ (θ b ∘ F f) : naturality θ f
 		      ... = (η b ∘ θ b) ∘ F f : assoc)
---congr_arg (λx, η b ∘ x) (naturality θ f) -- this needed to be explicit for some reason (on Oct 24)
 
   infixr `∘n`:60 := compose
 
-  protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) [fext fext2 fext3 : funext] :
+  protected theorem congr
-      η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
+    {C : Precategory} {D : Precategory}
-  -- Proof broken, universe issues?
+    (F G : C ⇒ D)
-  /-have aux [visible] : is_hprop (Π (a b : C) (f : hom a b), I f ∘ (η₃ ∘n η₂) a ∘ η₁ a = ((η₃ ∘n η₂) b ∘ η₁ b) ∘ F f),
+    (η₁ η₂ : Π (a : C), hom (F a) (G a))
+    (nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f)
+    (nat₂ : Π (a b : C) (f : hom a b), G f ∘ η₂ a = η₂ b ∘ F f)
+    (p₁ : η₁ = η₂) (p₂ : p₁ ▹ nat₁ = nat₂)
+    : @natural_transformation.mk C D F G η₁ nat₁ = @natural_transformation.mk C D F G η₂ nat₂
+  :=
   begin
-      repeat (apply trunc_pi; intros),
+    apply (dcongr_arg2 (@natural_transformation.mk C D F G) p₁ p₂),
-      apply (succ_is_trunc -1 (I a_2 ∘ (η₃ ∘n η₂) a ∘ η₁ a)),
+  end
-    end,
+
-  dcongr_arg2 mk (funext.path_forall _ _ (λ x, !assoc)) !is_hprop.elim-/
+  protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
-  sorry
+      η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
+  begin
+    apply (rec_on η₃), intros (η₃1, η₃2),
+    apply (rec_on η₂), intros (η₂1, η₂2),
+    apply (rec_on η₁), intros (η₁1, η₁2),
+    fapply natural_transformation.congr,
+      apply funext.path_pi, intro a,
+      apply assoc,
+    apply funext.path_pi, intro a,
+    apply funext.path_pi, intro b,
+    apply funext.path_pi, intro f,
+    apply (@is_hset.elim), apply !homH,
+  end
 
   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 definition id_left (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
+  protected definition ID {C D : Precategory} (F : functor C D) : natural_transformation F F :=
-      id ∘n η = η :=
+  id
-  --Proof broken like all trunc_pi proofs
+
+  protected definition id_left (η : F ⟹ G) : id ∘n η = η :=
+  begin
+    apply (rec_on η), intros (η₁, nat₁),
+    fapply (natural_transformation.congr F G),
+      apply funext.path_pi, intro a,
+      apply id_left,
+    apply funext.path_pi, intro a,
+    apply funext.path_pi, intro b,
+    apply funext.path_pi, intro f,
+    apply (@is_hset.elim), apply !homH,
+  end
+
+  protected definition id_right (η : F ⟹ G) : η ∘n id = η :=
+  begin
+    apply (rec_on η), intros (η₁, nat₁),
+    fapply (natural_transformation.congr F G),
+      apply funext.path_pi, intro a,
+      apply id_right,
+    apply funext.path_pi, intro a,
+    apply funext.path_pi, intro b,
+    apply funext.path_pi, intro f,
+    apply (@is_hset.elim), apply !homH,
+  end
+
+  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) :=
   /-begin
-    apply (rec_on η), intros (f, H),
+    intro what,
-    fapply (path.dcongr_arg2 mk),
+    fapply equiv.mk,
-      apply (funext.path_forall _ f (λa, !id_left)),
+      intro S, apply natural_transformation.mk, exact (S.2),
-    assert (H1 : is_hprop (Π {a b : C} (g : hom a b), G g ∘ f a = f b ∘ F g)),
+    fapply adjointify,
-      --repeat (apply trunc_pi; intros),
+      intro H, apply (natural_transformation.rec_on H), intros (η, natu),
-      apply (@trunc_pi _ _ _ (-2 .+1) _),
+      exact (sigma.mk η @natu),
-    /-  apply (succ_is_trunc -1 (G a_2 ∘ f a) (f a_1 ∘ F a_2)),
+    intro H, apply (natural_transformation.rec_on _ _ _),
-    apply (!is_hprop.elim),-/
+    intro S2,
   end-/
+  /-(λ x, 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, sigma.mk η nat))
+  (λ H, natural_transformation.rec_on H (λ η nat, refl (natural_transformation.mk η nat)))
+  (λ S, sigma.rec_on S (λ η nat, refl (sigma.mk η nat)))))-/
   sorry
 
-  protected definition id_right (η : F ⟹ G) [fext : funext.{l_1 l_4}] :
+  protected definition to_hset : is_hset (F ⟹ G) :=
-      η ∘n id = η :=
+  begin
-  --Proof broken like all trunc_pi proofs
-  /-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-/
-  sorry
-
-  protected definition to_hset [fx : funext] : is_hset (F ⟹ G) :=
-  --Proof broken like all trunc_pi proofs
-  /-begin
     apply trunc_equiv, apply (equiv.to_is_equiv sigma_char),
     apply trunc_sigma,
       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
-  sorry
 
 end natural_transformation