35 lines
1.3 KiB
Text
35 lines
1.3 KiB
Text
|
import algebra.category.functor
|
||
|
|
|
||
|
|
open function category eq prod prod.ops equiv is_equiv sigma sigma.ops is_trunc funext iso
|
||
|
|
open pi
|
||
|
|
|
||
|
|
namespace functor
|
||
|
|
variables {A B C D E : Precategory}
|
||
|
|
|
||
|
|
definition compose_pentagon_test (K : D ⇒ E) (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
|
||
|
|
(calc K ∘f H ∘f G ∘f F = (K ∘f H) ∘f G ∘f F : functor.assoc
|
||
|
|
... = ((K ∘f H) ∘f G) ∘f F : functor.assoc)
|
||
|
|
=
|
||
|
|
(calc K ∘f H ∘f G ∘f F = K ∘f (H ∘f G) ∘f F : ap (λx, K ∘f x) !functor.assoc
|
||
|
|
... = (K ∘f H ∘f G) ∘f F : functor.assoc
|
||
|
|
... = ((K ∘f H) ∘f G) ∘f F : ap (λx, x ∘f F) !functor.assoc) :=
|
||
|
|
begin
|
||
|
|
have lem1 : Π{F₁ F₂ : A ⇒ D} (p : F₁ = F₂) (a : A),
|
||
|
|
ap010 to_fun_ob (ap (λx, K ∘f x) p) a = ap (to_fun_ob K) (ap010 to_fun_ob p a),
|
||
|
|
by intros; cases p; esimp,
|
||
|
|
have lem2 : Π{F₁ F₂ : B ⇒ E} (p : F₁ = F₂) (a : A),
|
||
|
|
ap010 to_fun_ob (ap (λx, x ∘f F) p) a = ap010 to_fun_ob p (F a),
|
||
|
|
by intros; cases p; esimp,
|
||
|
|
apply functor_eq2,
|
||
|
|
intro a, esimp,
|
||
|
|
krewrite [ap010_con],
|
||
|
|
rewrite [+ap010_con,lem1,lem2,
|
||
|
|
ap010_assoc K H (G ∘f F) a,
|
||
|
|
ap010_assoc (K ∘f H) G F a,
|
||
|
|
ap010_assoc H G F a,
|
||
|
|
ap010_assoc K H G (F a),
|
||
|
|
ap010_assoc K (H ∘f G) F a]
|
||
|
|
end
|
||
|
|
|
||
|
|
end functor
|