Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 151:3bd5109c83f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Aug 2013 20:59:31 +0900
parents 5dc6f3f43507
children 3249aaddc405
comparison
equal deleted inserted replaced
150:5dc6f3f43507 151:3bd5109c83f3
22 Carrier : Set c 22 Carrier : Set c
23 _∙_ : Op₂ Carrier 23 _∙_ : Op₂ Carrier
24 ε : Carrier 24 ε : Carrier
25 isMonoid : IsMonoid _≡_ _∙_ ε 25 isMonoid : IsMonoid _≡_ _∙_ ε
26 26
27 postulate Mono : ≡-Monoid c 27 postulate M : ≡-Monoid c
28 open ≡-Monoid 28 open ≡-Monoid
29 29
30 A = Sets {c} 30 A = Sets {c}
31 31
32 -- T : A → (M x A) 32 -- T : A → (M x A)
33 33
34 T : Functor A A 34 T : Functor A A
35 T = record { 35 T = record {
36 FObj = λ a → (Carrier Mono) × a 36 FObj = λ a → (Carrier M) × a
37 ; FMap = λ f → map ( λ x → x ) f 37 ; FMap = λ f → map ( λ x → x ) f
38 ; isFunctor = record { 38 ; isFunctor = record {
39 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) 39 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
40 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) 40 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
41 ; ≈-cong = cong1 41 ; ≈-cong = cong1
42 } 42 }
43 } where 43 } where
44 cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → 44 cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} →
45 Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier Mono) → x) f ≈ map (λ (x : Carrier Mono) → x) g ] 45 Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier M) → x) f ≈ map (λ (x : Carrier M) → x) g ]
46 cong1 _≡_.refl = _≡_.refl 46 cong1 _≡_.refl = _≡_.refl
47 47
48 open Functor 48 open Functor
49 49
50 Lemma-MM1 : {a b : Obj A} {f : Hom A a b} → 50 Lemma-MM1 : {a b : Obj A} {f : Hom A a b} →
51 A [ A [ FMap T f o (λ x → ε Mono , x) ] ≈ 51 A [ A [ FMap T f o (λ x → ε M , x) ] ≈
52 A [ (λ x → ε Mono , x) o f ] ] 52 A [ (λ x → ε M , x) o f ] ]
53 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in 53 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in
54 begin 54 begin
55 FMap T f o (λ x → ε Mono , x) 55 FMap T f o (λ x → ε M , x)
56 ≈⟨⟩ 56 ≈⟨⟩
57 (λ x → ε Mono , x) o f 57 (λ x → ε M , x) o f
58 ∎ 58 ∎
59 59
60 -- η : a → (ε,a) 60 -- η : a → (ε,a)
61 η : NTrans A A identityFunctor T 61 η : NTrans A A identityFunctor T
62 η = record { 62 η = record {
63 TMap = λ a → λ(x : a) → ( ε Mono , x ) ; 63 TMap = λ a → λ(x : a) → ( ε M , x ) ;
64 isNTrans = record { 64 isNTrans = record {
65 commute = Lemma-MM1 65 commute = Lemma-MM1
66 } 66 }
67 } 67 }
68 68
69 -- μ : (m,(m',a)) → (m*m,a) 69 -- μ : (m,(m',a)) → (m*m,a)
70 70
71 muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a ) 71 muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a )
72 muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m m' , x ) 72 muMap a ( m , ( m' , x ) ) = ( _∙_ M m m' , x )
73 73
74 Lemma-MM2 : {a b : Obj A} {f : Hom A a b} → 74 Lemma-MM2 : {a b : Obj A} {f : Hom A a b} →
75 A [ A [ FMap T f o (λ x → muMap a x) ] ≈ 75 A [ A [ FMap T f o (λ x → muMap a x) ] ≈
76 A [ (λ x → muMap b x) o FMap (T ○ T) f ] ] 76 A [ (λ x → muMap b x) o FMap (T ○ T) f ] ]
77 Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in 77 Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in
92 open NTrans 92 open NTrans
93 93
94 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) 94 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x )
95 Lemma-MM33 = _≡_.refl 95 Lemma-MM33 = _≡_.refl
96 96
97 Lemma-MM34 : ∀{ x : Carrier Mono } → ( (Mono ∙ ε Mono) x ≡ x ) 97 Lemma-MM34 : ∀{ x : Carrier M } → ( (M ∙ ε M) x ≡ x )
98 Lemma-MM34 {x} = (( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x ) 98 Lemma-MM34 {x} = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
99 99
100 Lemma-MM35 : ∀{ x : Carrier Mono } → ((Mono ∙ x) (ε Mono)) ≡ x 100 Lemma-MM35 : ∀{ x : Carrier M } → ((M ∙ x) (ε M)) ≡ x
101 Lemma-MM35 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid Mono )) ) x 101 Lemma-MM35 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x
102 102
103 Lemma-MM36 : ∀{ x y z : Carrier Mono } → ((Mono ∙ (Mono ∙ x) y) z) ≡ (_∙_ Mono x (_∙_ Mono y z ) ) 103 Lemma-MM36 : ∀{ x y z : Carrier M } → ((M ∙ (M ∙ x) y) z) ≡ (_∙_ M x (_∙_ M y z ) )
104 Lemma-MM36 {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono )) x y z 104 Lemma-MM36 {x} {y} {z} = ( IsMonoid.assoc ( isMonoid M )) x y z
105 105
106 -- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming ) 106 -- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming )
107 postulate Extensionarity : {f g : Carrier Mono → Carrier Mono } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g ) 107 postulate Extensionarity : {f g : Carrier M → Carrier M } → (∀ {x} → (f x ≡ g x)) → ( f ≡ g )
108 108
109 postulate Extensionarity3 : {f g : Carrier Mono → Carrier Mono → Carrier Mono → Carrier Mono } → 109 postulate Extensionarity3 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } →
110 (∀{x y z} → f x y z ≡ g x y z ) → ( f ≡ g ) 110 (∀{x y z} → f x y z ≡ g x y z ) → ( f ≡ g )
111 111
112 Lemma-MM9 : ( λ(x : Carrier Mono) → ( Mono ∙ ε Mono ) x ) ≡ ( λ(x : Carrier Mono) → x ) 112 Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x )
113 Lemma-MM9 = Extensionarity Lemma-MM34 113 Lemma-MM9 = Extensionarity Lemma-MM34
114 114
115 Lemma-MM10 : ( λ x → ((Mono ∙ x) (ε Mono))) ≡ ( λ x → x ) 115 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x )
116 Lemma-MM10 = Extensionarity Lemma-MM35 116 Lemma-MM10 = Extensionarity Lemma-MM35
117 117
118 Lemma-MM11 : (λ x y z → ((Mono ∙ (Mono ∙ x) y) z)) ≡ (λ x y z → ( _∙_ Mono x (_∙_ Mono y z ) )) 118 Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z)) ≡ (λ x y z → ( _∙_ M x (_∙_ M y z ) ))
119 Lemma-MM11 = Extensionarity3 Lemma-MM36 119 Lemma-MM11 = Extensionarity3 Lemma-MM36
120 120
121 MonoidMonad : Monad A T η μ 121 MonoidMonad : Monad A T η μ
122 MonoidMonad = record { 122 MonoidMonad = record {
123 isMonad = record { 123 isMonad = record {
129 Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] 129 Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
130 Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in 130 Lemma-MM3 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
131 begin 131 begin
132 TMap μ a o TMap η ( FObj T a ) 132 TMap μ a o TMap η ( FObj T a )
133 ≈⟨⟩ 133 ≈⟨⟩
134 ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x )) 134 ( λ x → ((M ∙ ε M) (proj₁ x) , proj₂ x ))
135 ≈⟨ cong ( λ f → ( λ x → ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩ 135 ≈⟨ cong ( λ f → ( λ x → ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩
136 ( λ (x : FObj T a) → (proj₁ x) , proj₂ x ) 136 ( λ (x : FObj T a) → (proj₁ x) , proj₂ x )
137 ≈⟨⟩ 137 ≈⟨⟩
138 ( λ x → x ) 138 ( λ x → x )
139 ≈⟨⟩ 139 ≈⟨⟩
142 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] 142 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
143 Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in 143 Lemma-MM4 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
144 begin 144 begin
145 TMap μ a o (FMap T (TMap η a )) 145 TMap μ a o (FMap T (TMap η a ))
146 ≈⟨⟩ 146 ≈⟨⟩
147 ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x ) 147 ( λ x → (M ∙ proj₁ x) (ε M) , proj₂ x )
148 ≈⟨ cong ( λ f → ( λ x → ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩ 148 ≈⟨ cong ( λ f → ( λ x → ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩
149 ( λ x → (proj₁ x) , proj₂ x ) 149 ( λ x → (proj₁ x) , proj₂ x )
150 ≈⟨⟩ 150 ≈⟨⟩
151 ( λ x → x ) 151 ( λ x → x )
152 ≈⟨⟩ 152 ≈⟨⟩
155 Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] 155 Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
156 Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in 156 Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
157 begin 157 begin
158 TMap μ a o TMap μ ( FObj T a ) 158 TMap μ a o TMap μ ( FObj T a )
159 ≈⟨⟩ 159 ≈⟨⟩
160 ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) 160 ( λ x → (M ∙ (M ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
161 ≈⟨ cong ( λ f → ( λ x → 161 ≈⟨ cong ( λ f → ( λ x →
162 (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x))) )) , proj₂ (proj₂ (proj₂ x)) ) 162 (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x))) )) , proj₂ (proj₂ (proj₂ x)) )
163 )) Lemma-MM11 ⟩ 163 )) Lemma-MM11 ⟩
164 ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) 164 ( λ x → (M ∙ proj₁ x) ((M ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
165 ≈⟨⟩ 165 ≈⟨⟩
166 TMap μ a o FMap T (TMap μ a) 166 TMap μ a o FMap T (TMap μ a)
167 ∎ 167 ∎
168 168
169 169
170 F : (m : Carrier M) -> { a b : Obj A } -> ( f : a -> b ) -> Hom A a ( FObj T b )
171 F m {a} {b} f = \(x : a ) -> ( m , ( f x) )
170 172
173 postulate m m' : Carrier M
174 postulate a b c' : Obj A
175 postulate f : b -> c'
176 postulate g : a -> b
177
178 LemmaMM12 = Monad.join MonoidMonad (F m f) (F m' g)
179
180 open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad}
181
182