# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1614434262 -32400
# Node ID e05eb6029b5ba288879c5b084d1ca0875b15af91
# Parent  9746e93a8c31d6665306925c5cb4053dcef7dab6
...

diff -r 9746e93a8c31 -r e05eb6029b5b src/ToposEx.agda
--- a/src/ToposEx.agda	Sat Feb 27 12:15:28 2021 +0900
+++ b/src/ToposEx.agda	Sat Feb 27 22:57:42 2021 +0900
@@ -91,11 +91,27 @@
      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 = {!!}
+    m1 {d} {b} f g eq = begin
+            f  ≈↑⟨ idL ⟩
+            id1 A _ o f ≈↑⟨ car (IsCCC.e3a isCCC) ⟩
+            (π o < id1 A b , id1 A b >)  o f  ≈↑⟨ assoc ⟩
+            π o (< id1 A b , id1 A b >  o f)  ≈⟨ cdr eq ⟩
+            π o (< id1 A b , id1 A b >  o g)  ≈⟨ assoc ⟩
+            (π o < id1 A b , id1 A b >)  o g  ≈⟨  car (IsCCC.e3a isCCC) ⟩
+            id1 A _ o g  ≈⟨ idL ⟩
+            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→ = {!!}
+  prop32→ {a} {b} f g f=g = begin
+            char t < id1 A b , id1 A b > δmono o < f , g >  ≈⟨  cdr ( IsCCC.π-cong isCCC refl-hom (sym f=g))  ⟩
+            char t < id1 A b , id1 A b > δmono o < f , f >  ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩
+            char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f >    ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩
+            char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f)   ≈⟨ assoc ⟩
+            (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) o f   ≈⟨ {!!} ⟩
+            (⊤ t o  ○  b)  o f  ≈↑⟨ assoc ⟩
+            ⊤ t o  (○  b  o f)  ≈⟨ cdr (IsCCC.e2 isCCC)  ⟩
+            ⊤ t o  ○  a  ∎
 
   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 ]
@@ -104,25 +120,37 @@
   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
+  record prop33  (n : ToposNat 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 > ] ]
+       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' ]
 
   cor33  : (n : ToposNat A １ )
-     → ( {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → prop33 n f h )
+     → prop33 n 
      → 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)
+      ; κ2 = NatD.nsuc (ToposNat.TNat 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} → ?
+              _+_ = λ {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
            ;  uniqueness = {!!}
-           ;  +-cong = {!!}
+           ;  +-cong = λ f=f' g=g' → prop33.g-cong p f=f' (resp refl-hom g=g' )
 
        }
-    }
+    } where
+        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 ]
+        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 ⟩
+            g  ∎
+
+         
+
diff -r 9746e93a8c31 -r e05eb6029b5b src/cat-utility.agda
--- a/src/cat-utility.agda	Sat Feb 27 12:15:28 2021 +0900
+++ b/src/cat-utility.agda	Sat Feb 27 22:57:42 2021 +0900
@@ -253,8 +253,8 @@
                     : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
            field
               _+_ : {c : Obj A} ( f : Hom A a c ) → ( g : Hom A b c ) → Hom A ab c
-              κ1fxg=f : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ1    ] ≈  f ]
-              κ2fxg=g : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ2    ] ≈  g ]
+              κ1f+g=f : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ1    ] ≈  f ]
+              κ2f+g=g : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ2    ] ≈  g ]
               uniqueness : {c : Obj A} { h : Hom A ab c }  → A [  ( A [ h o κ1  ] ) + ( A [ h o κ2  ] ) ≈  h ]
               +-cong : {c : Obj A} { f f' : Hom A a c } → { g g' : Hom A b c } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f + g ≈ f' + g' ]