From ae618c20fb89123f6cbb38daec68262347379827 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Mon, 1 Dec 2014 19:24:44 -0500 Subject: [PATCH] fix(library/hott): finish associativity proof --- .../category/natural_transformation.lean | 23 +++++++++---------- 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/library/hott/algebra/category/natural_transformation.lean b/library/hott/algebra/category/natural_transformation.lean index ef4b7df2c..5adbc871a 100644 --- a/library/hott/algebra/category/natural_transformation.lean +++ b/library/hott/algebra/category/natural_transformation.lean @@ -2,7 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Floris van Doorn, Jakob von Raumer -import .functor hott.axioms.funext +import .functor hott.axioms.funext hott.types.pi open precategory path functor truncation inductive natural_transformation {C D : Precategory} (F G : C ⇒ D) : Type := @@ -43,19 +43,18 @@ namespace natural_transformation 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}] : + protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) [fext : funext] : η₃ ∘n (η₂ ∘n η₁) ≈ (η₃ ∘n η₂) ∘n η₁ := - 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 _ _ _ _ _ _) + 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 +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