# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678464864 -32400
# Node ID 4a6d3d27a9fbce14f3ebc276992e0428b66f82b6
# Parent  270f0ba65b88db7854f7683a0e680ba6d9acdf88
...

diff -r 270f0ba65b88 -r 4a6d3d27a9fb src/CCChom.agda
--- a/src/CCChom.agda	Fri Mar 10 16:19:46 2023 +0900
+++ b/src/CCChom.agda	Sat Mar 11 01:14:24 2023 +0900
@@ -36,17 +36,6 @@
          lemma {a} {b} {f} with f
          ... | OneObj = refl
 
-record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
-          :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔  c₁'  ⊔  c₂' ⊔ ℓ' ) where
-      field
-           ≅→ :  Hom A a b   → Hom B a' b'
-           ≅← :  Hom B a' b' → Hom A a b
-           iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
-           iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
-           cong→ : {f g : Hom A a b }  → A [ f ≈ g ] →  B [ ≅→ f ≈ ≅→ g ]
-           cong← : {f g : Hom B a' b'} → B [ f ≈ g ] →  A [ ≅← f ≈ ≅← g ]
-
-
 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) 
           ( _*_ : Obj A → Obj A → Obj A  ) ( _^_ : Obj A → Obj A → Obj A  ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
diff -r 270f0ba65b88 -r 4a6d3d27a9fb src/cat-utility.agda
--- a/src/cat-utility.agda	Fri Mar 10 16:19:46 2023 +0900
+++ b/src/cat-utility.agda	Sat Mar 11 01:14:24 2023 +0900
@@ -13,6 +13,9 @@
         id1 A a =  (Id {_} {_} {_} {A} a)
         -- We cannot make A implicit
 
+        --
+        -- one to one (without naturality)
+        -- 
         record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ)
                  (x y : Obj C )
                 : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
@@ -27,6 +30,18 @@
         sym-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) {x y : Obj C } → Iso C x y → Iso C y x
         sym-iso C i = record { ≅→ = Iso.≅← i  ; ≅← = Iso.≅→ i ; iso→  = Iso.iso← i ; iso←  =  Iso.iso→ i }
 
+        -- Iso with cong
+        --
+        record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
+                  :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔  c₁'  ⊔  c₂' ⊔ ℓ' ) where
+              field
+                   ≅→ :  Hom A a b   → Hom B a' b'
+                   ≅← :  Hom B a' b' → Hom A a b
+                   iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
+                   iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
+                   cong→ : {f g : Hom A a b }  → A [ f ≈ g ] →  B [ ≅→ f ≈ ≅→ g ]
+                   cong← : {f g : Hom B a' b'} → B [ f ≈ g ] →  A [ ≅← f ≈ ≅← g ]
+
         record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( U : Functor B A )
                          ( F : Obj A → Obj B )
diff -r 270f0ba65b88 -r 4a6d3d27a9fb src/freyd2.agda
--- a/src/freyd2.agda	Fri Mar 10 16:19:46 2023 +0900
+++ b/src/freyd2.agda	Sat Mar 11 01:14:24 2023 +0900
@@ -396,5 +396,43 @@
    -- FisLeftAdjoint  : Adjunction B A U F nat-η nat-ε 
    -- FisLeftAdjoint  = record { isAdjunction = record {
 
+open import Data.Product renaming (_×_ to _∧_  ) hiding ( <_,_> )
+open import Category.Constructions.Product
+
+module pro-ex {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( _*_ : Obj A → Obj A → Obj A ) 
+      (*-iso : (a b c x : Obj A) → IsoS A (A × A)  x c (x , x ) (a , b  )) where
+
+--  Hom A x c ≅ ( Hom A x a ) * ( Hom A x b )
+
+    open IsoS
+
+    import Axiom.Extensionality.Propositional
+    postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
+
+    open import Category.Cat
+
+    *eq :   {a b : Obj (A × A) } { x y : Hom (A × A) a b } →  (x≈y : (A × A) [ x ≈ y  ]) → x ≡ y
+    *eq {a} {b} {x1 , x2} {y1 , y2} (eq1 , eq2) = cong₂ _,_ ( ≡←≈ A eq1 ) ( ≡←≈ A eq2 )
+
+    opA = Category.op A
+    prodFunctor : Functor (Category.op A) (Category.op (A × A))
+    prodFunctor = record {
+           FObj = λ x → x , x
+         ; FMap = λ {x} {y} (f : Hom opA x y ) → f , f
+         ; isFunctor = record { identity = ? ; distr = ? ; ≈-cong = ? }
+      } 
+    t00 : (a c d e : Obj opA) (f : Hom opA a c ) → Hom (A × A) (c , c) (d , e )
+    t00 a c d e f = ≅→ (*-iso d e a  c) f  
+    nat-* : {a b c : Obj A} → NTrans (Category.op A) (Sets {c₂}) (Yoneda A (≡←≈ A) c ) (Yoneda (A × A) *eq (a , b) ○ prodFunctor )   
+    nat-* {a} {b} {c} = record { TMap = λ z f → ≅→ (*-iso a b c z) f  ; isNTrans = record { commute = nat-comm } } where
+       nat-comm : {x y : Obj opA} {f : Hom opA x y} → 
+            Sets [ Sets [ (λ g → opA [ f o proj₁ g ] , opA [ f o proj₂ g ]) o (λ f₁ → ≅→ (*-iso a b c x) f₁) ]
+               ≈  Sets [ (λ f₁ → ≅→ (*-iso a b c y) f₁) o (λ g → opA [ f o g ])  ]  ]
+       nat-comm {x} {y} {f} = f-extensionality (λ g → ( begin
+          opA [ f o proj₁ (≅→ (*-iso a b c x) g) ] , opA [ f o proj₂ (≅→ (*-iso a b c x) g) ] ≡⟨ ? ⟩
+          proj₁ (≅→ (*-iso a b c y) ( opA [ f o g ] )) , proj₂ (≅→ (*-iso a b c y) ( opA [ f o g ] ) ) ≡⟨ refl ⟩
+          ≅→ (*-iso a b c y) ( opA [ f o g ] ) ∎ )  ) where open ≡-Reasoning
+
+
 -- end