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

feat(hott/algebra/precategory/nat_trans): reduce compilation time using rewrite tactic

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-23 19:55:01 -07:00
parent 38a63a8a58
commit 30e3049c56
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/nat_trans.hlean
View file

@ -97,9 +97,9 @@ namespace nat_trans
nat_trans.mk nat_trans.mk
(λ a, F (η a)) (λ a, F (η a))
(λ a b f, calc (λ a b f, calc
F (H f) ∘ F (η a) = F (H f ∘ η a) : respect_comp F (H f) ∘ F (η a) = F (H f ∘ η a) : by rewrite respect_comp
... = F (η b ∘ G f) : by rewrite (naturality η f) ... = F (η b ∘ G f) : by rewrite (naturality η f)
... = F (η b) ∘ F (G f) : respect_comp) ... = F (η b) ∘ F (G f) : by rewrite respect_comp)
infixr `∘nf`:60 := nat_trans_functor_compose infixr `∘nf`:60 := nat_trans_functor_compose
infixr `∘fn`:60 := functor_nat_trans_compose infixr `∘fn`:60 := functor_nat_trans_compose