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

test(hott/algebra/category): test new 'abstract ... end' expression in the HoTT library

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-12 17:53:01 -07:00
parent 3d9b557cfd
commit 62e1be897c
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
hott/algebra/category/functor.hlean
View file

@ -30,12 +30,12 @@ namespace functor
functor.mk functor.mk
(λ x, G (F x)) (λ x, G (F x))
(λ a b f, G (F f)) (λ a b f, G (F f))
(λ a, calc (λ a, abstract calc
G (F (ID a)) = G (ID (F a)) : by rewrite respect_id G (F (ID a)) = G (ID (F a)) : by rewrite respect_id
... = ID (G (F a)) : by rewrite respect_id) ... = ID (G (F a)) : by rewrite respect_id end)
(λ a b c g f, calc (λ a b c g f, abstract calc
G (F (g ∘ f)) = G (F g ∘ F f) : by rewrite respect_comp G (F (g ∘ f)) = G (F g ∘ F f) : by rewrite respect_comp
... = G (F g) ∘ G (F f) : by rewrite respect_comp) ... = G (F g) ∘ G (F f) : by rewrite respect_comp end)
infixr `∘f`:60 := functor.compose infixr `∘f`:60 := functor.compose

5
hott/algebra/category/nat_trans.hlean
View file

@ -21,12 +21,13 @@ namespace nat_trans
nat_trans.mk nat_trans.mk
(λ a, η a ∘ θ a) (λ a, η a ∘ θ a)
(λ a b f, (λ a b f,
calc abstract calc
H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : by rewrite assoc H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : by rewrite assoc
... = (η b ∘ G f) ∘ θ a : by rewrite naturality ... = (η b ∘ G f) ∘ θ a : by rewrite naturality
... = η b ∘ (G f ∘ θ a) : by rewrite assoc ... = η b ∘ (G f ∘ θ a) : by rewrite assoc
... = η b ∘ (θ b ∘ F f) : by rewrite naturality ... = η b ∘ (θ b ∘ F f) : by rewrite naturality
... = (η b ∘ θ b) ∘ F f : by rewrite assoc) ... = (η b ∘ θ b) ∘ F f : by rewrite assoc
end)
infixr `∘n`:60 := nat_trans.compose infixr `∘n`:60 := nat_trans.compose