open import Level
open import Category
module monoidal where

open import Data.Product renaming (_×_ to _*_)
open import Category.Constructions.Product
open import HomReasoning
open import cat-utility
open import Relation.Binary.Core
open import Relation.Binary

open Functor

record Iso  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
         (x y : Obj C )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
   field
         ≅→ :  Hom C x y 
         ≅← :  Hom C y x 
         iso→  :  C [ C [ ≅← o ≅→  ] ≈  id1 C x ]
         iso←  :  C [ C [ ≅→ o ≅←  ] ≈  id1 C y ]

-- Monoidal Category

record IsMonoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (I : Obj C) ( BI : Functor ( C × C ) C )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  open Iso 
  infixr 9 _□_ _■_
  _□_ : ( x y : Obj C ) → Obj C
  _□_ x y = FObj BI ( x , y )
  _■_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a □ b ) ( c □ d )
  _■_ f g = FMap BI ( f , g )
  field
      mα-iso : {a b c : Obj C} →  Iso C ( ( a □ b) □ c)  ( a □ ( b □ c ) ) 
      mλ-iso : {a : Obj C} →  Iso C ( I □ a)  a 
      mρ-iso : {a : Obj C} →  Iso C ( a □ I)  a 
      mα→nat1 : {a a' b c : Obj C} →  ( f : Hom C a a' ) →
         C [ C [ ( f ■ id1 C ( b □ c ))  o ≅→ (mα-iso {a} {b} {c}) ]  ≈
            C [   ≅→ (mα-iso )  o ( (f ■ id1 C b ) ■ id1 C c )    ] ]
      mα→nat2 : {a b b' c : Obj C} →  ( f : Hom C b b' ) →
         C [ C [ ( id1 C a ■ ( f ■ id1 C c ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
            C [   ≅→ (mα-iso )  o ( (id1 C a ■ f )  ■ id1 C c ) ] ]
      mα→nat3 : {a b c c' : Obj C} →  ( f : Hom C c c' ) →
         C [ C [ ( id1 C a ■ ( id1 C b ■ f ) ) o ≅→ (mα-iso {a} {b} {c} ) ]  ≈
            C [   ≅→ (mα-iso )  o ( id1 C ( a □ b ) ■ f ) ] ]
      mλ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
         C [ C [ f o ≅→ (mλ-iso {a} ) ]  ≈
            C [   ≅→ (mλ-iso )  o ( id1 C I  ■ f )    ] ]
      mρ→nat : {a a' : Obj C} →  ( f : Hom C a a' ) →
         C [ C [ f o ≅→ (mρ-iso {a} ) ]  ≈
            C [   ≅→ (mρ-iso )  o ( f ■ id1 C I  )    ] ]
      -- we should write naturalities for ≅← (maybe derived from above )
  αABC□1D : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ (b □ c)) □ d)
  αABC□1D {a} {b} {c} {d} {e} = (  ≅→ mα-iso  ■ id1 C d )
  αAB□CD : {a b c d e : Obj C } → Hom C  ((a □ (b □ c)) □ d) (a □ ((b □ c ) □ d))
  αAB□CD {a} {b} {c} {d} {e} =   ≅→ mα-iso
  1A□BCD : {a b c d e : Obj C } → Hom C  (a □ ((b □ c ) □ d)) (a □ (b □ ( c □ d) ))
  1A□BCD {a} {b} {c} {d} {e} = ( id1 C a ■   ≅→ mα-iso )
  αABC□D : {a b c d e : Obj C } → Hom C  (a □ (b □ ( c □ d) )) ((a □ b ) □ (c □ d))
  αABC□D {a} {b} {c} {d} {e} =  ≅← mα-iso  
  αA□BCD : {a b c d e : Obj C } → Hom C (((a □ b) □ c ) □ d) ((a □ b ) □ (c □ d))
  αA□BCD {a} {b} {c} {d} {e} =  ≅→ mα-iso  
  αAIB :  {a b  : Obj C } →  Hom C (( a □ I ) □ b ) (a □ ( I □ b ))
  αAIB {a} {b} = ≅→ mα-iso
  1A□λB : {a b  : Obj C } →  Hom C  (a □ ( I □ b )) ( a □ b )
  1A□λB {a} {b} =  id1 C a ■  ≅→ mλ-iso 
  ρA□IB : {a b  : Obj C } →  Hom C  (( a □ I ) □ b ) ( a □ b )
  ρA□IB {a} {b} = ≅→  mρ-iso  ■  id1 C b

  field
      comm-penta : {a b c d e : Obj C}
         → C [ C [ αABC□D {a} {b} {c} {d} {e} o  C [ 1A□BCD {a} {b} {c} {d} {e} o C [ αAB□CD {a} {b} {c} {d} {e} o αABC□1D {a} {b} {c} {d} {e} ] ] ]
             ≈ αA□BCD {a} {b} {c} {d} {e} ]
      comm-unit : {a b : Obj C}
         → C [ C [ 1A□λB {a} {b} o  αAIB ] ≈ ρA□IB {a} {b} ]

record Monoidal  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) 
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  field
      m-i : Obj C
      m-bi : Functor ( C × C ) C 
      isMonoidal : IsMonoidal C m-i m-bi

---------
--
--  Lax Monoidal Functor
--
--    N → M
--
---------

---------
--
-- Two implementations of Functor ( C × C ) → D from F : Functor C → D (given)
--        dervied from F and two Monoidal Categories
--
--     F x ● F y
--     F ( x ⊗  y )
--
-- and a given natural transformation for them 
--
--      φ : F x ● F y  → F ( x ⊗  y )
--
--      TMap φ : ( x y : Obj C ) →  Hom D ( F x ● F y ) ( F ( x ⊗ y ))
--
-- a given unit arrow
--
--      ψ : IN → IM

Functor● :  {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( N : Monoidal D )
      ( MF :   Functor C D ) →  Functor ( C × C ) D
Functor● C D N MF =  record {
       FObj = λ x  → (FObj MF (proj₁ x) ) ●  (FObj MF (proj₂ x) )
     ; FMap = λ {x : Obj ( C × C ) } {y} f →  (  FMap MF  (proj₁  f ) ■ FMap MF (proj₂ f)  )
     ; isFunctor = record {
             ≈-cong   = ≈-cong
             ; identity = identity
             ; distr    = distr
     }
    } where
  _●_ : (x y : Obj D ) → Obj D
  _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
  _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d )
  _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
  F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b )
  F f = FMap MF f
  ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
        D [  (F (proj₁ f) ■ F (proj₂ f)) ≈  (F (proj₁ g) ■ F (proj₂ g)) ]
  ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning D in begin
        F (proj₁ f) ■ F (proj₂ f)
     ≈⟨ fcong (Monoidal.m-bi N) (  fcong MF (  proj₁ f≈g ) , fcong MF ( proj₂ f≈g ))  ⟩
        F (proj₁ g) ■ F (proj₂ g)
     ∎ 
  identity : {a : Obj (C × C)} → D [  (F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a)))
        ≈ id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a)) ]
  identity {a} =   let open ≈-Reasoning D in begin
         F (proj₁ (id1 (C × C) a)) ■ F (proj₂ (id1 (C × C) a))
     ≈⟨ fcong  (Monoidal.m-bi N) (  IsFunctor.identity (isFunctor MF )  ,  IsFunctor.identity (isFunctor MF ))  ⟩
         id1 D (FObj MF (proj₁ a)) ■ id1 D (FObj MF (proj₂ a))
     ≈⟨ IsFunctor.identity (isFunctor  (Monoidal.m-bi N)) ⟩
        id1 D (FObj MF (proj₁ a) ● FObj MF (proj₂ a))
     ∎
  distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} →
     D [  (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ])))
       ≈ D [  (F (proj₁ g) ■ F (proj₂ g)) o  (F (proj₁ f) ■ F (proj₂ f)) ] ]
  distr {a} {b} {c} {f} {g} =  let open ≈-Reasoning D in begin
        (F (proj₁ ((C × C) [ g o f ])) ■ F (proj₂ ((C × C) [ g o f ])))
     ≈⟨ fcong (Monoidal.m-bi N) (  IsFunctor.distr ( isFunctor  MF) ,  IsFunctor.distr ( isFunctor MF )) ⟩
         ( F (proj₁ g)  o F (proj₁ f) ) ■ (  F (proj₂ g) o F (proj₂ f)  )
     ≈⟨ IsFunctor.distr ( isFunctor  (Monoidal.m-bi N)) ⟩
        (F (proj₁ g) ■ F (proj₂ g)) o  (F (proj₁ f) ■ F (proj₂ f))
     ∎

Functor⊗ :  {c₁ c₂ ℓ : Level} (C D : Category c₁ c₂ ℓ) ( M : Monoidal C ) 
      ( MF :   Functor C D ) →  Functor ( C × C ) D
Functor⊗ C D M MF =  record {
       FObj = λ x → FObj MF ( proj₁ x ⊗ proj₂ x )
     ; FMap = λ {a} {b} f →  F ( proj₁ f □ proj₂ f )
     ; isFunctor = record {
             ≈-cong   = ≈-cong
             ; identity = identity
             ; distr    = distr
     }
    } where
  _⊗_ : (x y : Obj C ) → Obj C
  _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
  _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
  _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
  F : { a b : Obj C } → ( f : Hom C a b ) → Hom D (FObj MF a) (FObj MF b )
  F f = FMap MF f
  ≈-cong : {a b : Obj (C × C)} {f g : Hom (C × C) a b} → (C × C) [ f ≈ g ] →
     D [ F ( (proj₁ f □ proj₂ f)) ≈ F ( (proj₁ g □ proj₂ g)) ]
  ≈-cong {a} {b} {f} {g} f≈g = IsFunctor.≈-cong (isFunctor MF ) ( IsFunctor.≈-cong (isFunctor  (Monoidal.m-bi M) ) f≈g  )
  identity : {a : Obj (C × C)} → D [ F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a)))
      ≈ id1 D (FObj MF (proj₁ a ⊗ proj₂ a)) ]
  identity {a} = let open ≈-Reasoning D in begin
        F ( (proj₁ (id1 (C × C) a) □ proj₂ (id1 (C × C) a)))
     ≈⟨⟩
        F (FMap (Monoidal.m-bi M) (id1 (C × C) a ) )
     ≈⟨ fcong MF ( IsFunctor.identity (isFunctor (Monoidal.m-bi M) )) ⟩
        F (id1 C (proj₁ a ⊗ proj₂ a))
     ≈⟨ IsFunctor.identity (isFunctor MF) ⟩
        id1 D (FObj MF (proj₁ a ⊗ proj₂ a))
     ∎
  distr : {a b c : Obj (C × C)} {f : Hom (C × C) a b} {g : Hom (C × C) b c} → D [
        F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ])))
    ≈ D [ F ( (proj₁ g □ proj₂ g)) o F ( (proj₁ f □ proj₂ f)) ] ]
  distr {a} {b} {c} {f} {g} =  let open ≈-Reasoning D in begin
        F ( (proj₁ ((C × C) [ g o f ]) □ proj₂ ((C × C) [ g o f ])))
     ≈⟨⟩
        F (FMap (Monoidal.m-bi M) ( (C × C)  [ g o f ] ))
     ≈⟨ fcong MF ( IsFunctor.distr (isFunctor (Monoidal.m-bi M))) ⟩
        F (C [ FMap (Monoidal.m-bi M) g o FMap (Monoidal.m-bi M) f ])
     ≈⟨ IsFunctor.distr ( isFunctor MF ) ⟩
        F ( proj₁ g □ proj₂ g) o F ( proj₁ f □ proj₂ f) 
     ∎


record IsMonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
      ( MF :   Functor C D )
      ( ψ  :  Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) ) )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  _⊗_ : (x y : Obj C ) → Obj C
  _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
  _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d )
  _□_ f g = FMap (Monoidal.m-bi M) ( f , g )
  _●_ : (x y : Obj D ) → Obj D
  _●_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal N) ) x y
  _■_ : {a b c d : Obj D } ( f : Hom D a c ) ( g : Hom D b d ) → Hom D ( a ● b ) ( c ● d )
  _■_ f g = FMap (Monoidal.m-bi N) ( f , g )
  F● :  Functor ( C × C ) D
  F●  =  Functor●  C D N MF
  F⊗ : Functor ( C × C ) D
  F⊗  =  Functor⊗  C D M MF
  field
      φab :  NTrans  ( C × C ) D  F● F⊗ 
  open Iso
  open Monoidal
  open IsMonoidal hiding ( _■_ ;  _□_ )
  αC :  {a b c : Obj C} → Hom C (( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
  αC {a} {b} {c} =  ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) 
  αD :  {a b c : Obj D} → Hom D (( a ● b ) ● c ) ( a ● ( b ● c ) )
  αD {a} {b} {c} =  ≅→ (mα-iso (isMonoidal N) {a} {b} {c}) 
  F : Obj C → Obj D
  F x = FObj MF x
  φ : ( x y : Obj C ) →  Hom D ( FObj  F● (x , y) ) ( FObj F⊗ ( x , y ))
  φ x y = NTrans.TMap φab ( x , y )
  1●φBC :  {a b c : Obj C} → Hom D  ( F a ● ( F b ● F c ) ) ( F a ● ( F ( b ⊗ c ) ))
  1●φBC {a} {b} {c} =  id1 D (F a) ■  φ b c
  φAB⊗C :  {a b c : Obj C} → Hom D  ( F a ● ( F ( b ⊗ c ) )) (F ( a  ⊗ ( b  ⊗ c )))
  φAB⊗C {a} {b} {c} =   φ  a  (b ⊗ c )
  φAB●1 :  {a b c : Obj C} → Hom D  ( ( F a ●  F b ) ● F c ) ( F ( a ⊗ b ) ● F c )
  φAB●1 {a} {b} {c} =  φ a b ■ id1 D (F c)
  φA⊗BC :  {a b c : Obj C} → Hom D  ( F ( a ⊗ b ) ● F c ) (F ( (a  ⊗  b ) ⊗ c ))
  φA⊗BC {a} {b} {c} = φ ( a ⊗ b ) c
  FαC : {a b c : Obj C} → Hom D (F ( (a  ⊗  b ) ⊗ c )) (F ( a  ⊗ ( b  ⊗ c )))
  FαC {a} {b} {c} =  FMap MF ( ≅→ (mα-iso (isMonoidal M) {a} {b} {c}) )
  1●ψ : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a ● F ( Monoidal.m-i M ) )
  1●ψ{a} {b} =  id1 D (F a)  ■  ψ
  φAIC : { a b : Obj C } → Hom D  ( F a ● F ( Monoidal.m-i M ) ) (F ( a  ⊗ Monoidal.m-i M ))
  φAIC {a} {b} = φ a (  Monoidal.m-i M )
  FρC : { a b : Obj C } → Hom D   (F ( a  ⊗ Monoidal.m-i M ))( F a  )
  FρC {a} {b} = FMap MF (  ≅→ (mρ-iso (isMonoidal M) {a} ) )
  ρD : { a b : Obj C } → Hom D (F a  ● Monoidal.m-i N ) ( F a  )
  ρD {a} {b} =  ≅→ (mρ-iso (isMonoidal N) {F a} )
  ψ●1 : { a b : Obj C } → Hom D (Monoidal.m-i N ● F b  ) ( F ( Monoidal.m-i M )  ● F b  )
  ψ●1 {a} {b} =  ψ ■ id1 D (F b)
  φICB : { a b : Obj C } → Hom D  ( F ( Monoidal.m-i M )  ● F b  ) ( F (  ( Monoidal.m-i M )  ⊗ b ) )
  φICB {a} {b} = φ  ( Monoidal.m-i M ) b
  FλD : { a b : Obj C } → Hom D  ( F (  ( Monoidal.m-i M )  ⊗ b ) ) (F b ) 
  FλD {a} {b} = FMap MF ( ≅→ (mλ-iso (isMonoidal M) {b} ) )
  λD : { a b : Obj C } → Hom D  (Monoidal.m-i N ● F b  )  (F b ) 
  λD {a} {b} = ≅→ (mλ-iso (isMonoidal N) {F b} )
  field
     associativity : {a b c : Obj C } → D [ D [ φAB⊗C {a} {b} {c} o D [ 1●φBC o αD ] ]  ≈ D [ FαC  o  D [ φA⊗BC o φAB●1 ] ] ]
     unitarity-idr : {a b : Obj C } → D [ D [ FρC  {a} {b}  o D [ φAIC {a} {b} o  1●ψ{a} {b} ] ]  ≈ ρD {a} {b}  ]
     unitarity-idl : {a b : Obj C } → D [ D [ FλD  {a} {b}  o D [ φICB {a} {b} o  ψ●1 {a} {b} ] ]  ≈ λD {a} {b}  ]

record MonoidalFunctor {c₁ c₂ ℓ : Level} {C D : Category c₁ c₂ ℓ}  ( M : Monoidal C ) ( N : Monoidal D )
        : Set ( suc  (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where
  field
      MF : Functor C D
      ψ  : Hom D (Monoidal.m-i N)  (FObj MF (Monoidal.m-i M) )
      isMonodailFunctor : IsMonoidalFunctor  M N MF ψ

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.Product as a Tensor Product for Monoidal Category
--

SetsTensorProduct : {c : Level} → Functor ( Sets {c} × Sets {c} )  (Sets {c})
SetsTensorProduct =   record {
       FObj = λ x  →  proj₁ x  *  proj₂ x
     ; FMap = λ {x : Obj ( Sets × Sets ) } {y} f → map (proj₁ f)  (proj₂ f)
     ; isFunctor = record {
             ≈-cong   = ≈-cong 
             ; identity = refl
             ; distr    = refl
     }
    } where
        ≈-cong : {a b : Obj (Sets × Sets)} {f g : Hom (Sets × Sets) a b} →
                (Sets × Sets) [ f ≈ g ] → Sets [ map (proj₁ f) (proj₂ f) ≈ map (proj₁ g) (proj₂ g) ]
        ≈-cong (refl , refl) =  refl

-----
--
-- Sets as Monoidal Category
--
--  almost all comutativities are refl
--
--
--

data One {c : Level} : Set c where
  OneObj : One   -- () in Haskell ( or any one object set )

MonoidalSets : {c : Level} → Monoidal (Sets {c})
MonoidalSets {c} = record {
      m-i = One {c} ;
      m-bi = SetsTensorProduct  ;
      isMonoidal = record {
              mα-iso  =  record { ≅→  =  mα→ ; ≅← =  mα← ; iso→  = refl ; iso← = refl } ;
              mλ-iso  =  record { ≅→  =  mλ→ ; ≅← =  mλ← ; iso→  = extensionality Sets ( λ x → mλiso x ) ; iso← = refl } ;
              mρ-iso  =  record { ≅→  =  mρ→ ; ≅← =  mρ← ; iso→  = extensionality Sets ( λ x → mρiso x ) ; iso← = refl } ;
              mα→nat1  = λ f → refl  ;
              mα→nat2  =  λ f → refl  ;
              mα→nat3  =  λ f → refl  ;
              mλ→nat  =  λ f → refl  ;
              mρ→nat  =  λ f → refl  ;
              comm-penta  = refl ;
              comm-unit  = refl
      }
   } where
       _⊗_ : ( a b : Obj Sets ) → Obj Sets
       _⊗_ a b = FObj SetsTensorProduct (a , b )
       --  association operations
       mα→ : {a b c : Obj Sets} →  Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
       mα→ ((a , b) , c ) =  (a , ( b , c ) )
       mα← : {a b c : Obj Sets} →  Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c )
       mα← (a , ( b , c ) ) =  ((a , b) , c )
       --  (One , a) ⇔ a 
       mλ→ : {a  : Obj Sets} →  Hom Sets ( One ⊗ a ) a
       mλ→ (_ , a) =  a
       mλ← : {a  : Obj Sets} →  Hom Sets  a ( One ⊗ a )
       mλ←  a = ( OneObj , a )
       mλiso : {a : Obj Sets} (x : One ⊗ a) →  (Sets [ mλ← o mλ→ ]) x ≡ id1 Sets (One ⊗ a) x
       mλiso (OneObj , _ ) = refl
       --  (a , One) ⇔ a 
       mρ→ : {a  : Obj Sets} →  Hom Sets ( a ⊗ One )  a
       mρ→ (a , _) =  a
       mρ← : {a  : Obj Sets} →  Hom Sets a ( a ⊗ One ) 
       mρ←  a = ( a , OneObj )
       mρiso : {a : Obj Sets} (x : a ⊗ One ) →  (Sets [ mρ← o mρ→ ]) x ≡ id1 Sets (a ⊗ One) x
       mρiso (_ , OneObj ) = refl

≡-cong = Relation.Binary.PropositionalEquality.cong 


record IsHaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
      ( unit  : FObj F One )
      ( φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) ) )
        : Set (suc (suc c₁)) where
  isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct  
  isM = Monoidal.isMonoidal MonoidalSets 
  open IsMonoidal
  field
          natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
             → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
          assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
             → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c))
          idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
          idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x

--   http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
-- naturality of φ       fmap(f × g)(φ u v) = φ ( fmap f u) ( fmap g v )
-- left identity         fmap snd (φ unit v) = v
-- right identity        fmap fst (φ u unit) = u
-- associativity         fmap assoc  (φ u (φ v w)) = φ (φ u v) w


record HaskellMonoidalFunctor {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
        : Set (suc (suc c₁)) where
  field
      unit  : FObj F One
      φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )

HaskellMonoidalFunctor→MonoidalFunctor :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : HaskellMonoidalFunctor F )
   → IsHaskellMonoidalFunctor F ( HaskellMonoidalFunctor.unit mf ) ( HaskellMonoidalFunctor.φ mf ) 
   → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
HaskellMonoidalFunctor→MonoidalFunctor {c} F mf ismf = record {
      MF = F
    ; ψ  = λ _ → HaskellMonoidalFunctor.unit mf
    ; isMonodailFunctor = record {
             φab  = record { TMap = λ x →  φ ; isNTrans = record { commute = comm0 } }
         ;   associativity  = λ {a b c} → comm1 {a} {b} {c}
         ;   unitarity-idr = λ {a b} → comm2 {a} {b}
         ;   unitarity-idl = λ {a b} → comm3 {a} {b}
      }
  } where
      open Monoidal 
      open IsMonoidal hiding ( _■_ ;  _□_ )
      M : Monoidal (Sets {c})
      M = MonoidalSets
      isM  : IsMonoidal (Sets {c}) One SetsTensorProduct  
      isM = Monoidal.isMonoidal MonoidalSets 
      unit : FObj F One
      unit = HaskellMonoidalFunctor.unit mf
      _⊗_ : (x y : Obj Sets ) → Obj Sets
      _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
      _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
      _□_ f g = FMap (m-bi M) ( f , g )
      φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
      φ z = HaskellMonoidalFunctor.φ mf z
      comm00 : {a b :  Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b}  (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
         (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
      comm00 {a} {b} {(f , g)} (x , y) = begin
                 (FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) (φ  (x , y))
             ≡⟨⟩
                 (FMap F ( f □ g ) ) (φ  (x , y))
             ≡⟨⟩
                 FMap F ( map f g ) (φ  (x , y))
             ≡⟨ IsHaskellMonoidalFunctor.natφ ismf ⟩
                 φ (  FMap F  f x , FMap F g  y )
             ≡⟨⟩
                 φ ( (  FMap F  f □ FMap F g ) (x , y) )
             ≡⟨⟩
                 φ ((FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) (x , y) )
             ∎ 
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ  ]
        ≈ Sets [ φ  o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
      comm0 {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
      comm10 :  {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ  o Sets [ id1 Sets (FObj F a) □ φ  o Iso.≅→ (mα-iso isM) ] ]) x ≡
                (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o φ  □ id1 Sets (FObj F c) ] ]) x
      comm10 {x} {y} {f} ((a , b) , c ) = begin
                  φ  (( id1 Sets (FObj F x) □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
               ≡⟨⟩
                  φ  ( a , φ  (b , c)) 
               ≡⟨ IsHaskellMonoidalFunctor.assocφ ismf ⟩
                 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  (a , b)) , c ))
               ≡⟨⟩
                 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  □  id1 Sets (FObj F f) ) ((a , b) , c)))
             ∎
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ 
           o Sets [  (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
        ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o  (φ  □ id1 Sets (FObj F c)) ] ] ]
      comm1 {a} {b} {c} =  extensionality Sets ( λ x  → comm10 x )
      comm20 : {a b : Obj Sets} ( x : FObj F a * One )  → (  Sets [
         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x  ≡ Iso.≅→ (mρ-iso isM) x
      comm20 {a} {b} (x , OneObj ) =  begin 
                 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ  ( x , unit ) )
               ≡⟨ IsHaskellMonoidalFunctor.idrφ ismf ⟩
                 x
               ≡⟨⟩
                 Iso.≅→ (mρ-iso isM) ( x , OneObj )
             ∎ 
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm2 : {a b : Obj Sets} → Sets [ Sets [
         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
      comm2 {a} {b} =  extensionality Sets ( λ x  → comm20 {a} {b} x )
      comm30 : {a b : Obj Sets} ( x : One * FObj F b )  → (  Sets [
         FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ  o
             FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x  ≡ Iso.≅→ (mλ-iso isM) x
      comm30 {a} {b} ( OneObj , x) =  begin 
                 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ  ( unit , x ) )
               ≡⟨ IsHaskellMonoidalFunctor.idlφ ismf ⟩
                 x
               ≡⟨⟩
                 Iso.≅→ (mλ-iso isM) (  OneObj , x )
             ∎ 
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
        Sets [ φ  o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
      comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )


_・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
_・_ f g = λ x → f ( g x ) 

record IsApplicative {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
    ( pure  : {a : Obj Sets} → Hom Sets a ( FObj f a ) )
    ( _<*>_ : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b )
        : Set (suc (suc c₁)) where
  field
          identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a )  <*> u ≡ u
          composition : { a b c : Obj Sets } { u : FObj f ( b → c ) } { v : FObj f (a → b ) } { w : FObj f a }
              → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
          homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
          interchange : { a b : Obj Sets } { u : FObj f ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
          --  from  http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf

record Applicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
        : Set (suc (suc c₁)) where
  field
      pure  : {a : Obj Sets} → Hom Sets a ( FObj F a )
      <*>   : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b

------
--
--  Applicative ⇔ Monoidal
--
--

lemma1 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative F → HaskellMonoidalFunctor F
lemma1 F app = record { unit = unit ; φ = φ }
  where
     open Applicative
     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 (FMap F (λ j k → (j , k)) x) y

lemma2 : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor F → Applicative F 
lemma2 F mono = record { pure = pure ; <*> = <*> }
  where
     open HaskellMonoidalFunctor
     pure  :  {a : Obj Sets} → Hom Sets a ( FObj F a )
     pure {a} x = FMap F ( λ y → x ) (unit mono)
     <*> :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b  
     <*> {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ mono ( x , y ))


------
--
-- Appllicative Functor is a Monoidal Functor
--

Applicative→Monoidal :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F )
   → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf ) 
   → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
Applicative→Monoidal {l} F mf ismf = record {
      MF = F
    ; ψ  = λ x → unit
    ; isMonodailFunctor = record {
             φab  = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
         ;   associativity  = λ {a b c} → comm1 {a} {b} {c}
         ;   unitarity-idr = λ {a b} → comm2 {a} {b}
         ;   unitarity-idl = λ {a b} → comm3 {a} {b}
      }
  } where
      open Monoidal 
      open IsMonoidal hiding ( _■_ ;  _□_ )
      M = MonoidalSets
      isM = Monoidal.isMonoidal MonoidalSets 
      unit = Applicative.pure mf OneObj
      _⊗_ : (x y : Obj Sets ) → Obj Sets
      _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
      _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
      _□_ f g = FMap (m-bi M) ( f , g )
      φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
      φ x = Applicative.<*> mf  (FMap F (λ j k → (j , k))  (proj₁ x )) (proj₂ x)
      _<*>_ :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b  
      _<*>_  = Applicative.<*> mf  
      left  :   {a b : Obj Sets} → {x y : FObj F ( a → b )} → {h : FObj F a  } → ( x ≡ y ) → x <*> h ≡ y <*> h
      left {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k <*> h ) eq 
      right  :   {a b : Obj Sets} → {h : FObj F ( a → b )} → {x y : FObj F a  } → ( x ≡ y ) → h <*> x ≡ h <*> y
      right {_} {_} {h} {_} {_} eq = ≡-cong ( λ k → h <*> k ) eq 
      id : { a : Obj Sets } → a → a 
      id x = x
      pure : {a : Obj Sets } → Hom Sets a ( FObj F a )
      pure a = Applicative.pure mf a
      -- special case
      F→pureid : {a b : Obj Sets } → (x : FObj F a ) →  FMap F id x ≡ pure id <*> x
      F→pureid {a} {b} x = sym ( begin
                 pure id <*> x
             ≡⟨ IsApplicative.identity ismf  ⟩
                 x
             ≡⟨ ≡-cong ( λ k → k x ) (sym ( IsFunctor.identity (isFunctor F ) )) ⟩ FMap F id x
             ∎ )
           where
                  open Relation.Binary.PropositionalEquality
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      -----
      -- they say it is not possible to prove FreeTheorem in Agda nor Coq
      --    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
      -- so we postulate this
      --    and we cannot indent postulate ...
      postulate FreeTheorem : {l : Level } {a b c : Obj (Sets {l}) } → (F : Functor (Sets {l}) (Sets {l} ) ) →  ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) ) →  {h f : Hom Sets a b } →  {g k : Hom Sets b c } →  Sets [  g o h  ≈  k o f  ] →  Sets [ FMap F g o fmap h  ≈  fmap k o FMap F f  ]
      UniquenessOfFunctor :   (F : Functor Sets Sets)
          {a b : Obj Sets } { f : Hom Sets a b } → ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) )
              → ( {b : Obj Sets } → Sets [ fmap  (id1 Sets b) ≈  id1 Sets (FObj F b) ] )
              → Sets [ fmap f ≈  FMap F f ]
      UniquenessOfFunctor F {a} {b} {f} fmap eq = begin
                fmap f 
             ≈↑⟨ idL ⟩
                id1 Sets (FObj F b)  o  fmap f 
             ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
                FMap F (id1 Sets b)  o  fmap f 
             ≈⟨ FreeTheorem F  fmap refl-hom ⟩ 
                fmap  (id1 Sets b)  o  FMap F f  
             ≈⟨ car eq ⟩
                id1 Sets (FObj F b)  o  FMap F f  
             ≈⟨ idL ⟩
                FMap F f 
             ∎  
           where open ≈-Reasoning Sets hiding ( _o_ )
      F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } →  FMap F f x ≡ pure f <*> x
      F→pure {a} {b} {f} {x} = sym ( begin
                 pure f <*> x
             ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x →  IsApplicative.identity ismf  ))) ⟩
                 FMap F f x
             ∎ )
           where
                  open Relation.Binary.PropositionalEquality
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      p*p : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
      p*p =  IsApplicative.homomorphism ismf
      comp = IsApplicative.composition ismf
      inter = IsApplicative.interchange ismf
      pureAssoc :  {a b c : Obj Sets } ( f : b → c ) ( g : a → b ) ( h : FObj F a ) → pure f <*> ( pure g <*> h ) ≡ pure ( f ・ g ) <*> h
      pureAssoc f g h = trans ( trans (sym comp) (left (left p*p) )) ( left p*p  )
           where
                  open Relation.Binary.PropositionalEquality
      comm00 : {a b :  Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b}  (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
         (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
      comm00 {a} {b} {(f , g)} (x , y) = begin
                 ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) )
             ≡⟨⟩
                 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y)
             ≡⟨⟩
                 FMap F (map f g) ((FMap F (λ j k → j , k) x) <*> y)
             ≡⟨ F→pure  ⟩
                 (pure (map f g) <*> (FMap F (λ j k → j , k) x <*> y))
             ≡⟨ right ( left F→pure )  ⟩
                 (pure (map f g)) <*> ((pure (λ j k → j , k) <*> x) <*> y)
             ≡⟨ sym ( IsApplicative.composition ismf )  ⟩
                 (( pure _・_ <*> (pure (map f g))) <*> (pure (λ j k → j , k) <*> x)) <*> y
             ≡⟨ left ( sym ( IsApplicative.composition ismf ))  ⟩
                 ((( pure _・_ <*> (( pure _・_ <*> (pure (map f g))))) <*> pure (λ j k → j , k)) <*> x) <*> y
             ≡⟨ trans ( trans (left ( left (left (right  p*p )))) ( left ( left ( left p*p)))) (left (left p*p)) ⟩
                 (pure (( _・_ (( _・_ ((map f g))))) (λ j k → j , k)) <*> x) <*> y
             ≡⟨⟩
                (pure (λ j k → f j , g k) <*> x) <*> y
             ≡⟨⟩
                 ( pure ((_・_ (( _・_ ( ( λ h → h g ))) ( _・_ ))) ((λ j k → f j , k))) <*> x ) <*> y 
             ≡⟨ sym ( trans (left (left (left p*p))) (left ( left p*p)) ) ⟩
                ((((pure _・_ <*> pure ((λ h → h g) ・ _・_)) <*> pure (λ j k → f j , k)) <*> x) <*> y)
             ≡⟨ sym (trans ( left ( left ( left (right (left p*p) )))) (left ( left  (left (right p*p ))))) ⟩
                 (((pure  _・_ <*> (( pure  _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ ))) <*> (pure (λ j k → f j , k))) <*> x ) <*> y 
             ≡⟨ left ( ( IsApplicative.composition ismf ))  ⟩
                 ((( pure  _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ )) <*> (pure (λ j k → f j , k) <*> x )) <*> y 
             ≡⟨  left (IsApplicative.composition ismf )  ⟩
                 ( pure ( λ h → h g ) <*> ( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) ) <*> y 
             ≡⟨ left (sym (IsApplicative.interchange ismf )) ⟩
                 (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*>  pure g) <*> y 
             ≡⟨  IsApplicative.composition ismf ⟩
                 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y)
             ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩
                 (FMap F (λ j k → f j , k)  x) <*> (FMap F g y)
             ≡⟨  ≡-cong ( λ k → k  x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F ))  ⟩
                 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y)
             ≡⟨⟩
                 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
             ∎ 
           where
                  open Relation.Binary.PropositionalEquality
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ  ]
        ≈ Sets [ φ  o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
      comm0 {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
      comm10 :  {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ  o Sets [ id1 Sets (FObj F a) □ φ  o Iso.≅→ (mα-iso isM) ] ]) x ≡
                (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o φ  □ id1 Sets (FObj F c) ] ]) x
      comm10 {x} {y} {f} ((a , b) , c ) = begin
                  φ  (( id □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
               ≡⟨⟩
                 (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c)
               ≡⟨ trans (left  F→pure) (right (left F→pure) )  ⟩
                 (pure (λ j k → j , k) <*> a) <*> ( (pure (λ j k → j , k) <*> b) <*> c)
               ≡⟨ sym comp ⟩
                  ( ( pure _・_ <*> (pure (λ j k → j , k) <*> a)) <*>  (pure (λ j k → j , k) <*> b)) <*> c
               ≡⟨ sym ( left comp ) ⟩
                  (( (  pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*>  (pure (λ j k → j , k))) <*> b) <*> c
               ≡⟨ sym ( left ( left ( left (right comp )))) ⟩
                  (( (  pure _・_ <*> (( (pure _・_ <*> pure _・_ ) <*> (pure (λ j k → j , k))) <*> a)) <*>  (pure (λ j k → j , k))) <*> b) <*> c
               ≡⟨ trans (left ( left (left ( right (left ( left p*p )))))) (left ( left ( left (right (left p*p))))) ⟩
                  (( (  pure _・_ <*> ((pure ((_・_ ( _・_ )) ((λ j k → j , k)))) <*> a)) <*>  (pure (λ j k → j , k))) <*> b) <*> c
               ≡⟨ sym (left ( left ( left comp ) )) ⟩
                  (((( ( pure _・_  <*> (pure _・_ )) <*> (pure ((_・_ ( _・_ )) ((λ j k → j , k))))) <*> a) <*>  (pure (λ j k → j , k))) <*> b) <*> c
               ≡⟨  trans (left ( left ( left (left (left p*p))))) (left ( left ( left (left p*p ))))  ⟩
                  ((((pure ( ( _・_  (_・_ )) (((_・_ ( _・_ )) ((λ j k → j , k)))))) <*> a) <*>  (pure (λ j k → j , k))) <*> b) <*> c
               ≡⟨⟩
                  ((((pure (λ f g x y → f , g x y)) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c
               ≡⟨ left ( left inter )  ⟩
                  (((pure (λ f → f (λ j k → j , k))) <*> ((pure (λ f g x y → f , g x y)) <*> a) ) <*> b) <*> c
               ≡⟨ sym ( left ( left comp )) ⟩
                  ((((   pure _・_   <*>  (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c
               ≡⟨ trans (left ( left (left (left p*p) ))) (left (left (left p*p ) )) ⟩
                  ((pure ((   _・_  (λ f → f (λ j k → j , k))) (λ f g x y → f , g x y)) <*> a ) <*> b) <*> c
               ≡⟨⟩
                   (((pure (λ f g h → f , g , h)) <*> a) <*> b) <*> c
               ≡⟨⟩
                    ((pure ((_・_  ((_・_  ((_・_   ( (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) 
                          (( _・_  ( _・_  ((λ j k → j , k)))) (λ j k → j , k))) <*> a) <*> b) <*> c
               ≡⟨ sym (trans ( left ( left ( left (left (right (right p*p))) ) )) (trans (left (left( left (left (right p*p)))))
                       (trans (left (left (left (left p*p)))) (trans ( left (left (left (right (left (right p*p ))))))
                       (trans (left (left (left (right (left p*p))))) (trans (left (left (left (right p*p)))) (left (left (left p*p)))) ) ) )
                        ) ) ⟩
                    ((((pure _・_   <*> ((pure _・_   <*> ((pure _・_   <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) <*>
                          (( pure _・_  <*> ( pure _・_  <*>  (pure (λ j k → j , k)))) <*> pure (λ j k → j , k))) <*> a) <*> b) <*> c
               ≡⟨ left (left comp )  ⟩
                    (((pure _・_   <*> ((pure _・_   <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))) <*>
                          ((( pure _・_  <*> ( pure _・_  <*>  (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a)) <*> b) <*> c
               ≡⟨ left comp ⟩
                    ((pure _・_   <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
                          (((( pure _・_  <*> ( pure _・_  <*>  (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a) <*> b)) <*> c
               ≡⟨ left ( right (left comp )) ⟩
                    ((pure _・_   <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
                          ((( pure _・_  <*>  (pure (λ j k → j , k))) <*> (pure (λ j k → j , k) <*> a)) <*> b)) <*> c
               ≡⟨ left ( right comp ) ⟩
                    ((pure _・_   <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
                            (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b))) <*> c
               ≡⟨ comp ⟩
                  pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) <*> ( (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b)) <*> c)
               ≡⟨ sym ( trans ( trans F→pure (right (left F→pure ))) ( right ( left (right (left F→pure ))))) ⟩
                  FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) ( (FMap F (λ j k → j , k) ( (FMap F (λ j k → j , k) a) <*> b)) <*> c)
               ≡⟨⟩
                 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ  □  id1 Sets (FObj F f) ) ((a , b) , c)))
             ∎
           where
                  open Relation.Binary.PropositionalEquality
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ 
           o Sets [  (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
        ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o  (φ  □ id1 Sets (FObj F c)) ] ] ]
      comm1 {a} {b} {c} =  extensionality Sets ( λ x  → comm10 x )
      comm20 : {a b : Obj Sets} ( x : FObj F a * One )  → (  Sets [
         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x  ≡ Iso.≅→ (mρ-iso isM) x
      comm20 {a} {b} (x , OneObj ) =  begin 
                 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ((  FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
               ≡⟨⟩
                 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (pure OneObj))
               ≡⟨ ≡-cong ( λ k → FMap F  proj₁ k) ( IsApplicative.interchange   ismf )  ⟩
                 FMap F proj₁ ((pure (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x))
               ≡⟨ ( trans  F→pure (right  ( right F→pure )) ) ⟩
                 pure proj₁ <*> ((pure (λ f → f OneObj)) <*> (pure (λ j k → j , k) <*> x))
               ≡⟨ sym ( right comp ) ⟩
                 pure proj₁ <*> (((pure _・_   <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x)
               ≡⟨ sym  comp  ⟩
                 ( ( pure _・_   <*>  (pure proj₁ ) ) <*> ((pure _・_   <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x
               ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) )  ) (left p*p) ⟩
                 pure ( ( _・_ (proj₁ {l} {l})) ((_・_  ((λ f → f OneObj))) (λ j k → j , k))) <*> x
               ≡⟨⟩
                 pure id <*> x
               ≡⟨ IsApplicative.identity ismf  ⟩
                 x
               ≡⟨⟩
                 Iso.≅→ (mρ-iso isM) (x , OneObj)
             ∎ 
           where
                  open Relation.Binary.PropositionalEquality
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm2 : {a b : Obj Sets} → Sets [ Sets [
         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
      comm2 {a} {b} =  extensionality Sets ( λ x  → comm20 {a} {b} x )
      comm30 : {a b : Obj Sets} ( x : One * FObj F b )  → (  Sets [
         FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ  o
             FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x  ≡ Iso.≅→ (mλ-iso isM) x
      comm30 {a} {b} ( OneObj , x) =  begin 
                 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ  ( unit , x ) )
               ≡⟨⟩
                  FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x)
               ≡⟨ ( trans  F→pure (right  ( left F→pure )) ) ⟩
                  pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x)
               ≡⟨ sym comp ⟩
                  ((pure  _・_  <*>  (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x
               ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p)  ⟩
                  pure ((_・_  (proj₂ {l}) )((λ (j : One {l})  (k : b ) → j , k) OneObj)) <*> x
               ≡⟨⟩
                 pure id <*> x
               ≡⟨ IsApplicative.identity ismf  ⟩
                 x
               ≡⟨⟩
                 Iso.≅→ (mλ-iso isM) (  OneObj , x )
             ∎ 
           where
                  open Relation.Binary.PropositionalEquality
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
      comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
        Sets [ φ  o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
      comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )

----
--
-- Monoidal laws imples Applicative laws
--

HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
      ( unit  : FObj F One )
      ( φ    : {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) ) )
      ( mono : IsHaskellMonoidalFunctor F unit φ ) 
         → IsApplicative F (λ x →  FMap F ( λ y → x ) unit) (λ x y → FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ ( x , y )))
HaskellMonoidal→Applicative {c₁} F unit φ mono = record {
          identity = identity 
        ; composition = composition
        ; homomorphism = homomorphism
        ; interchange = interchange
        }
     where 
          id : { a : Obj Sets } → a → a 
          id x = x
          isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct  
          isM = Monoidal.isMonoidal MonoidalSets 
          pure  :  {a : Obj Sets} → Hom Sets a ( FObj F a )
          pure {a} x = FMap F ( λ y → x ) (unit )
          _<*>_ :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b        
          _<*>_ {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ ( x , y ))
          -- right does not work right it makes yellows. why?
          -- right : {n : Level} { a b : Set n} → { x y : a } { h : a → b }  → ( x ≡ y ) → h x ≡ h y
          -- right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq 
          left : {n : Level} { a b : Set n} → { x y : a → b } { h : a }  → ( x ≡ y ) → x h ≡ y h
          left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
          open Relation.Binary.PropositionalEquality
          FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d }
              { f : Hom Sets (c * d) e }
                   { x :  FObj F a } { y :  FObj F b }
              →  FMap F f ( φ ( FMap F g x , FMap F h y ) )  ≡  FMap F (  f o map g h ) ( φ ( x , y ) ) 
          FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin
                  FMap F (  f o map g h ) ( φ ( x , y ) ) 
               ≡⟨  ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩
                  FMap F  f (( FMap F ( map g h ) ) ( φ ( x , y )))
               ≡⟨  ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono )  ⟩
                  FMap F f ( φ ( FMap F g x , FMap F h y ) )
             ∎  )
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
          u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u 
          u→F {a} {u} =  sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) )
          φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
          φunitr {a} {u} = sym ( begin 
                  FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
               ≡⟨  ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩
                  FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) )
               ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
                  (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o   (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) )
               ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) ))  ⟩
                  FMap F id ( φ ( unit , u) )
               ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩
                  id ( φ ( unit , u) )
               ≡⟨⟩
                  φ ( unit , u)
             ∎  )
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
          φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
          φunitl {a} {u} = sym ( begin 
                  FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
               ≡⟨  ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩
                  FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) )
               ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
                  (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o   (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) )
               ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) ))  ⟩
                  FMap F id ( φ ( u , unit ) )
               ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩
                  id ( φ ( u , unit ) )
               ≡⟨⟩
                  φ ( u , unit )
             ∎  )
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
          open IsMonoidal
          identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
          identity {a} {u} = begin 
                 pure id <*> u
               ≡⟨⟩
                 ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ (  FMap F ( λ y → id ) unit  , u ) )
               ≡⟨   ≡-cong ( λ k → ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ ( FMap F ( λ y → id ) unit  ,  k  ))) u→F  ⟩
                 ( FMap F ( λ r →  ( proj₁ r )  ( proj₂  r )) ) ( φ (  FMap F ( λ y → id ) unit  , FMap F id u ) )
               ≡⟨ FφF→F ⟩
                   FMap F (λ x → proj₂ x ) (φ (unit , u ) )
               ≡⟨⟩
                   FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
               ≡⟨  IsHaskellMonoidalFunctor.idlφ mono   ⟩
                  u
             ∎ 
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
          composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
              → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
          composition {a} {b} {c} {u} {v} {w} = begin
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w))
                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , k)) , v)) , w))  ) u→F  ⟩
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u )) , v)) , w))
                ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k  , v)) , w))  ) FφF→F ⟩
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , v)) , w))
                ≡⟨  ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w))  ) ) φunitr ⟩
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   ( (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w))
                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   (k u , v)) , w)) )  (sym ( IsFunctor.distr (isFunctor F )))  ⟩
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w))
                ≡⟨⟩
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
                   ( FMap F (λ x g h → x (g h) ) u , v)) , w))
                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( FMap F (λ x g h → x (g h) ) u , k)) , w))   ) u→F  ⟩
                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x g h → x (g h)) u , FMap F id v)) , w))
                ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w))  )  FφF→F  ⟩
                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id) (φ (u , v)) , w))
                ≡⟨⟩
                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w))
                ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k))  ) u→F  ⟩
                     FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w))
                ≡⟨  FφF→F  ⟩
                     FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w))
                ≡⟨⟩
                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w))
                ≡⟨  ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)) )) (sym (IsFunctor.identity (isFunctor F ))) ⟩
                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) )
                ≡⟨  ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F k (φ (φ (u , v) , w)) )  ) (sym (Iso.iso→ (mα-iso isM)))  ⟩
                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F ( (Iso.≅← (mα-iso isM)) o  (Iso.≅→ (mα-iso isM))) (φ (φ (u , v) , w)) )
                ≡⟨  ≡-cong ( λ k →  FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)))) ( IsFunctor.distr (isFunctor F ))  ⟩
                    FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F  (Iso.≅← (mα-iso isM)) ( FMap F  (Iso.≅→ (mα-iso isM)) (φ (φ (u , v) , w)) ))
                ≡⟨ ≡-cong ( λ k →   FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F  (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩
                     FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w))))
                ≡⟨⟩
                     FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) (φ (u , φ (v , w))))
                ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩
                      FMap F (λ y → (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) ((λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) y )) (φ (u , φ (v , w)))
                ≡⟨⟩
                     FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w)))
                ≡⟨⟩
                 FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) (  proj₂ x)))  ( φ ( u , (φ (v , w))))
                ≡⟨ sym FφF→F ⟩
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
                ≡⟨   ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ) (sym u→F ) ⟩
                 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
              ∎ 
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
          homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
          homomorphism {a} {b} {f} {x} = begin
                  pure f <*> pure x
                ≡⟨⟩
                        FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit))
                ≡⟨ FφF→F  ⟩
                        FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x)) (φ (unit , unit))
                ≡⟨⟩
                        FMap F (λ y → f x) (φ (unit , unit))
                ≡⟨ ≡-cong ( λ k →  FMap F (λ y → f x) k ) φunitl ⟩
                        FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit)
                ≡⟨⟩
                        FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit)
                ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F ))) ⟩
                        FMap F (λ y → f x) unit
                ≡⟨⟩
                  pure (f x)
              ∎ 
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning
          interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
          interchange {a} {b} {u} {x} =  begin
                  u <*> pure x 
              ≡⟨⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ y → x) unit))
              ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit))  ) u→F  ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit))
              ≡⟨  FφF→F  ⟩
                   FMap F ((λ r → proj₁ r (proj₂ r)) o map id (λ y → x)) (φ (u , unit))
              ≡⟨⟩
                  FMap F (λ r → proj₁ r x) (φ (u , unit))
              ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₁ r x) k ) φunitl ⟩
                  FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u )
              ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩
                  FMap F (( λ r → proj₁ r x)  o ((Iso.≅← (mρ-iso isM) ))) u
              ≡⟨⟩
                  FMap F (( λ r → proj₂ r x)  o ((Iso.≅← (mλ-iso isM) ))) u
              ≡⟨ left (  IsFunctor.distr (isFunctor F ))  ⟩
                  FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u)
              ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩
                  FMap F (λ r → proj₂ r x) (φ (unit , u))
              ≡⟨⟩
                 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id) (φ (unit , u)) 
              ≡⟨ sym FφF→F ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u))
              ≡⟨  ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩
                  FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , u))
              ≡⟨⟩
                  pure (λ f → f x) <*> u
              ∎
           where
                  open Relation.Binary.PropositionalEquality.≡-Reasoning

--