--- a/src/ToposEx.agda	Fri Feb 26 12:19:58 2021 +0900
+++ b/src/ToposEx.agda	Sat Feb 27 12:15:28 2021 +0900
@@ -82,5 +82,47 @@
 --       }
 --    }
 
+module _  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A (CCC.１ c) (CCC.○ c) ) where
+  open ≈-Reasoning A
+  open CCC.CCC c
 
+  δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
+  δmono  = record {
+     isMono = m1
+   } where
+    m1 :   {d b : Obj A} (f g : Hom A d b) → A [ A [  < id1 A b , id1 A b > o f ] ≈ A [  < id1 A b , id1 A b > o g ] ] → A [ f ≈ g ]
+    m1 {d} {b} f g = {!!}
 
+  prop32→ :  {a b : Obj A}→ (f g : Hom A a b )
+    → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono  o < f , g > ]  ≈ A [ ⊤ t o  ○  a  ] ]
+  prop32→ = {!!}
+
+  prop23→ :  {a b : Obj A}→ (f g : Hom A a b )
+    → A [ A [ char t  < id1 A b , id1 A b > δmono  o < f , g > ]  ≈ A [ ⊤ t o  ○  a  ] ] → A [ f ≈ g ]
+  prop23→ = {!!}
+
+  N : (n : ToposNat A １ ) → Obj A
+  N n = NatD.Nat (ToposNat.TNat n)
+
+  record prop33  (n : ToposNat A １ ) {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) : Set  ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+     field 
+       g :  Hom A (N n) a
+       g0=f : A [ A [ g o NatD.nzero (ToposNat.TNat n) ]  ≈ f ]
+       gs=h : A [ A [ g o NatD.nsuc  (ToposNat.TNat n) ]  ≈ A [ h o < id1 A _ , g > ] ]
+
+  cor33  : (n : ToposNat A １ )
+     → ( {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → prop33 n f h )
+     → coProduct A １ ( NatD.Nat (ToposNat.TNat n)  ) --  N ≅ N + 1
+  cor33 n p = record {
+        coproduct = N n
+      ; κ1 = NatD.nzero (ToposNat.TNat n)
+      ; κ2 = id1 A (N n)
+      ; isProduct = record {
+              _+_ = λ {a} f g → prop33.g ( p {a} f π' )
+           ;  κ1fxg=f = λ {a} {f} {g} → prop33.g0=f (p f π' )
+           ;  κ2fxg=g = λ {a} {f} {g} → ?
+           ;  uniqueness = {!!}
+           ;  +-cong = {!!}
+
+       }
+    }