Mercurial > hg > Members > kono > Proof > category

changeset 981:0e417c508096

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Mar 2021 04:51:55 +0900
parents 8ab4307d9337
children 888e6613b99a
files src/CCC.agda src/ToposEx.agda
diffstat 2 files changed, 8 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- 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
 
--- 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