Mercurial > hg > Members > kono > Proof > category

comparison src/applicative.agda @ 1115:5620d4a85069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe rewriting nearly finished
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Jul 2024 11:44:58 +0900
parents 71049ed05151
children
comparison
equal deleted inserted replaced
1114:ce23d2b47c5e 1115:5620d4a85069
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 open import Level 3 open import Level
2 open import Category 4 open import Category
3 module applicative where 5 open import Definitions
6 open Functor
7
8 --
9 -- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem.
10 --
11 -- they say it is not possible to prove FreeTheorem in Agda nor Coq
12 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
13 -- so we postulate this
14
15 module applicative (
16 FT : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C } → FreeTheorem C D {a} {b} {c} )
17 where
18
4 19
5 open import Data.Product renaming (_×_ to _*_) hiding (_<*>_) 20 open import Data.Product renaming (_×_ to _*_) hiding (_<*>_)
6 open import Category.Constructions.Product 21 open import Category.Constructions.Product
7 open import HomReasoning 22 open import HomReasoning
8 open import cat-utility
9 open import Relation.Binary.Core 23 open import Relation.Binary.Core
10 open import Relation.Binary 24 open import Relation.Binary
11 open import monoidal 25 open import monoidal
12 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 26 open import Relation.Binary.PropositionalEquality hiding ( [_] )
13 27
18 -- is a monoidal functor on Sets and it can be constructoed from Haskell monoidal functor and vais versa 32 -- is a monoidal functor on Sets and it can be constructoed from Haskell monoidal functor and vais versa
19 -- 33 --
20 ---- 34 ----
21 35
22 ----- 36 -----
23 --
24 -- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem.
25 --
26 -- they say it is not possible to prove FreeTheorem in Agda nor Coq
27 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
28 -- so we postulate this
29
30 open Functor
31
32 postulate
33 FreeTheorem : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') {a b c : Obj C }
34 → (F : Functor C D )
35 → (fmap : {a : Obj C } {b : Obj C } → Hom C a b → Hom D (FObj F a) ( FObj F b) )
36 → {h f : Hom C a b } → {g k : Hom C b c }
37 → C [ C [ g o h ] ≈ C [ k o f ] ] → D [ D [ FMap F g o fmap h ] ≈ D [ fmap k o FMap F f ] ]
38
39 UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D) 37 UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D)
40 {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) ) 38 {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) )
41 → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] ) 39 → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] )
42 → D [ fmap f ≈ FMap F f ] 40 → D [ fmap f ≈ FMap F f ]
43 UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin 41 UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin
44 fmap f 42 fmap f
45 ≈↑⟨ idL ⟩ 43 ≈↑⟨ idL ⟩
46 id1 D (FObj F b) o fmap f 44 id1 D (FObj F b) o fmap f
47 ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩ 45 ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
48 FMap F (id1 C b) o fmap f 46 FMap F (id1 C b) o fmap f
49 ≈⟨ FreeTheorem C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩ 47 ≈⟨ FT C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩
50 fmap (id1 C b) o FMap F f 48 fmap (id1 C b) o FMap F f
51 ≈⟨ car eq ⟩ 49 ≈⟨ car eq ⟩
52 id1 D (FObj F b) o FMap F f 50 id1 D (FObj F b) o FMap F f
53 ≈⟨ idL ⟩ 51 ≈⟨ idL ⟩
54 FMap F f 52 FMap F f
58 open import Category.Sets 56 open import Category.Sets
59 import Relation.Binary.PropositionalEquality 57 import Relation.Binary.PropositionalEquality
60 58
61 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c 59 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
62 _・_ f g = λ x → f ( g x ) 60 _・_ f g = λ x → f ( g x )
63
64 record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) ) 61 record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
65 ( pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) ) 62 ( pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) )
66 ( _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b ) 63 ( _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b )
67 : Set (suc (suc c₁)) where 64 : Set (suc (suc c₁)) where
68 field 65 field
123 F→pureid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x 120 F→pureid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x
124 F→pureid {a} {b} x = sym ( begin 121 F→pureid {a} {b} x = sym ( begin
125 pure id <*> x 122 pure id <*> x
126 ≡⟨ IsApplicative.identity ismf ⟩ 123 ≡⟨ IsApplicative.identity ismf ⟩
127 x 124 x
128 ≡⟨ ≡-cong ( λ k → k x ) (sym ( IsFunctor.identity (isFunctor F ) )) ⟩ FMap F id x 125 ≡⟨ sym ( IsFunctor.identity (isFunctor F ) x ) ⟩
126 FMap F id x
129 ∎ ) 127 ∎ )
130 where 128 where
131 open Relation.Binary.PropositionalEquality 129 open Relation.Binary.PropositionalEquality
132 open Relation.Binary.PropositionalEquality.≡-Reasoning 130 open Relation.Binary.PropositionalEquality.≡-Reasoning
133 F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x 131 F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x
134 F→pure {a} {b} {f} {x} = sym ( begin 132 F→pure {a} {b} {f} {x} = sym ( begin
135 pure f <*> x 133 pure f <*> x
136 ≡⟨ ≡-cong ( λ k → k x ) (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x → IsApplicative.identity ismf ))) ⟩ 134 ≡⟨ (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) (λ x → IsApplicative.identity ismf )) x ⟩
137 FMap F f x 135 FMap F f x
138 ∎ ) 136 ∎ )
139 where 137 where
140 open Relation.Binary.PropositionalEquality 138 open Relation.Binary.PropositionalEquality
141 open Relation.Binary.PropositionalEquality.≡-Reasoning 139 open Relation.Binary.PropositionalEquality.≡-Reasoning
181 (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*> pure g) <*> y 179 (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*> pure g) <*> y
182 ≡⟨ IsApplicative.composition ismf ⟩ 180 ≡⟨ IsApplicative.composition ismf ⟩
183 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y) 181 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y)
184 ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩ 182 ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩
185 (FMap F (λ j k → f j , k) x) <*> (FMap F g y) 183 (FMap F (λ j k → f j , k) x) <*> (FMap F g y)
186 ≡⟨ ≡-cong ( λ k → k x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F )) ⟩ 184 ≡⟨ ≡-cong ( λ k → k <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F ) x ) ⟩
187 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y) 185 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y)
188 ≡⟨⟩ 186 ≡⟨⟩
189 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) ) 187 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
190 ∎ 188 ∎
191 where 189 where
192 open Relation.Binary.PropositionalEquality 190 open Relation.Binary.PropositionalEquality
193 open Relation.Binary.PropositionalEquality.≡-Reasoning 191 open Relation.Binary.PropositionalEquality.≡-Reasoning
194 φab-comm : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ] 192 φab-comm : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]
195 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ] 193 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
196 φab-comm {a} {b} {f} = extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → φab-comm0 x ) 194 φab-comm {a} {b} {f} = λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → φab-comm0 x
197 associativity0 : {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 ≡ 195 associativity0 : {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 ≡
198 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x 196 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x
199 associativity0 {x} {y} {f} ((a , b) , c ) = begin 197 associativity0 {x} {y} {f} ((a , b) , c ) = begin
200 φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c))) 198 φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
201 ≡⟨⟩ 199 ≡⟨⟩
251 open Relation.Binary.PropositionalEquality 249 open Relation.Binary.PropositionalEquality
252 open Relation.Binary.PropositionalEquality.≡-Reasoning 250 open Relation.Binary.PropositionalEquality.≡-Reasoning
253 associativity : {a b c : Obj Sets} → Sets [ Sets [ φ 251 associativity : {a b c : Obj Sets} → Sets [ Sets [ φ
254 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ] 252 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
255 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ] 253 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ]
256 associativity {a} {b} {c} = extensionality Sets ( λ x → associativity0 x ) 254 associativity {a} {b} {c} x = associativity0 x
257 unitarity-idr0 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [ 255 unitarity-idr0 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [
258 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o 256 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
259 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x 257 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x
260 unitarity-idr0 {a} {b} (x , OneObj ) = begin 258 unitarity-idr0 {a} {b} (x , OneObj ) = begin
261 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ (( FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) )) 259 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ (( FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
282 open Relation.Binary.PropositionalEquality 280 open Relation.Binary.PropositionalEquality
283 open Relation.Binary.PropositionalEquality.≡-Reasoning 281 open Relation.Binary.PropositionalEquality.≡-Reasoning
284 unitarity-idr : {a b : Obj Sets} → Sets [ Sets [ 282 unitarity-idr : {a b : Obj Sets} → Sets [ Sets [
285 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o 283 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
286 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ] 284 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
287 unitarity-idr {a} {b} = extensionality Sets ( λ x → unitarity-idr0 {a} {b} x ) 285 unitarity-idr {a} {b} x = unitarity-idr0 {a} {b} x
288 unitarity-idl0 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [ 286 unitarity-idl0 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [
289 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o 287 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o
290 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x 288 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x
291 unitarity-idl0 {a} {b} ( OneObj , x) = begin 289 unitarity-idl0 {a} {b} ( OneObj , x) = begin
292 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) ) 290 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) )
308 where 306 where
309 open Relation.Binary.PropositionalEquality 307 open Relation.Binary.PropositionalEquality
310 open Relation.Binary.PropositionalEquality.≡-Reasoning 308 open Relation.Binary.PropositionalEquality.≡-Reasoning
311 unitarity-idl : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o 309 unitarity-idl : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
312 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ] 310 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
313 unitarity-idl {a} {b} = extensionality Sets ( λ x → unitarity-idl0 {a} {b} x ) 311 unitarity-idl {a} {b} x = unitarity-idl0 {a} {b} x
314 312
315 ---- 313 ----
316 -- 314 --
317 -- Monoidal laws implies Applicative laws 315 -- Monoidal laws implies Applicative laws
318 -- 316 --
352 left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 350 left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq
353 open Relation.Binary.PropositionalEquality 351 open Relation.Binary.PropositionalEquality
354 FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d } 352 FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d }
355 { f : Hom Sets (c * d) e } 353 { f : Hom Sets (c * d) e }
356 { x : FObj F a } { y : FObj F b } 354 { x : FObj F a } { y : FObj F b }
357 → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( f o map g h ) ( φ ( x , y ) ) 355 → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( Sets [ f o map g h ] ) ( φ ( x , y ) )
358 FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin 356 FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin
359 FMap F ( f o map g h ) ( φ ( x , y ) ) 357 FMap F ( Sets [ f o map g h ] ) ( φ ( x , y ) )
360 ≡⟨ ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩ 358 ≡⟨ IsFunctor.distr (isFunctor F) ( φ ( x , y )) ⟩
361 FMap F f (( FMap F ( map g h ) ) ( φ ( x , y ))) 359 FMap F f (( FMap F ( map g h ) ) ( φ ( x , y )))
362 ≡⟨ ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono ) ⟩ 360 ≡⟨ ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono ) ⟩
363 FMap F f ( φ ( FMap F g x , FMap F h y ) ) 361 FMap F f ( φ ( FMap F g x , FMap F h y ) )
364 ∎ ) 362 ∎ )
365 where 363 where
366 open Relation.Binary.PropositionalEquality.≡-Reasoning 364 open Relation.Binary.PropositionalEquality.≡-Reasoning
367 u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u 365 u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u
368 u→F {a} {u} = sym ( ≡-cong ( λ k → k u ) ( IsFunctor.identity ( isFunctor F ) ) ) 366 u→F {a} {u} = sym ( IsFunctor.identity ( isFunctor F ) u)
369 φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u 367 φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
370 φunitr {a} {u} = sym ( begin 368 φunitr {a} {u} = sym ( begin
371 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u 369 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
372 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩ 370 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩
373 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) ) 371 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) )
374 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ 372 ≡⟨ sym ( IsFunctor.distr ( isFunctor F ) _ ) ⟩
375 (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) ) 373 (FMap F ( Sets [ (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)) ] )) ( φ ( unit , u) )
376 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) )) ⟩ 374 ≡⟨ IsFunctor.≈-cong ( isFunctor F ) (Iso.iso→ (IsMonoidal.mλ-iso isM)) _ ⟩
377 FMap F id ( φ ( unit , u) ) 375 FMap F id ( φ ( unit , u) )
378 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ 376 ≡⟨ IsFunctor.identity ( isFunctor F ) _ ⟩
379 id ( φ ( unit , u) ) 377 id ( φ ( unit , u) )
380 ≡⟨⟩ 378 ≡⟨⟩
381 φ ( unit , u) 379 φ ( unit , u)
382 ∎ ) 380 ∎ )
383 where 381 where
385 φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u 383 φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
386 φunitl {a} {u} = sym ( begin 384 φunitl {a} {u} = sym ( begin
387 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u 385 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
388 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩ 386 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩
389 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) ) 387 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) )
390 ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩ 388 ≡⟨ sym ( IsFunctor.distr ( isFunctor F ) _ ) ⟩
391 (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) ) 389 (FMap F (Sets [ (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)) ] )) ( φ ( u , unit ) )
392 ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) )) ⟩ 390 ≡⟨ IsFunctor.≈-cong ( isFunctor F ) (Iso.iso→ (IsMonoidal.mρ-iso isM)) _ ⟩
393 FMap F id ( φ ( u , unit ) ) 391 FMap F id ( φ ( u , unit ) )
394 ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩ 392 ≡⟨ IsFunctor.identity ( isFunctor F ) _ ⟩
395 id ( φ ( u , unit ) ) 393 id ( φ ( u , unit ) )
396 ≡⟨⟩ 394 ≡⟨⟩
397 φ ( u , unit ) 395 φ ( u , unit )
398 ∎ ) 396 ∎ )
399 where 397 where
429 ≡⟨ ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ 427 ≡⟨ ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
430 (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w)) ) ) φunitr ⟩ 428 (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w)) ) ) φunitr ⟩
431 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ 429 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
432 ( (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w)) 430 ( (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w))
433 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ 431 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
434 (k u , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ))) ⟩ 432 (k , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ) _ )) ⟩
435 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ 433 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
436 ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w)) 434 ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w))
437 ≡⟨⟩ 435 ≡⟨⟩
438 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ 436 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
439 ( FMap F (λ x g h → x (g h) ) u , v)) , w)) 437 ( FMap F (λ x g h → x (g h) ) u , v)) , w))
440 ≡⟨ ≡-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 ⟩ 438 ≡⟨ ≡-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 ⟩
441 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)) 439 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))
442 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩ 440 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩
443 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)) 441 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id ]) (φ (u , v)) , w))
444 ≡⟨⟩ 442 ≡⟨⟩
445 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w)) 443 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w))
446 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩ 444 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩
447 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w)) 445 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w))
448 ≡⟨ FφF→F ⟩ 446 ≡⟨ FφF→F ⟩
449 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w)) 447 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id ] ) (φ (φ (u , v) , w))
450 ≡⟨⟩ 448 ≡⟨⟩
451 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w)) 449 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w))
452 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)) )) (sym (IsFunctor.identity (isFunctor F ))) ⟩ 450 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k) (sym (IsFunctor.identity (isFunctor F ) _)) ⟩
453 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) ) 451 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) )
454 ≡⟨ ≡-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))) ⟩ 452 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k ) (sym (IsFunctor.≈-cong (isFunctor F) (Iso.iso→ (mα-iso isM)) _)) ⟩
455 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)) ) 453 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Sets [ (Iso.≅← (mα-iso isM)) o (Iso.≅→ (mα-iso isM)) ] ) (φ (φ (u , v) , w)) )
456 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (k (φ (φ (u , v) , w)))) ( IsFunctor.distr (isFunctor F )) ⟩ 454 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k) ( IsFunctor.distr (isFunctor F ) _ ) ⟩
457 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)) )) 455 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)) ))
458 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩ 456 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) k) ) (sym ( IsHaskellMonoidalFunctor.assocφ mono ) ) ⟩
459 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w)))) 457 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w))))
460 ≡⟨⟩ 458 ≡⟨⟩
461 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)))) 459 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))))
462 ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩ 460 ≡⟨ (sym ( IsFunctor.distr (isFunctor F ) _ )) ⟩
463 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))) 461 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)))
464 ≡⟨⟩ 462 ≡⟨⟩
465 FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w))) 463 FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w)))
466 ≡⟨⟩ 464 ≡⟨⟩
467 FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) ( proj₂ x))) ( φ ( u , (φ (v , w)))) 465 FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) ( proj₂ x))) ( φ ( u , (φ (v , w))))
476 homomorphism {a} {b} {f} {x} = begin 474 homomorphism {a} {b} {f} {x} = begin
477 pure f <*> pure x 475 pure f <*> pure x
478 ≡⟨⟩ 476 ≡⟨⟩
479 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit)) 477 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit))
480 ≡⟨ FφF→F ⟩ 478 ≡⟨ FφF→F ⟩
481 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x)) (φ (unit , unit)) 479 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x) ] ) (φ (unit , unit))
482 ≡⟨⟩ 480 ≡⟨⟩
483 FMap F (λ y → f x) (φ (unit , unit)) 481 FMap F (λ y → f x) (φ (unit , unit))
484 ≡⟨ ≡-cong ( λ k → FMap F (λ y → f x) k ) φunitl ⟩ 482 ≡⟨ ≡-cong ( λ k → FMap F (λ y → f x) k ) φunitl ⟩
485 FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit) 483 FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit)
486 ≡⟨⟩ 484 ≡⟨⟩
487 FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit) 485 FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit)
488 ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F ))) ⟩ 486 ≡⟨ sym (IsFunctor.distr (isFunctor F) _) ⟩
489 FMap F (λ y → f x) unit 487 FMap F (λ y → f x) unit
490 ≡⟨⟩ 488 ≡⟨⟩
491 pure (f x) 489 pure (f x)
492 ∎ 490 ∎
493 where 491 where
498 ≡⟨⟩ 496 ≡⟨⟩
499 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ y → x) unit)) 497 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ y → x) unit))
500 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit)) ) u→F ⟩ 498 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit)) ) u→F ⟩
501 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit)) 499 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit))
502 ≡⟨ FφF→F ⟩ 500 ≡⟨ FφF→F ⟩
503 FMap F ((λ r → proj₁ r (proj₂ r)) o map id (λ y → x)) (φ (u , unit)) 501 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map id (λ y → x) ] ) (φ (u , unit))
504 ≡⟨⟩ 502 ≡⟨⟩
505 FMap F (λ r → proj₁ r x) (φ (u , unit)) 503 FMap F (λ r → proj₁ r x) (φ (u , unit))
506 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩ 504 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩
507 FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u ) 505 FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u )
508 ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩ 506 ≡⟨ ( sym ( IsFunctor.distr (isFunctor F ) _) ) ⟩
509 FMap F (( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) ))) u 507 FMap F (Sets [ ( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) )) ] ) u
510 ≡⟨⟩ 508 ≡⟨⟩
511 FMap F (( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) ))) u 509 FMap F (Sets [( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) )) ] ) u
512 ≡⟨ left ( IsFunctor.distr (isFunctor F )) ⟩ 510 ≡⟨ IsFunctor.distr (isFunctor F ) _ ⟩
513 FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u) 511 FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u)
514 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩ 512 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩
515 FMap F (λ r → proj₂ r x) (φ (unit , u)) 513 FMap F (λ r → proj₂ r x) (φ (unit , u))
516 ≡⟨⟩ 514 ≡⟨⟩
517 FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id) (φ (unit , u)) 515 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id ] ) (φ (unit , u))
518 ≡⟨ sym FφF→F ⟩ 516 ≡⟨ sym FφF→F ⟩
519 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u)) 517 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u))
520 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩ 518 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩
521 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , u)) 519 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , u))
522 ≡⟨⟩ 520 ≡⟨⟩
560 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) 558 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
561 natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin 559 natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin
562 FMap F (map f g) (φ (x , y)) 560 FMap F (map f g) (φ (x , y))
563 ≡⟨⟩ 561 ≡⟨⟩
564 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (<*> (FMap F (λ j k → j , k) x) y) 562 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (<*> (FMap F (λ j k → j , k) x) y)
565 ≡⟨ ≡-cong ( λ h → h (x , y)) ( IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF ))) ⟩ 563 ≡⟨ IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF )) _ ⟩
566 <*> (FMap F (λ j k → j , k) (FMap F f x)) (FMap F g y) 564 <*> (FMap F (λ j k → j , k) (FMap F f x)) (FMap F g y)
567 ≡⟨⟩ 565 ≡⟨⟩
568 φ (FMap F f x , FMap F g y) 566 φ (FMap F f x , FMap F g y)
569 ∎ 567 ∎
570 where 568 where
571 open Relation.Binary.PropositionalEquality.≡-Reasoning 569 open Relation.Binary.PropositionalEquality.≡-Reasoning
572 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } 570 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
573 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c)) 571 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c))
574 assocφ {x} {y} {z} {a} {b} {c} = ≡-cong ( λ h → h ((a , b) , c ) ) ( IsMonoidalFunctor.associativity isMF ) 572 assocφ {x} {y} {z} {a} {b} {c} = IsMonoidalFunctor.associativity isMF _
575 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x 573 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x
576 idrφ {a} {x} = ≡-cong ( λ h → h (x , OneObj ) ) ( IsMonoidalFunctor.unitarity-idr isMF {a} {One} ) 574 idrφ {a} {x} = IsMonoidalFunctor.unitarity-idr isMF {a} {One} (x , OneObj)
577 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x 575 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x
578 idlφ {a} {x} = ≡-cong ( λ h → h (OneObj , x ) ) ( IsMonoidalFunctor.unitarity-idl isMF {One} {a} ) 576 idlφ {a} {x} = IsMonoidalFunctor.unitarity-idl isMF {One} {a} (OneObj , x)
579 577
580 -- end 578 -- end