Mercurial > hg > Members > kono > Proof > category

changeset 284:4be696e3fd94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comutativity remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 19:12:45 +0900
parents 5492a0681f55
children 46d4ad55b948
files pullback.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 19:08:23 2013 +0900
+++ b/pullback.agda	Mon Sep 23 19:12:45 2013 +0900
@@ -403,7 +403,13 @@
                       e o f 
                 ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩
                       product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e  o f ) ) )
-                ≈⟨ ? ⟩
+                ≈⟨ ip-cong  (prod p (FObj Γ) proj) ( λ i → begin
+                    proj i o ( e o f )
+                ≈⟨ assoc  ⟩
+                    ( proj i o  e ) o f 
+                ≈⟨  lim=t {i} ⟩
+                    TMap t i
+                ∎ ) ⟩
                       product (prod p (FObj Γ) proj) (TMap t)
                 ∎ ) ⟩
                     f