# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1497361014 -32400
# Node ID afddfebea79747039b2e392c3515b44811a86069
# Parent  f924056bf08a08cfe66c4deb050bef44d4ed6d12
t0f=t0 done

diff -r f924056bf08a -r afddfebea797 freyd2.agda
--- a/freyd2.agda	Tue Jun 13 10:15:24 2017 +0900
+++ b/freyd2.agda	Tue Jun 13 22:36:54 2017 +0900
@@ -153,14 +153,14 @@
       t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
                  ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t  ] ) x
              ≈⟨⟩
-                (FMap (HomA A b) ( TMap (t0 lim) i)) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
-             ≈⟨ {!!} ⟩
-                FMap (HomA A b) (A [ TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) ])  (id1 A b )
-             ≈⟨ ? ⟩
-                FMap (HomA A b) (TMap t i x)  (id1 A b )
-             ≈⟨ {!!} ⟩
-                 {!!} o TMap t i x
-             ≈⟨ idL ⟩
+                FMap (HomA A b) ( TMap (t0 lim) i) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
+             ≈⟨⟩
+                TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b )
+             ≈⟨  cdr idR ⟩
+                TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) 
+             ≈⟨  t0f=t (isLimit lim) ⟩
+                TMap (ta a x t) i
+             ≈⟨⟩
                  TMap t i x
              ∎  ))