# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1380106475 -32400
# Node ID db4ecbdbf9e9fa29cd2610c79d857a6d0095ae93
# Parent  fb0ab8c72e15476851090a81786b2d177823abbc
limit1 done

diff -r fb0ab8c72e15 -r db4ecbdbf9e9 pullback.agda
--- a/pullback.agda	Wed Sep 25 19:34:10 2013 +0900
+++ b/pullback.agda	Wed Sep 25 19:54:35 2013 +0900
@@ -486,7 +486,25 @@
              TMap = tfmap a t ; 
              isNTrans = record { commute = λ {a'} {b} {f} → let  open ≈-Reasoning (B) in begin
                   FMap Γ f o tfmap a t a' 
-               ≈⟨ {!!}  ⟩
+               ≈⟨⟩
+                  FMap Γ f o ( TMap ε (FObj Γ a') o FMap F (TMap t a'))
+               ≈⟨ assoc ⟩
+                  (FMap Γ f o  TMap ε (FObj Γ a') ) o FMap F (TMap t a')
+               ≈⟨ car (nat ε) ⟩
+                  (TMap ε (FObj Γ b) o FMap (F ○ U) (FMap Γ f) ) o FMap F (TMap t a')
+               ≈↑⟨ assoc ⟩
+                  TMap ε (FObj Γ b) o ( FMap (F ○ U) (FMap Γ f)  o FMap F (TMap t a') )
+               ≈↑⟨ cdr ( distr F ) ⟩
+                  TMap ε (FObj Γ b) o ( FMap F (A [ FMap U (FMap Γ f) o TMap t a' ] ) )
+               ≈⟨ cdr ( fcong F (nat t) ) ⟩
+                  TMap ε (FObj Γ b) o  FMap F (A [ TMap t b o FMap (K A I a) f ])
+               ≈⟨⟩
+                  TMap ε (FObj Γ b) o  FMap F (A [ TMap t b o id1 A (FObj (K A I a) b) ])
+               ≈⟨ cdr ( fcong F (IsCategory.identityR (Category.isCategory A))) ⟩
+                  TMap ε (FObj Γ b) o  FMap F (TMap t b )
+               ≈↑⟨ idR ⟩
+                  ( TMap ε (FObj Γ b)  o  FMap F (TMap t b))  o  id1 B (FObj F (FObj (K A I a) b))
+               ≈⟨⟩
                   tfmap a t b o FMap (K B I (FObj F a)) f 
                ∎
           } }