From 31d1076bd7f602b9f55e217b7073ca9e3fd298bd Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Wed, 31 Dec 2014 19:30:17 -0500 Subject: [PATCH] fix(hott/algebra) fix some proofs for functor category --- hott/algebra/precategory/functor.hlean | 86 ++++++++--- .../precategory/natural_transformation.hlean | 139 ++++++++++-------- 2 files changed, 143 insertions(+), 82 deletions(-) diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 4a4b8aac1..bf05502f2 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/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) @@ -24,7 +25,7 @@ namespace functor -- "functor C D" is equivalent to a certain sigma type set_option unifier.max_steps 38500 protected definition sigma_char : - (Σ (obF : C → D) + (Σ (obF : C → D) (homF : Π ⦃a b : C⦄, hom a b → hom (obF a) (obF b)), (Π (a : C), homF (ID a) = ID (obF a)) × (Π {a b c : C} (g : hom b c) (f : hom a b), @@ -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 - ... = id : respect_id G (F a)) + G (F (ID a)) = G (ID (F a)) : {respect_id 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 diff --git a/hott/algebra/precategory/natural_transformation.hlean b/hott/algebra/precategory/natural_transformation.hlean index 9b364ce9a..506340c31 100644 --- a/hott/algebra/precategory/natural_transformation.hlean +++ b/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 + {C : Precategory} {D : Precategory} + (F G : C ⇒ D) + (η₁ η₂ : Π (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 + apply (dcongr_arg2 (@natural_transformation.mk C D F G) p₁ p₂), + end + + protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) : η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ := - -- Proof broken, universe issues? - /-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-/ - sorry + 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}] : - id ∘n η = η := - --Proof broken like all trunc_pi proofs + protected definition ID {C D : Precategory} (F : functor C D) : natural_transformation F F := + id + + 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), - 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 (@trunc_pi _ _ _ (-2 .+1) _), - /- apply (succ_is_trunc -1 (G a_2 ∘ f a) (f a_1 ∘ F a_2)), - apply (!is_hprop.elim),-/ + intro what, + 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 (sigma.mk η @natu), + intro H, apply (natural_transformation.rec_on _ _ _), + 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}] : - η ∘n id = η := - --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 + protected definition to_hset : is_hset (F ⟹ G) := + 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-/ - sorry + 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