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

diff -r 72b6b4577911 -r 9746e93a8c31 src/Polynominal.agda
--- a/src/Polynominal.agda	Fri Feb 26 12:19:58 2021 +0900
+++ b/src/Polynominal.agda	Sat Feb 27 12:15:28 2021 +0900
@@ -14,7 +14,7 @@
     open NTrans
 
 --
---  Hom in Sleisli Category
+--  Hom in Kleisli Category
 --
 
     record SHom (a : Obj A)  (b : Obj A)
diff -r 72b6b4577911 -r 9746e93a8c31 src/ToposEx.agda
--- 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 = {!!}
+
+       }
+    }
diff -r 72b6b4577911 -r 9746e93a8c31 src/cat-utility.agda
--- a/src/cat-utility.agda	Fri Feb 26 12:19:58 2021 +0900
+++ b/src/cat-utility.agda	Sat Feb 27 12:15:28 2021 +0900
@@ -247,6 +247,25 @@
               π2 : Hom A product b
               isProduct : IsProduct A a b product π1 π2 
 
+        record IsCoProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  (a b ab : Obj A)
+              ( κ1 : Hom A a ab  )
+              ( κ2 : Hom A b ab  )
+                    : 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 ]
+              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' ]
+
+        record coProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A )
+                    : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
+           field
+              coproduct : Obj A
+              κ1 : Hom A a coproduct 
+              κ2 : Hom A b coproduct 
+              isProduct : IsCoProduct A a b coproduct κ1 κ2 
+
         -----
         --
         -- product on arbitrary index
diff -r 72b6b4577911 -r 9746e93a8c31 src/monoid-monad.agda
--- a/src/monoid-monad.agda	Fri Feb 26 12:19:58 2021 +0900
+++ b/src/monoid-monad.agda	Sat Feb 27 12:15:28 2021 +0900
@@ -5,7 +5,7 @@
 module monoid-monad {c : Level} where
 
 open import Algebra.Structures
-open import HomReasoning
+open import HomReasoning 
 open import cat-utility
 open import Category.Cat
 open import Data.Product
@@ -13,7 +13,7 @@
 open import Relation.Binary
 
 -- open Monoid
-open import Algebra.FunctionProperties using (Op₁; Op₂)
+-- open import Algebra.FunctionProperties using (Op₁; Op₂)
 
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
 
@@ -110,21 +110,23 @@
 Lemma-MM36 : ∀( x y z : Carrier M ) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z ) 
 Lemma-MM36  x y z = ( IsMonoid.assoc ( isMonoid M ))  x y z
 
--- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
 import Relation.Binary.PropositionalEquality
 -- postulate extensionality : { a b : Obj A } {f g : Hom A a b } →  Relation.Binary.PropositionalEquality.Extensionality c c
-postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
+-- postulate extensionality : Axiom.Extensionality.Propositional.Extensionality c c
+
+import Axiom.Extensionality.Propositional
+postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality  c₂ c₂
 
 -- Multi Arguments Functional Extensionality
 extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 
                (∀ x y z  → f x y z ≡ g x y z )  → ( f ≡ g ) 
-extensionality30 eq = extensionality ( λ x → extensionality ( λ y → extensionality (eq x y) ) )
+extensionality30 eq = extensionality A ( λ x → extensionality A ( λ y → extensionality A (eq x y) ) )
 
 Lemma-MM9  :  (λ(x : Carrier M) → ( ε M ∙ x ))  ≡ ( λ(x : Carrier M) → x  )
-Lemma-MM9  = extensionality Lemma-MM34
+Lemma-MM9  = extensionality A Lemma-MM34
 
 Lemma-MM10 : ( λ x →   (x ∙ ε M))  ≡ ( λ x → x ) 
-Lemma-MM10  = extensionality Lemma-MM35
+Lemma-MM10  = extensionality A Lemma-MM35
 
 Lemma-MM11 : (λ x y z → ((x ∙ y ) ∙ z))  ≡ (λ x y z → ( x ∙ (y ∙ z ) ))
 Lemma-MM11 = extensionality30 Lemma-MM36 
@@ -141,7 +143,7 @@
        }  
    } where
        Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-       Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
+       Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) hiding (_∙_) in
                 begin
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
@@ -154,7 +156,7 @@
                      Id {_} {_} {_} {A} (FObj T a)
                 ∎
        Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-       Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
+       Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ )  hiding (_∙_) in
                 begin
                      TMap μ a o (FMap T (TMap η a ))
                 ≈⟨⟩
@@ -167,7 +169,7 @@
                      Id {_} {_} {_} {A} (FObj T a)
                 ∎
        Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-       Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
+       Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ )  hiding (_∙_) in
                 begin
                       TMap μ a o TMap μ ( FObj T a ) 
                 ≈⟨⟩