michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/hott): finish associativity proof

Browse source
This commit is contained in:
Jakob von Raumer 2014-12-01 19:24:44 -05:00 committed by Leonardo de Moura
parent d8e2206bbc
commit ae618c20fb
1 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
library/hott/algebra/category/natural_transformation.lean
View file

@ -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