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

diff -r 8e97363859ce -r 8ab4307d9337 src/CCC.agda
--- a/src/CCC.agda	Wed Mar 03 00:58:24 2021 +0900
+++ b/src/CCC.agda	Wed Mar 03 04:30:18 2021 +0900
@@ -224,5 +224,6 @@
      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 ]
          isToposN : IsToposNat A １ TNat gNat
 
diff -r 8e97363859ce -r 8ab4307d9337 src/ToposEx.agda
--- a/src/ToposEx.agda	Wed Mar 03 00:58:24 2021 +0900
+++ b/src/ToposEx.agda	Wed Mar 03 04:30:18 2021 +0900
@@ -3,7 +3,7 @@
 open import Category
 open import cat-utility
 open import HomReasoning
-module ToposEx   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) where
+module ToposEx   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where
 
   open Topos
   open Equalizer
@@ -151,42 +151,90 @@
             < id1 A b o k , id1 A b o k >   ≈⟨ IsCCC.π-cong isCCC idL idL ⟩ 
             < k , k >  ∎
 
-  N : (n : ToposNat A １ ) → Obj A
-  N n = NatD.Nat (ToposNat.TNat n)
+  open NatD
+  open ToposNat n
 
-  record prop33  (n : ToposNat A １ ) : Set  ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+  N : Obj A
+  N = Nat TNat 
+
+  record prop33   {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N  ∧ a) a )  : Set  ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field 
-       g :  {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → Hom A (N n) a
-       g0=f : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nzero (ToposNat.TNat n) ]  ≈ f ]
-       gs=h : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nsuc  (ToposNat.TNat n) ]  ≈ A [ h o < id1 A _ , g f h > ] ]
-       g-cong :  {a : Obj A} {f f' : Hom A １ a } { h h' : Hom A (N n ∧ a) a } →  A [ f ≈ f' ] → A [ h ≈ h' ] → A [ g f h ≈ g f' h' ]
-
-  p33 : (n : ToposNat A １ ) → prop33 n
-  p33 = {!!}
+       g :  Hom A N  a
+       g0=f : A [ A [ g o nzero TNat  ]  ≈ f ]
+       gs=h : A [ A [ g o nsuc  TNat  ]  ≈ A [ h o < id1 A _ , g > ] ]
 
-  cor33  : (n : ToposNat A １ )
-     → coProduct A １ ( NatD.Nat (ToposNat.TNat n)  ) --  N ≅ N + 1
-  cor33 n = record {
-        coproduct = N n
-      ; κ1 = NatD.nzero (ToposNat.TNat n)
-      ; κ2 = NatD.nsuc (ToposNat.TNat n)
+  p33 : {a : Obj A} (z : Hom A １ a ) ( h : Hom A (N  ∧ a) a )  → prop33  z h
+  p33  {a} z h = record {
+        g = g
+      ; g0=f = iii
+      ; gs=h = v
+    } where
+        xnat : NatD A １
+        xnat = record { Nat = N ∧ a ; nzero = < nzero TNat , z > ; nsuc = < nsuc TNat o π , h > }
+        fg : Hom A N (N ∧ a )
+        fg = gNat xnat
+        f : Hom A N N
+        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 ⟩
+           id1 A _  ∎
+        i : f o nzero TNat  ≈ nzero TNat
+        i = begin
+            f o nzero TNat  ≈⟨ car ig  ⟩ id1 A _ o nzero TNat  ≈⟨ idL  ⟩
+            nzero TNat  ∎  
+        ii : f o nsuc TNat  ≈ nsuc  TNat o f
+        ii = begin
+            f o nsuc TNat  ≈⟨ car ig ⟩ id1 A _ o nsuc TNat  ≈⟨ idL ⟩ nsuc TNat  ≈↑⟨ idR ⟩ nsuc TNat o id1 A _  ≈↑⟨ cdr ig  ⟩
+             nsuc  TNat o f  ∎  
+        iii : g o nzero TNat ≈ z
+        iii = begin
+            g o nzero TNat  ≈⟨⟩ (π' o gNat xnat ) o nzero TNat  ≈↑⟨ assoc ⟩ 
+            π' o ( gNat xnat  o nzero TNat)  ≈⟨ cdr (IsToposNat.izero isToposN xnat) ⟩ 
+            π' o < nzero TNat , z >  ≈⟨ IsCCC.e3b isCCC ⟩ 
+            z  ∎  
+        iv : g o nsuc TNat ≈ h o < f , g >
+        iv = begin 
+            g o nsuc TNat  ≈⟨⟩ 
+            (π' o gNat xnat) o nsuc TNat   ≈↑⟨ assoc ⟩ 
+            π' o (gNat xnat o nsuc TNat )  ≈⟨ cdr (IsToposNat.isuc isToposN xnat) ⟩ 
+            π' o  (nsuc xnat o gNat xnat ) ≈⟨ assoc ⟩ 
+            (π' o  nsuc xnat ) o gNat xnat  ≈⟨ car (IsCCC.e3b isCCC) ⟩ 
+            h o gNat xnat  ≈↑⟨ cdr (IsCCC.e3c isCCC) ⟩ 
+            h o < π o fg , π' o fg >  ≈⟨⟩ 
+            h o < f , g >  ∎  
+        v : A [ A [ g o nsuc TNat ] ≈ A [ h o < id1 A N , g > ] ]
+        v = begin
+            g o nsuc TNat   ≈⟨ iv  ⟩ 
+            h o < f , g >   ≈⟨ cdr ( IsCCC.π-cong isCCC ig refl-hom) ⟩ 
+            h o < id1 A N , g >  ∎  
+
+
+  cor33  :  coProduct A １ (Nat TNat ) --  N ≅ N + 1
+  cor33 = record {
+        coproduct = N 
+      ; κ1 = nzero TNat 
+      ; κ2 = nsuc TNat 
       ; isProduct = record {
-              _+_ = λ {a} f g → prop33.g p  f ( g o π )  -- Hom A (N n ∧ a) a
-           ;  κ1f+g=f = λ {a} {f} {g} → prop33.g0=f p f (g o π ) 
-           ;  κ2f+g=g = k2
+              _+_ = λ {a} f g → prop33.g (p  f ( g o π ))  -- Hom A (N n ∧ a) a
+           ;  κ1f+g=f = λ {a} {f} {g} → prop33.g0=f (p f (g o π ) )
+           ;  κ2f+g=g = λ {a} {f} {g} → k2 {a} {f} {g}
            ;  uniqueness = {!!}
-           ;  +-cong = λ f=f' g=g' → prop33.g-cong p f=f' (resp refl-hom g=g' )
-
+           ;  +-cong = λ f=f' g=g' → {!!} -- prop33.g-cong p f=f' (resp refl-hom g=g' )
        }
     } where
-        p = p33 n
-        k2 : {a : Obj A} {f  : Hom A １ a} {g : Hom A (NatD.Nat (ToposNat.TNat n)) a }
-           → A [ A [ prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n) ] ≈ g ]
+        p :  {a : Obj A} (f  : Hom A １ a) ( h : Hom A (N  ∧ a) a ) → prop33  f h
+        p f h = p33  f h
+        k2 : {a : Obj A} {f  : Hom A １ a} {g : Hom A (Nat TNat) a }
+           → A [ A [ prop33.g (p f (g o  π)) o nsuc TNat ] ≈ g ]
         k2 {a} {f} {g} = begin
-            (prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n))  ≈⟨ prop33.gs=h p f (g o π )   ⟩
-            ( g o π ) o  < id1 A (N n) , prop33.g p f (g o π) >   ≈⟨ sym assoc ⟩
-            g o ( π  o   < id1 A (N n) , prop33.g p f (g o π) >)  ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩
-            g o id1 A (N n)  ≈⟨ idR ⟩
+            (prop33.g (p f (g o π)) o nsuc TNat)  ≈⟨ prop33.gs=h (p f (g o π ))   ⟩
+            ( g o π ) o  < id1 A N  , prop33.g (p f (g o π)) >   ≈⟨ sym assoc ⟩
+            g o ( π  o   < id1 A N  , prop33.g (p f (g o π)) >)  ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩
+            g o id1 A N   ≈⟨ idR ⟩
             g  ∎