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

refactor(hott/algebra/precategory/yoneda): remove unnecessary annotations

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-12 20:06:25 -07:00
parent 7accd0f1e6
commit 0118ecf3cd
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
hott/algebra/precategory/yoneda.hlean
View file

@ -51,7 +51,7 @@ namespace functor
(λd₁ d₂ d₃ g' g, calc
F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : by rewrite id_comp
... = F ((id,g') ∘ (id, g)) : by esimp
... = F (id,g') ∘ F (id, g) : by rewrite (respect_comp F))
... = F (id,g') ∘ F (id, g) : by rewrite respect_comp)
local abbreviation Fob := @functor_curry_ob
@ -109,9 +109,9 @@ namespace functor
Ghom G (f' ∘ f)
= to_fun_hom (to_fun_ob G p''.1) (f'.2 ∘ f.2) ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by esimp
... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by rewrite (respect_comp (to_fun_ob G p''.1) f'.2 f.2)
∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by rewrite respect_comp
... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2 : by rewrite (respect_comp G f'.1 f.1)
∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2 : by rewrite respect_comp
... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp
... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)