# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511322557 -32400
# Node ID dad072d52d0e00828c9e9a10da6790820e89731e
# Parent  73a9987111187dc5c475feae6b95f48fd54b5ad2
fix

diff -r 73a998711118 -r dad072d52d0e monoidal.agda
--- a/monoidal.agda	Wed Nov 22 11:51:34 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 12:49:17 2017 +0900
@@ -295,15 +295,32 @@
 
 open import Category.Sets
 
+import Relation.Binary.PropositionalEquality
+-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
+postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
 data One {c : Level} : Set c where
   OneObj : One   -- () in Haskell ( or any one object set )
 
+isoSets  :{c₁ : Level} {a : Obj (Sets {c₁} ) } → Iso (Sets {c₁}) a ( a * One {c₁} )
+isoSets {a} = record {
+         ≅→ =  λ x → ( x , OneObj ) ;
+         ≅← =  λ x →   proj₁ x ;
+         iso→  =  refl ;
+         iso←  =  iso←
+     }
+  where
+    lemma : {a : Obj Sets } → (x : a * One) → (Sets [ (λ x₁ → x₁ , OneObj) o proj₁ ]) x ≡ id1 Sets (a * One) x
+    lemma (_ , OneObj ) = refl
+    iso← : {a : Obj Sets} → Sets [ Sets [ (λ x → x , OneObj) o proj₁ ] ≈ id1 Sets (a * One) ]
+    iso← {a} = extensionality Sets ( λ x → lemma x ) 
+
+
 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where
   field
-      unit  : Hom (Sets {c₁}) One One
+      unit  : FObj f One
       φ    : {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
-      iso  : {a : Obj Sets} → Iso Sets One {!!}
   **    : {a b : Obj Sets} → FObj f a →  FObj f b →  FObj f ( a * b ) 
   ** x y  = φ ( x , y )
 
@@ -319,8 +336,8 @@
 lemma1 f app = record { unit = unit ; φ = φ }
   where
      open Applicative
-     unit  :  Hom Sets One One
-     unit OneObj = OneObj
+     unit  :  FObj f One
+     unit = pure app OneObj
      φ :  {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
      φ {a} {b} ( x , y ) = <*> app {!!} {!!}
 
@@ -329,6 +346,6 @@
   where
      open HaskellMonoidalFunctor
      pure  :  {a : Obj Sets} → Hom Sets a ( FObj f a )
-     pure {a} x = {!!}
+     pure {a} x = {!!} -- (unit app)
      <*> :   {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
      <*> {a} {b} x = {!!}