Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 3:dce706edd66b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Kleisli
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Jul 2013 07:27:57 +0900
parents 7ce421d5ee2b
children 05087d3aeac0
comparison
equal deleted inserted replaced
2:7ce421d5ee2b 3:dce706edd66b
31 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A)) 31 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
32 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where 32 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
33 field 33 field
34 naturality : {a b : Obj D} {f : Hom D a b} 34 naturality : {a b : Obj D} {f : Hom D a b}
35 → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ] 35 → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ]
36 -- how to write uniquness?
37 -- uniqness : {d : Obj D} 36 -- uniqness : {d : Obj D}
38 -- → ∃{e : Trans d} -> ∀{a : Trans d} → C [ e ≈ a ] 37 -- → C [ Trans d ≈ Trans d ]
39 38
40 39
41 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) 40 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
42 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where 41 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
43 field 42 field
62 ( T : Functor A A ) 61 ( T : Functor A A )
63 ( η : NTrans A A identityFunctor T ) 62 ( η : NTrans A A identityFunctor T )
64 ( μ : NTrans A A (T ○ T) T) 63 ( μ : NTrans A A (T ○ T) T)
65 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where 64 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
66 field 65 field
67 assoc : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] 66 assoc : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ]
68 unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] 67 unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
69 unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] 68 unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
70 69
71 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) 70 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
72 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where 71 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
73 field 72 field
74 isMonad : IsMonad A T η μ 73 isMonad : IsMonad A T η μ
86 85
87 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} 86 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
88 -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] 87 -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
89 Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a ) 88 Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a )
90 89
90 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
91 { T : Functor A A }
92 { η : NTrans A A identityFunctor T }
93 { μ : NTrans A A (T ○ T) T }
94 { a : Obj A } ->
95 ( M : Monad A T η μ )
96 -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
97 Lemma5 = \m -> IsMonad.unity1 ( isMonad m )
98
99 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
100 { T : Functor A A }
101 { η : NTrans A A identityFunctor T }
102 { μ : NTrans A A (T ○ T) T }
103 { a : Obj A } ->
104 ( M : Monad A T η μ )
105 -> A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
106 Lemma6 = \m -> IsMonad.unity2 ( isMonad m )
107
108 -- T = M x A
109
110 -- open import Data.Product -- renaming (_×_ to _*_)
111
112 -- MonoidalMonad :
113 -- MonoidalMonad = record { Obj = M × A
114 -- ; Hom = _⟶_
115 -- ; Id = IdProd
116 -- ; _o_ = _∘_
117 -- ; _≈_ = _≈_
118 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ}
119 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
120 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
121 -- }
122 -- ; identityL = identityL
123 -- ; identityR = identityR
124 -- ; o-resp-≈ = o-resp-≈
125 -- ; associative = associative
126 -- }
127 -- }
128
129
91 -- nat of η 130 -- nat of η
92 131
93 132
94 -- g ○ f = μ(c) T(g) f 133 -- g ○ f = μ(c) T(g) f
95
96 -- h ○ (g ○ f) = (h ○ g) ○ f 134 -- h ○ (g ○ f) = (h ○ g) ○ f
97 135
98 -- η(b) ○ f = f 136 -- η(b) ○ f = f
99 -- f ○ η(a) = f 137 -- f ○ η(a) = f
100 138
101 139
140 record Kleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
141 { T : Functor A A }
142 { η : NTrans A A identityFunctor T }
143 { μ : NTrans A A (T ○ T) T }
144 { M : Monad A T η μ } : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
145 infix 9 _*_
146 _*_ : { a b c : Obj A } ->
147 ( Hom A b ( FObj T c )) -> ( Hom A a ( FObj T b)) -> Hom A a ( FObj T c )
148 g * f = A [ Trans μ ({!!} (Category.cod A g)) o A [ FMap T g o f ] ]
149
150
151
152 -- Kleisli :
153 -- Kleisli = record { Hom =
154 -- ; Hom = _⟶_
155 -- ; Id = IdProd
156 -- ; _o_ = _∘_
157 -- ; _≈_ = _≈_
158 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ}
159 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
160 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
161 -- }
162 -- ; identityL = identityL
163 -- ; identityR = identityR
164 -- ; o-resp-≈ = o-resp-≈
165 -- ; associative = associative
166 -- }
167 -- }