Mercurial > hg > Members > kono > Proof > category

comparison freyd1.agda @ 659:372205f40ab0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Jul 2017 14:05:18 +0900
parents 5c7908202d5a
children 917e51be9bbf
comparison
equal deleted inserted replaced
658:9242298cffa8 659:372205f40ab0
225 ( hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) 225 ( hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) )
226 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) 226 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
227 ≈↑⟨ assoc ⟩ 227 ≈↑⟨ assoc ⟩
228 hom ( FObj Γ i ) o 228 hom ( FObj Γ i ) o
229 ((FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) 229 ((FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) )
230 ≈↑⟨ cdr ( distr F ) ⟩ 230 ≈↑⟨ cdr ( distr F) ⟩
231 hom ( FObj Γ i ) o 231 hom ( FObj Γ i ) o
232 FMap F ( A [ TMap (t0 ( climit comp (FIA Γ))) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) 232 FMap F ( A [ TMap (t0 ( climit comp (FIA Γ))) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] )
233 ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩ 233 ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩
234 hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) 234 hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i )
235 ≈⟨⟩ 235 ≈⟨⟩