Mercurial > hg > Members > kono > Proof > category

comparison cat-utility.agda @ 300:d6a6dd305da2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arrow and lambda fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Sep 2013 14:01:07 +0900
parents 2ff44ee3cb32
children 702adc45704f
comparison
equal deleted inserted replaced
299:8c72f5284bc8 300:d6a6dd305da2
104 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) 104 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c )
105 join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] 105 join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ]
106 106
107 107
108 Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') 108 Functor*Nat : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
109 (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○ G) (F ○ H) 109 (F : Functor B C) → { G H : Functor A B } → ( n : NTrans A B G H ) → NTrans A C (F ○ G) (F ○ H)
110 Functor*Nat A {B} C F {G} {H} n = record { 110 Functor*Nat A {B} C F {G} {H} n = record {
111 TMap = \a -> FMap F (TMap n a) 111 TMap = λ a → FMap F (TMap n a)
112 ; isNTrans = record { 112 ; isNTrans = record {
113 commute = commute 113 commute = commute
114 } 114 }
115 } where 115 } where
116 commute : {a b : Obj A} {f : Hom A a b} 116 commute : {a b : Obj A} {f : Hom A a b}
125 ≈⟨ distr F ⟩ 125 ≈⟨ distr F ⟩
126 (FMap F (TMap n b )) o (FMap F (FMap G f)) 126 (FMap F (TMap n b )) o (FMap F (FMap G f))
127 ∎ 127 ∎
128 128
129 Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'') 129 Nat*Functor : {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
130 { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○ F) (H ○ F) 130 { G H : Functor B C } → ( n : NTrans B C G H ) → (F : Functor A B) → NTrans A C (G ○ F) (H ○ F)
131 Nat*Functor A {B} C {G} {H} n F = record { 131 Nat*Functor A {B} C {G} {H} n F = record {
132 TMap = \a -> TMap n (FObj F a) 132 TMap = λ a → TMap n (FObj F a)
133 ; isNTrans = record { 133 ; isNTrans = record {
134 commute = commute 134 commute = commute
135 } 135 }
136 } where 136 } where
137 commute : {a b : Obj A} {f : Hom A a b} 137 commute : {a b : Obj A} {f : Hom A a b}
154 { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) } 154 { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) }
155 ( Adj : Adjunction A B UR FR ηR εR ) 155 ( Adj : Adjunction A B UR FR ηR εR )
156 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where 156 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
157 field 157 field
158 T=UF : T ≃ (UR ○ FR) 158 T=UF : T ≃ (UR ○ FR)
159 μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] 159 μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
160 -- ηR=η : {x : Obj A } -> A [ TMap ηR x ≈ TMap η x ] -- We need T -> UR FR conversion 160 -- ηR=η : {x : Obj A } → A [ TMap ηR x ≈ TMap η x ] -- We need T → UR FR conversion
161 -- μR=μ : {x : Obj A } -> A [ TMap μR x ≈ TMap μ x ] 161 -- μR=μ : {x : Obj A } → A [ TMap μR x ≈ TMap μ x ]
162 162
163 163
164 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where 164 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
165 field 165 field
166 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] 166 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
176 -- 176 --
177 -- c 177 -- c
178 -- f | g 178 -- f | g
179 -- |f×g 179 -- |f×g
180 -- v 180 -- v
181 -- a <-------- ab ----------> b 181 -- a <-------- ab ---------→ b
182 -- π1 π2 182 -- π1 π2
183 183
184 184
185 record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) 185 record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A)
186 ( π1 : Hom A ab a ) 186 ( π1 : Hom A ab a )
199 pi2 : Hom A ab b 199 pi2 : Hom A ab b
200 pi2 = π2 200 pi2 = π2
201 201
202 -- Pullback 202 -- Pullback
203 -- f 203 -- f
204 -- a -------> c 204 -- a ------→ c
205 -- ^ ^ 205 -- ^ ^
206 -- π1 | |g 206 -- π1 | |g
207 -- | | 207 -- | |
208 -- ab -------> b 208 -- ab ------→ b
209 -- ^ π2 209 -- ^ π2
210 -- | 210 -- |
211 -- d 211 -- d
212 -- 212 --
213 record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A) 213 record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A)