Mercurial > hg > Members > kono > Proof > category

diff 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
line wrap: on
line diff
--- a/freyd1.agda	Thu Jul 06 13:50:45 2017 +0900
+++ b/freyd1.agda	Sun Jul 16 14:05:18 2017 +0900
@@ -227,7 +227,7 @@
                    ≈↑⟨ assoc ⟩ 
                            hom ( FObj Γ i ) o 
                               ((FMap F ( TMap (t0 ( climit comp (FIA Γ)))  i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) )
-                   ≈↑⟨ cdr (  distr F ) ⟩ 
+                   ≈↑⟨ cdr (  distr F)  ⟩ 
                            hom ( FObj Γ i ) o  
                                FMap F ( A [ TMap (t0 ( climit comp (FIA Γ)))  i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] )
                    ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩