Mercurial > hg > Members > kono > Proof > category

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
2
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Category
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
5 open import Definitions
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
6 open Functor
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
7
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
8 --
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
9 -- To show Applicative functor is monoidal functor, uniquness of Functor is necessary, which is derived from the free theorem.
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
10 --
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
11 -- they say it is not possible to prove FreeTheorem in Agda nor Coq
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
12 -- https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
13 -- so we postulate this
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
14
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
15 module applicative (
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
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} )
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
17 where
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
18
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
1109
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1106
diff changeset
20 open import Data.Product renaming (_×_ to _*_) hiding (_<*>_)
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 open import Category.Constructions.Product
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open import HomReasoning
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 open import Relation.Binary.Core
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 open import Relation.Binary
768
9bcdbfbaaa39 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 766
diff changeset
25 open import monoidal
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 778
diff changeset
26 open import Relation.Binary.PropositionalEquality hiding ( [_] )
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
27
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
28 -----
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
29 --
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
30 -- Applicative Functor
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
31 --
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
32 -- is a monoidal functor on Sets and it can be constructoed from Haskell monoidal functor and vais versa
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
33 --
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
34 ----
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
35
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
36 -----
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
37 UniquenessOfFunctor : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁' c₂' ℓ') (F : Functor C D)
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
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) )
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
39 → ( {b : Obj C } → D [ fmap (id1 C b) ≈ id1 D (FObj F b) ] )
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
40 → D [ fmap f ≈ FMap F f ]
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
41 UniquenessOfFunctor C D F {a} {b} {f} fmap eq = begin
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
42 fmap f
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
43 ≈↑⟨ idL ⟩
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
44 id1 D (FObj F b) o fmap f
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
45 ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
46 FMap F (id1 C b) o fmap f
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
47 ≈⟨ FT C D F fmap (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory C ))) ⟩
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
48 fmap (id1 C b) o FMap F f
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
49 ≈⟨ car eq ⟩
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
50 id1 D (FObj F b) o FMap F f
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
51 ≈⟨ idL ⟩
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
52 FMap F f
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
53 ∎
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
54 where open ≈-Reasoning D
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
55
768
9bcdbfbaaa39 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 766
diff changeset
56 open import Category.Sets
9bcdbfbaaa39 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 766
diff changeset
57 import Relation.Binary.PropositionalEquality
696
10ccac3bc285 Monoidal category and applicative functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
59 _・_ : {c₁ : Level} { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
60 _・_ f g = λ x → f ( g x )
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
61 record IsApplicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
62 ( pure : {a : Obj Sets} → Hom Sets a ( FObj F a ) )
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
63 ( _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b )
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
64 : Set (suc (suc c₁)) where
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
65 field
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
66 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
67 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
68 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w)
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
69 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
70 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
71 -- from http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
72
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
73 record Applicative {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
705
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
74 : Set (suc (suc c₁)) where
73a998711118 add Applicative and HaskellMonoidal Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 704
diff changeset
75 field
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
76 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
77 <*> : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
78 isApplicative : IsApplicative F pure <*>
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
79
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
80 ------
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
81 --
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
82 -- Appllicative Functor is a Monoidal Functor
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
83 --
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
84
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
85 Applicative→Monoidal : {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F )
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
86 → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf )
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
87 → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
727
ea84cc6c1797 monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 726
diff changeset
88 Applicative→Monoidal {l} F mf ismf = record {
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
89 MF = F
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
90 ; ψ = λ x → unit
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
91 ; isMonodailFunctor = record {
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
92 φab = record { TMap = λ x → φ ; isNTrans = record { commute = φab-comm } }
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
93 ; associativity = λ {a b c} → associativity {a} {b} {c}
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
94 ; unitarity-idr = λ {a b} → unitarity-idr {a} {b}
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
95 ; unitarity-idl = λ {a b} → unitarity-idl {a} {b}
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
96 }
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
97 } where
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
98 open Monoidal
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
99 open IsMonoidal hiding ( _■_ ; _□_ )
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
100 M = MonoidalSets
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
101 isM = Monoidal.isMonoidal MonoidalSets
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
102 unit = Applicative.pure mf OneObj
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
103 _⊗_ : (x y : Obj Sets ) → Obj Sets
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
104 _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
105 _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
106 _□_ f g = FMap (m-bi M) ( f , g )
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
107 φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
108 φ x = Applicative.<*> mf (FMap F (λ j k → (j , k)) (proj₁ x )) (proj₂ x)
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
109 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
110 _<*>_ = Applicative.<*> mf
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
111 left : {a b : Obj Sets} → {x y : FObj F ( a → b )} → {h : FObj F a } → ( x ≡ y ) → x <*> h ≡ y <*> h
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
112 left {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k <*> h ) eq
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
113 right : {a b : Obj Sets} → {h : FObj F ( a → b )} → {x y : FObj F a } → ( x ≡ y ) → h <*> x ≡ h <*> y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
114 right {_} {_} {h} {_} {_} eq = ≡-cong ( λ k → h <*> k ) eq
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
115 id : { a : Obj Sets } → a → a
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
116 id x = x
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
117 pure : {a : Obj Sets } → Hom Sets a ( FObj F a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
118 pure a = Applicative.pure mf a
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
119 -- special case
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
120 F→pureid : {a b : Obj Sets } → (x : FObj F a ) → FMap F id x ≡ pure id <*> x
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
121 F→pureid {a} {b} x = sym ( begin
722
69f01b82dfc9 uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 721
diff changeset
122 pure id <*> x
69f01b82dfc9 uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 721
diff changeset
123 ≡⟨ IsApplicative.identity ismf ⟩
69f01b82dfc9 uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 721
diff changeset
124 x
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
125 ≡⟨ sym ( IsFunctor.identity (isFunctor F ) x ) ⟩
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
126 FMap F id x
722
69f01b82dfc9 uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 721
diff changeset
127 ∎ )
69f01b82dfc9 uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 721
diff changeset
128 where
69f01b82dfc9 uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 721
diff changeset
129 open Relation.Binary.PropositionalEquality
69f01b82dfc9 uniquness of functor fmap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 721
diff changeset
130 open Relation.Binary.PropositionalEquality.≡-Reasoning
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
131 F→pure : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } → FMap F f x ≡ pure f <*> x
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
132 F→pure {a} {b} {f} {x} = sym ( begin
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
133 pure f <*> x
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
134 ≡⟨ (UniquenessOfFunctor Sets Sets F ( λ f x → pure f <*> x ) (λ x → IsApplicative.identity ismf )) x ⟩
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
135 FMap F f x
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
136 ∎ )
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
137 where
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
138 open Relation.Binary.PropositionalEquality
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
139 open Relation.Binary.PropositionalEquality.≡-Reasoning
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
140 p*p : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
141 p*p = IsApplicative.homomorphism ismf
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
142 comp = IsApplicative.composition ismf
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
143 inter = IsApplicative.interchange ismf
729
6bc9d68898ef clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 727
diff changeset
144 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
6bc9d68898ef clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 727
diff changeset
145 pureAssoc f g h = trans ( trans (sym comp) (left (left p*p) )) ( left p*p )
6bc9d68898ef clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 727
diff changeset
146 where
6bc9d68898ef clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 727
diff changeset
147 open Relation.Binary.PropositionalEquality
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
148 φab-comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
149 (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
150 φab-comm0 {a} {b} {(f , g)} (x , y) = begin
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
151 ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) )
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
152 ≡⟨⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
153 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y)
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
154 ≡⟨⟩
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
155 FMap F (map f g) ((FMap F (λ j k → j , k) x) <*> y)
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
156 ≡⟨ F→pure ⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
157 (pure (map f g) <*> (FMap F (λ j k → j , k) x <*> y))
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
158 ≡⟨ right ( left F→pure ) ⟩
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
159 (pure (map f g)) <*> ((pure (λ j k → j , k) <*> x) <*> y)
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
160 ≡⟨ sym ( IsApplicative.composition ismf ) ⟩
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
161 (( pure _・_ <*> (pure (map f g))) <*> (pure (λ j k → j , k) <*> x)) <*> y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
162 ≡⟨ left ( sym ( IsApplicative.composition ismf )) ⟩
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
163 ((( pure _・_ <*> (( pure _・_ <*> (pure (map f g))))) <*> pure (λ j k → j , k)) <*> x) <*> y
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
164 ≡⟨ trans ( trans (left ( left (left (right p*p )))) ( left ( left ( left p*p)))) (left (left p*p)) ⟩
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
165 (pure (( _・_ (( _・_ ((map f g))))) (λ j k → j , k)) <*> x) <*> y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
166 ≡⟨⟩
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
167 (pure (λ j k → f j , g k) <*> x) <*> y
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
168 ≡⟨⟩
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
169 ( pure ((_・_ (( _・_ ( ( λ h → h g ))) ( _・_ ))) ((λ j k → f j , k))) <*> x ) <*> y
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
170 ≡⟨ sym ( trans (left (left (left p*p))) (left ( left p*p)) ) ⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
171 ((((pure _・_ <*> pure ((λ h → h g) ・ _・_)) <*> pure (λ j k → f j , k)) <*> x) <*> y)
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
172 ≡⟨ sym (trans ( left ( left ( left (right (left p*p) )))) (left ( left (left (right p*p ))))) ⟩
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
173 (((pure _・_ <*> (( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ ))) <*> (pure (λ j k → f j , k))) <*> x ) <*> y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
174 ≡⟨ left ( ( IsApplicative.composition ismf )) ⟩
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
175 ((( pure _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ )) <*> (pure (λ j k → f j , k) <*> x )) <*> y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
176 ≡⟨ left (IsApplicative.composition ismf ) ⟩
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
177 ( pure ( λ h → h g ) <*> ( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) ) <*> y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
178 ≡⟨ left (sym (IsApplicative.interchange ismf )) ⟩
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
179 (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*> pure g) <*> y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
180 ≡⟨ IsApplicative.composition ismf ⟩
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
181 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y)
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
182 ≡⟨ sym ( trans (left F→pure ) ( right F→pure ) ) ⟩
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
183 (FMap F (λ j k → f j , k) x) <*> (FMap F g y)
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
184 ≡⟨ ≡-cong ( λ k → k <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F ) x ) ⟩
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
185 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y)
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
186 ≡⟨⟩
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
187 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
188 ∎
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
189 where
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
190 open Relation.Binary.PropositionalEquality
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
191 open Relation.Binary.PropositionalEquality.≡-Reasoning
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
192 φab-comm : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
193 ≈ Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
194 φab-comm {a} {b} {f} = λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → φab-comm0 x
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
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 ≡
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
196 (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o φ □ id1 Sets (FObj F c) ] ]) x
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
197 associativity0 {x} {y} {f} ((a , b) , c ) = begin
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
198 φ (( id □ φ ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
199 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
200 (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c)
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
201 ≡⟨ trans (left F→pure) (right (left F→pure) ) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
202 (pure (λ j k → j , k) <*> a) <*> ( (pure (λ j k → j , k) <*> b) <*> c)
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
203 ≡⟨ sym comp ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
204 ( ( pure _・_ <*> (pure (λ j k → j , k) <*> a)) <*> (pure (λ j k → j , k) <*> b)) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
205 ≡⟨ sym ( left comp ) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
206 (( ( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k) <*> a))) <*> (pure (λ j k → j , k))) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
207 ≡⟨ sym ( left ( left ( left (right comp )))) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
208 (( ( pure _・_ <*> (( (pure _・_ <*> pure _・_ ) <*> (pure (λ j k → j , k))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
209 ≡⟨ trans (left ( left (left ( right (left ( left p*p )))))) (left ( left ( left (right (left p*p))))) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
210 (( ( pure _・_ <*> ((pure ((_・_ ( _・_ )) ((λ j k → j , k)))) <*> a)) <*> (pure (λ j k → j , k))) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
211 ≡⟨ sym (left ( left ( left comp ) )) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
212 (((( ( pure _・_ <*> (pure _・_ )) <*> (pure ((_・_ ( _・_ )) ((λ j k → j , k))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
213 ≡⟨ trans (left ( left ( left (left (left p*p))))) (left ( left ( left (left p*p )))) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
214 ((((pure ( ( _・_ (_・_ )) (((_・_ ( _・_ )) ((λ j k → j , k)))))) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
215 ≡⟨⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
216 ((((pure (λ f g x y → f , g x y)) <*> a) <*> (pure (λ j k → j , k))) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
217 ≡⟨ left ( left inter ) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
218 (((pure (λ f → f (λ j k → j , k))) <*> ((pure (λ f g x y → f , g x y)) <*> a) ) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
219 ≡⟨ sym ( left ( left comp )) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
220 (((( pure _・_ <*> (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
221 ≡⟨ trans (left ( left (left (left p*p) ))) (left (left (left p*p ) )) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
222 (((pure (λ f g h → f , g , h)) <*> a) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
223 ≡⟨ sym (trans ( left ( left ( left (left (right (right p*p))) ) )) (trans (left (left( left (left (right p*p)))))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
224 (trans (left (left (left (left p*p)))) (trans ( left (left (left (right (left (right p*p ))))))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
225 (trans (left (left (left (right (left p*p))))) (trans (left (left (left (right p*p)))) (left (left (left p*p)))) ) ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
226 ) ) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
227 ((((pure _・_ <*> ((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) <*>
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
228 (( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k))) <*> a) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
229 ≡⟨ left (left comp ) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
230 (((pure _・_ <*> ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))) <*>
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
231 ((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a)) <*> b) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
232 ≡⟨ left comp ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
233 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
234 (((( pure _・_ <*> ( pure _・_ <*> (pure (λ j k → j , k)))) <*> pure (λ j k → j , k)) <*> a) <*> b)) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
235 ≡⟨ left ( right (left comp )) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
236 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
237 ((( pure _・_ <*> (pure (λ j k → j , k))) <*> (pure (λ j k → j , k) <*> a)) <*> b)) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
238 ≡⟨ left ( right comp ) ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
239 ((pure _・_ <*> ( pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))) <*>
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
240 (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b))) <*> c
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
241 ≡⟨ comp ⟩
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
242 pure (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) <*> ( (pure (λ j k → j , k) <*> ( (pure (λ j k → j , k) <*> a) <*> b)) <*> c)
726
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 725
diff changeset
243 ≡⟨ sym ( trans ( trans F→pure (right (left F→pure ))) ( right ( left (right (left F→pure ))))) ⟩
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
244 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)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
245 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
246 ( FMap F (Iso.≅→ (mα-iso isM))) (φ (( φ □ id1 Sets (FObj F f) ) ((a , b) , c)))
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
247 ∎
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
248 where
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
249 open Relation.Binary.PropositionalEquality
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
250 open Relation.Binary.PropositionalEquality.≡-Reasoning
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
251 associativity : {a b c : Obj Sets} → Sets [ Sets [ φ
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
252 o Sets [ (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
253 ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ o (φ □ id1 Sets (FObj F c)) ] ] ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
254 associativity {a} {b} {c} x = associativity0 x
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
255 unitarity-idr0 : {a b : Obj Sets} ( x : FObj F a * One ) → ( Sets [
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
256 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
257 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x ≡ Iso.≅→ (mρ-iso isM) x
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
258 unitarity-idr0 {a} {b} (x , OneObj ) = begin
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
259 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ (( FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
260 ≡⟨⟩
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
261 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (pure OneObj))
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
262 ≡⟨ ≡-cong ( λ k → FMap F proj₁ k) ( IsApplicative.interchange ismf ) ⟩
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
263 FMap F proj₁ ((pure (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x))
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
264 ≡⟨ ( trans F→pure (right ( right F→pure )) ) ⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
265 pure proj₁ <*> ((pure (λ f → f OneObj)) <*> (pure (λ j k → j , k) <*> x))
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
266 ≡⟨ sym ( right comp ) ⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
267 pure proj₁ <*> (((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k)) <*> x)
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
268 ≡⟨ sym comp ⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
269 ( ( pure _・_ <*> (pure proj₁ ) ) <*> ((pure _・_ <*> (pure (λ f → f OneObj))) <*> pure (λ j k → j , k))) <*> x
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
270 ≡⟨ trans ( trans ( trans ( left ( left p*p)) ( left ( right (left p*p) ))) (left (right p*p) ) ) (left p*p) ⟩
727
ea84cc6c1797 monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 726
diff changeset
271 pure ( ( _・_ (proj₁ {l} {l})) ((_・_ ((λ f → f OneObj))) (λ j k → j , k))) <*> x
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
272 ≡⟨⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
273 pure id <*> x
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
274 ≡⟨ IsApplicative.identity ismf ⟩
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
275 x
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
276 ≡⟨⟩
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
277 Iso.≅→ (mρ-iso isM) (x , OneObj)
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
278 ∎
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
279 where
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
280 open Relation.Binary.PropositionalEquality
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
281 open Relation.Binary.PropositionalEquality.≡-Reasoning
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
282 unitarity-idr : {a b : Obj Sets} → Sets [ Sets [
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
283 FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ o
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
284 FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
285 unitarity-idr {a} {b} x = unitarity-idr0 {a} {b} x
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
286 unitarity-idl0 : {a b : Obj Sets} ( x : One * FObj F b ) → ( Sets [
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
287 FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ o
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
288 FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x ≡ Iso.≅→ (mλ-iso isM) x
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
289 unitarity-idl0 {a} {b} ( OneObj , x) = begin
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
290 (FMap F (Iso.≅→ (mλ-iso isM))) ( φ ( unit , x ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
291 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
292 FMap F proj₂ ((FMap F (λ j k → j , k) (pure OneObj)) <*> x)
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
293 ≡⟨ ( trans F→pure (right ( left F→pure )) ) ⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
294 pure proj₂ <*> ((pure (λ j k → j , k) <*> (pure OneObj)) <*> x)
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
295 ≡⟨ sym comp ⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
296 ((pure _・_ <*> (pure proj₂)) <*> (pure (λ j k → j , k) <*> (pure OneObj))) <*> x
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
297 ≡⟨ trans (trans (left (left p*p )) (left ( right p*p)) ) (left p*p) ⟩
727
ea84cc6c1797 monoidal functor and applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 726
diff changeset
298 pure ((_・_ (proj₂ {l}) )((λ (j : One {l}) (k : b ) → j , k) OneObj)) <*> x
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
299 ≡⟨⟩
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
300 pure id <*> x
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
301 ≡⟨ IsApplicative.identity ismf ⟩
720
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
302 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
303 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 719
diff changeset
304 Iso.≅→ (mλ-iso isM) ( OneObj , x )
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
305 ∎
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
306 where
725
bd371f36df9a fill proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 724
diff changeset
307 open Relation.Binary.PropositionalEquality
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
308 open Relation.Binary.PropositionalEquality.≡-Reasoning
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
309 unitarity-idl : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
310 Sets [ φ o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
311 unitarity-idl {a} {b} x = unitarity-idl0 {a} {b} x
719
a017ed40dd77 Applicative law → Monoidal law begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 717
diff changeset
312
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
313 ----
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
314 --
773
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 769
diff changeset
315 -- Monoidal laws implies Applicative laws
730
e4ef69bae044 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 729
diff changeset
316 --
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
317
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
318 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
319 ( Mono : HaskellMonoidalFunctor F )
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
320 → Applicative F
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
321 HaskellMonoidal→Applicative {c₁} F Mono = record {
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
322 pure = pure ;
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
323 <*> = _<*>_ ;
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
324 isApplicative = record {
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
325 identity = identity
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
326 ; composition = composition
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
327 ; homomorphism = homomorphism
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
328 ; interchange = interchange
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
329 }
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
330 }
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
331 where
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
332 unit : FObj F One
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
333 unit = HaskellMonoidalFunctor.unit Mono
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
334 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) )
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
335 φ = HaskellMonoidalFunctor.φ Mono
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
336 mono : IsHaskellMonoidalFunctor F unit φ
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
337 mono = HaskellMonoidalFunctor.isHaskellMonoidalFunctor Mono
714
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
338 id : { a : Obj Sets } → a → a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
339 id x = x
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
340 isM : IsMonoidal (Sets {c₁}) One SetsTensorProduct
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
341 isM = Monoidal.isMonoidal MonoidalSets
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
342 pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
343 pure {a} x = FMap F ( λ y → x ) (unit )
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
344 _<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
345 _<*>_ {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ ( x , y ))
721
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
346 -- right does not work right it makes yellows. why?
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
347 -- right : {n : Level} { a b : Set n} → { x y : a } { h : a → b } → ( x ≡ y ) → h x ≡ h y
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
348 -- right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
349 left : {n : Level} { a b : Set n} → { x y : a → b } { h : a } → ( x ≡ y ) → x h ≡ y h
a8b595fb4905 use FMap F f x ≡ pure f <*> x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 720
diff changeset
350 left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
351 open Relation.Binary.PropositionalEquality
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
352 FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d }
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
353 { f : Hom Sets (c * d) e }
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
354 { x : FObj F a } { y : FObj F b }
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
355 → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( Sets [ f o map g h ] ) ( φ ( x , y ) )
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
356 FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
357 FMap F ( Sets [ f o map g h ] ) ( φ ( x , y ) )
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
358 ≡⟨ IsFunctor.distr (isFunctor F) ( φ ( x , y )) ⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
359 FMap F f (( FMap F ( map g h ) ) ( φ ( x , y )))
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
360 ≡⟨ ≡-cong ( λ k → FMap F f k ) ( IsHaskellMonoidalFunctor.natφ mono ) ⟩
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
361 FMap F f ( φ ( FMap F g x , FMap F h y ) )
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
362 ∎ )
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
363 where
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
364 open Relation.Binary.PropositionalEquality.≡-Reasoning
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
365 u→F : {a : Obj Sets } {u : FObj F a} → u ≡ FMap F id u
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
366 u→F {a} {u} = sym ( IsFunctor.identity ( isFunctor F ) u)
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
367 φunitr : {a : Obj Sets } {u : FObj F a} → φ ( unit , u) ≡ FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
368 φunitr {a} {u} = sym ( begin
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
369 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
370 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
371 FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) )
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
372 ≡⟨ sym ( IsFunctor.distr ( isFunctor F ) _ ) ⟩
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
373 (FMap F ( Sets [ (Iso.≅← (IsMonoidal.mλ-iso isM)) o (Iso.≅→ (IsMonoidal.mλ-iso isM)) ] )) ( φ ( unit , u) )
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
374 ≡⟨ IsFunctor.≈-cong ( isFunctor F ) (Iso.iso→ (IsMonoidal.mλ-iso isM)) _ ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
375 FMap F id ( φ ( unit , u) )
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
376 ≡⟨ IsFunctor.identity ( isFunctor F ) _ ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
377 id ( φ ( unit , u) )
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
378 ≡⟨⟩
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
379 φ ( unit , u)
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
380 ∎ )
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
381 where
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
382 open Relation.Binary.PropositionalEquality.≡-Reasoning
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
383 φunitl : {a : Obj Sets } {u : FObj F a} → φ ( u , unit ) ≡ FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
384 φunitl {a} {u} = sym ( begin
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
385 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
386 ≡⟨ ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
387 FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) )
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
388 ≡⟨ sym ( IsFunctor.distr ( isFunctor F ) _ ) ⟩
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
389 (FMap F (Sets [ (Iso.≅← (IsMonoidal.mρ-iso isM)) o (Iso.≅→ (IsMonoidal.mρ-iso isM)) ] )) ( φ ( u , unit ) )
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
390 ≡⟨ IsFunctor.≈-cong ( isFunctor F ) (Iso.iso→ (IsMonoidal.mρ-iso isM)) _ ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
391 FMap F id ( φ ( u , unit ) )
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
392 ≡⟨ IsFunctor.identity ( isFunctor F ) _ ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
393 id ( φ ( u , unit ) )
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
394 ≡⟨⟩
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
395 φ ( u , unit )
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
396 ∎ )
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
397 where
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
398 open Relation.Binary.PropositionalEquality.≡-Reasoning
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
399 open IsMonoidal
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
400 identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a ) <*> u ≡ u
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
401 identity {a} {u} = begin
714
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
402 pure id <*> u
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
403 ≡⟨⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
404 ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , u ) )
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
405 ≡⟨ ≡-cong ( λ k → ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , k ))) u→F ⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
406 ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , FMap F id u ) )
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
407 ≡⟨ FφF→F ⟩
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
408 FMap F (λ x → proj₂ x ) (φ (unit , u ) )
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
409 ≡⟨⟩
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
410 FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u ))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
411 ≡⟨ IsHaskellMonoidalFunctor.idlφ mono ⟩
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
412 u
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
413 ∎
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
414 where
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
415 open Relation.Binary.PropositionalEquality.≡-Reasoning
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
416 composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
417 → (( pure _・_ <*> u ) <*> v ) <*> w ≡ u <*> (v <*> w)
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
418 composition {a} {b} {c} {u} {v} {w} = begin
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
419 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
420 (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w))
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
421 ≡⟨ ≡-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 ⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
422 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
423 (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u )) , v)) , w))
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
424 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k , v)) , w)) ) FφF→F ⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
425 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 773
diff changeset
426 (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , v)) , w))
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
427 ≡⟨ ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 773
diff changeset
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 ⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
429 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
778
06388660995b fix applicative for Agda version 2.5.4.1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 773
diff changeset
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))
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
431 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
432 (k , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ) _ )) ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
433 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
434 ( FMap F (λ x → ((λ y f g x₁ → f (g x₁)) unit x) ) u , v)) , w))
714
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
435 ≡⟨⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
436 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
437 ( FMap F (λ x g h → x (g h) ) u , v)) , w))
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
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 ⟩
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
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))
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
440 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
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))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
442 ≡⟨⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
443 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w))
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
444 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
445 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w))
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
446 ≡⟨ FφF→F ⟩
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
447 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id ] ) (φ (φ (u , v) , w))
714
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 713
diff changeset
448 ≡⟨⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
449 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w))
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
450 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k) (sym (IsFunctor.identity (isFunctor F ) _)) ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
451 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F id (φ (φ (u , v) , w)) )
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
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)) _)) ⟩
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
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)) )
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
454 ≡⟨ ≡-cong ( λ k → FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) k) ( IsFunctor.distr (isFunctor F ) _ ) ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
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)) ))
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
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 ) ) ⟩
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
457 FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w))))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
458 ≡⟨⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
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))))
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
460 ≡⟨ (sym ( IsFunctor.distr (isFunctor F ) _ )) ⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
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)))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
462 ≡⟨⟩
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
463 FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w)))
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
464 ≡⟨⟩
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
465 FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) ( proj₂ x))) ( φ ( u , (φ (v , w))))
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
466 ≡⟨ sym FφF→F ⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
467 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
716
35457f9568f3 composition done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 715
diff changeset
468 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ) (sym u→F ) ⟩
715
1be42267eeee add some tools
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 714
diff changeset
469 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w))))
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
470 ∎
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
471 where
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
472 open Relation.Binary.PropositionalEquality.≡-Reasoning
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
473 homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x)
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
474 homomorphism {a} {b} {f} {x} = begin
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
475 pure f <*> pure x
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
476 ≡⟨⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
477 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
478 ≡⟨ FφF→F ⟩
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
479 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x) ] ) (φ (unit , unit))
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
480 ≡⟨⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
481 FMap F (λ y → f x) (φ (unit , unit))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
482 ≡⟨ ≡-cong ( λ k → FMap F (λ y → f x) k ) φunitl ⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
483 FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit)
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
484 ≡⟨⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
485 FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit)
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
486 ≡⟨ sym (IsFunctor.distr (isFunctor F) _) ⟩
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
487 FMap F (λ y → f x) unit
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
488 ≡⟨⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
489 pure (f x)
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
490 ∎
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
491 where
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
492 open Relation.Binary.PropositionalEquality.≡-Reasoning
713
5e101ee6dab9 identity done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 712
diff changeset
493 interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
494 interchange {a} {b} {u} {x} = begin
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
495 u <*> pure x
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
496 ≡⟨⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
497 FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ y → x) unit))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
498 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit)) ) u→F ⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
499 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
500 ≡⟨ FφF→F ⟩
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
501 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map id (λ y → x) ] ) (φ (u , unit))
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
502 ≡⟨⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
503 FMap F (λ r → proj₁ r x) (φ (u , unit))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
504 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
505 FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u )
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
506 ≡⟨ ( sym ( IsFunctor.distr (isFunctor F ) _) ) ⟩
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
507 FMap F (Sets [ ( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) )) ] ) u
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
508 ≡⟨⟩
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
509 FMap F (Sets [( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) )) ] ) u
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
510 ≡⟨ IsFunctor.distr (isFunctor F ) _ ⟩
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
511 FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u)
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
512 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
513 FMap F (λ r → proj₂ r x) (φ (unit , u))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
514 ≡⟨⟩
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
515 FMap F (Sets [ (λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id ] ) (φ (unit , u))
717
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
516 ≡⟨ sym FφF→F ⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
517 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
518 ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
519 FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , u))
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
520 ≡⟨⟩
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
521 pure (λ f → f x) <*> u
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
522 ∎
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
523 where
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
524 open Relation.Binary.PropositionalEquality.≡-Reasoning
a41b2b9b0407 Haskell Monoidal Funtor to Applicative done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 716
diff changeset
525
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
526 ----
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
527 --
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
528 -- Applicative functor implements Haskell Monoidal functor
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
529 -- Haskell Monoidal functor is directly represents monoidal functor, it is easy to make it from a monoidal functor
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
530 --
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
531
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
532 Applicative→HaskellMonoidal : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
533 ( App : Applicative F )
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
534 → HaskellMonoidalFunctor F
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
535 Applicative→HaskellMonoidal {l} F App = record {
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
536 unit = unit ;
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
537 φ = φ ;
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
538 isHaskellMonoidalFunctor = record {
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
539 natφ = natφ
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
540 ; assocφ = assocφ
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
541 ; idrφ = idrφ
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
542 ; idlφ = idlφ
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
543 }
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
544 } where
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
545 pure = Applicative.pure App
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
546 <*> = Applicative.<*> App
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
547 app = Applicative.isApplicative App
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
548 unit : FObj F One
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
549 unit = pure OneObj
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
550 φ : {a b : Obj Sets} → Hom Sets ((FObj F a) * (FObj F b )) ( FObj F ( a * b ) )
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
551 φ = λ x → <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x)
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
552 isM : IsMonoidal (Sets {l}) One SetsTensorProduct
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
553 isM = Monoidal.isMonoidal MonoidalSets
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
554 MF : MonoidalFunctor {_} {l} {_} {Sets} {Sets} MonoidalSets MonoidalSets
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
555 MF = Applicative→Monoidal F App app
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
556 isMF = MonoidalFunctor.isMonodailFunctor MF
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
557 natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d }
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
558 → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
559 natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
560 FMap F (map f g) (φ (x , y))
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
561 ≡⟨⟩
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
562 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (<*> (FMap F (λ j k → j , k) x) y)
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
563 ≡⟨ IsNTrans.commute ( NTrans.isNTrans ( IsMonoidalFunctor.φab isMF )) _ ⟩
766
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
564 <*> (FMap F (λ j k → j , k) (FMap F f x)) (FMap F g y)
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
565 ≡⟨⟩
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
566 φ (FMap F f x , FMap F g y)
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
567 ∎
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
568 where
c30ca91f3a76 Applicative all done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 765
diff changeset
569 open Relation.Binary.PropositionalEquality.≡-Reasoning
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
570 assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
571 → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c))
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
572 assocφ {x} {y} {z} {a} {b} {c} = IsMonoidalFunctor.associativity isMF _
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
573 idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
574 idrφ {a} {x} = IsMonoidalFunctor.unitarity-idr isMF {a} {One} (x , OneObj)
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
575 idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1109
diff changeset
576 idlφ {a} {x} = IsMonoidalFunctor.unitarity-idl isMF {One} {a} (OneObj , x)
765
171f5386e87e Applicative→HaskellMonoidal begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 732
diff changeset
577
769
43138aead09b clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 768
diff changeset
578 -- end