--- 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