lean2/tests/lean/hott/krewrite_bug.hlean
2015-06-08 16:46:28 -07:00

34 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