# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1499038861 -32400
# Node ID 53f2a11474eee122378adf5a13fa194642d14fd3
# Parent  c65d08d8509225098cf970d79badb6ed361fee69
on going ..

diff -r c65d08d85092 -r 53f2a11474ee freyd2.agda
--- a/freyd2.agda	Mon Jul 03 07:26:58 2017 +0900
+++ b/freyd2.agda	Mon Jul 03 08:41:01 2017 +0900
@@ -299,10 +299,19 @@
                ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i}
                ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t 
          } where
+               revUub : (pi : FObj U (obj (preinitialObj PI)) ) → pi ≡ (hom (preinitialObj PI) OneObj)
+               revUub _ = {!!}
+               revU' : (a : Obj (K Sets A * ↓ U)) 
+                  → Sets [ Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) o hom (preinitialObj PI) ] ≈ hom a ]
+               revU' a  =  let open ≈-Reasoning Sets in begin
+                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) o hom (preinitialObj PI)
+                  ≈⟨ comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ⟩
+                     hom a
+                  ∎ 
                revU : (a : Obj (K Sets A * ↓ U)) 
                   → Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) ≈ ( λ upi → hom a OneObj ) ]
-               revU a  = extensionality Sets ( λ (pi : FObj U (obj (preinitialObj PI)) ) → ( begin 
-                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) pi  
+               revU a  = extensionality Sets ( λ (upi : FObj U (obj (preinitialObj PI)) ) → ( begin 
+                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) upi  
                   ≡⟨ {!!} ⟩
                      FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) (hom (preinitialObj PI) OneObj)
                   ≡⟨ ≡-cong ( λ k → k OneObj ) ( comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) ⟩