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

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

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-12 20:13:40 -07:00
parent 265316a9f5
commit adae95cf68
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/algebra/precategory/functor.hlean
View file

@ -36,8 +36,8 @@ namespace functor
G (F (ID a)) = G (ID (F a)) : {respect_id F a}
... = ID (G (F a)) : respect_id G (F a))
(λ a b c g f, calc
G (F (g ∘ f)) = G (F g ∘ F f) : respect_comp F g f
... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
G (F (g ∘ f)) = G (F g ∘ F f) : by rewrite respect_comp
... = G (F g) ∘ G (F f) : by rewrite respect_comp)
infixr `∘f`:60 := compose