# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1614714715 -32400
# Node ID 0e417c5080966933d06ed558b3a8d61f5e97bc72
# Parent  8ab4307d9337dd300c96b6c10e085ec2d50f568e
...

diff -r 8ab4307d9337 -r 0e417c508096 src/CCC.agda
--- a/src/CCC.agda	Wed Mar 03 04:30:18 2021 +0900
+++ b/src/CCC.agda	Wed Mar 03 04:51:55 2021 +0900
@@ -224,6 +224,9 @@
      field
          TNat : NatD A １
          gNat : (nat : NatD A １ ) → Hom A (Nat TNat) (Nat nat)
-         nat-unique : (nat : NatD A １ ) → {g : Hom A (Nat TNat) (Nat nat) } → A [ g ≈ gNat nat ]
+         nat-unique : (nat : NatD A １ ) → {g : Hom A (Nat TNat) (Nat nat) }
+             → A [ A [ g o nzero TNat ] ≈ nzero nat ]
+             → A [ A [ g o nsuc TNat ] ≈ A [ nsuc nat o g ] ]
+             → A [ g ≈ gNat nat ]
          isToposN : IsToposNat A １ TNat gNat
 
diff -r 8ab4307d9337 -r 0e417c508096 src/ToposEx.agda
--- a/src/ToposEx.agda	Wed Mar 03 04:30:18 2021 +0900
+++ b/src/ToposEx.agda	Wed Mar 03 04:51:55 2021 +0900
@@ -177,10 +177,10 @@
         f = π o fg
         g : Hom A N a
         g = π' o fg
-        ig : {i : Hom A N N }  → i ≈ id1 A N 
-        ig {i} = begin
-           i   ≈⟨ nat-unique TNat  ⟩
-           gNat TNat   ≈↑⟨ nat-unique TNat ⟩
+        ig : f ≈ id1 A N 
+        ig  = begin
+           f   ≈⟨ nat-unique TNat {!!} {!!}  ⟩
+           gNat TNat   ≈↑⟨ nat-unique TNat idL (trans-hom idL (sym idR) ) ⟩
            id1 A _  ∎
         i : f o nzero TNat  ≈ nzero TNat
         i = begin