Mercurial > hg > Members > kono > Proof > category
view monoidal.agda @ 757:a4074765abf8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 15:58:52 +0900 |
| parents | 2439a142aba2 |
| children | 171f5386e87e |
line wrap: on
line source
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 ψ ----- -- 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 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → (F : Functor C D ) → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) → {h f : Hom C a b } → {g k : Hom C b c } → C [ C [ g o h ] ≈ C [ k o f ] ] → D [ D [ FMap F g o fmap h ] ≈ D [ fmap k o FMap F f ] ] UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D) {a b : Obj C } { f : Hom C a b } → ( fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) ) → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] ) → D [ fmap f ≈ FMap F f ] UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin fmap f ≈↑⟨ idL ⟩ id1 D (FObj F b) o fmap f ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩ FMap F (id1 C b) o fmap f ≈⟨ FreeTheorem C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩ fmap (id1 C b) o FMap F f ≈⟨ car eq ⟩ id1 D (FObj F b) o FMap F f ≈⟨ idL ⟩ FMap F f ∎ where open ≈-Reasoning D 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 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 Sets Sets 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