Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 291:c8e26650ddf9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit preserving ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 25 Sep 2013 18:07:58 +0900
parents 1f897357ec6c
children a84fab7cf46a
comparison
equal deleted inserted replaced
290:1f897357ec6c 291:c8e26650ddf9
132 -- 132 --
133 ----- 133 -----
134 134
135 -- Constancy Functor 135 -- Constancy Functor
136 136
137 K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → ( a : Obj A ) → Functor I A 137 K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' )
138 K I a = record { 138 → ( a : Obj A ) → Functor I A
139 K A I a = record {
139 FObj = λ i → a ; 140 FObj = λ i → a ;
140 FMap = λ f → id1 A a ; 141 FMap = λ f → id1 A a ;
141 isFunctor = let open ≈-Reasoning (A) in record { 142 isFunctor = let open ≈-Reasoning (A) in record {
142 ≈-cong = λ f=g → refl-hom 143 ≈-cong = λ f=g → refl-hom
143 ; identity = refl-hom 144 ; identity = refl-hom
145 } 146 }
146 } 147 }
147 148
148 open NTrans 149 open NTrans
149 150
150 record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 151 record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
151 ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where 152 ( a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
152 field 153 field
153 limit : ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0 154 limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
154 t0f=t : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } → 155 t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
155 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] 156 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ]
156 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → 157 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
157 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] 158 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ]
158 A0 : Obj A 159 A0 : Obj A
159 A0 = a0 160 A0 = a0
160 T0 : NTrans I A ( K I a0 ) Γ 161 T0 : NTrans I A ( K A I a0 ) Γ
161 T0 = t0 162 T0 = t0
162 163
163 -------------------------------- 164 --------------------------------
164 -- 165 --
165 -- If we have two limits on c and c', there are isomorphic pair h, h' 166 -- If we have two limits on c and c', there are isomorphic pair h, h'
166 167
167 open Limit 168 open Limit
168 169
169 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 170 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
170 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) 171 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
171 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) 172 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' )
172 → Hom A a0 a0' 173 → Hom A a0 a0'
173 iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0 174 iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
174 175
175 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 176 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
176 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) 177 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
177 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) 178 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' )
178 → Hom A a0' a0 179 → Hom A a0' a0
179 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0' 180 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
180 181
181 182
182 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 183 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
183 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) 184 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ )
184 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) → ∀{ i : Obj I } → 185 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) → ∀{ i : Obj I } →
185 A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ] 186 A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ]
186 iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin 187 iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin
187 limit lim' a0 t0 o limit lim a0' t0' 188 limit lim' a0 t0 o limit lim a0' t0'
188 ≈↑⟨ limit-uniqueness lim' ( λ {i} → ( begin 189 ≈↑⟨ limit-uniqueness lim' ( λ {i} → ( begin
189 TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' ) 190 TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
208 -- 209 --
209 -- Contancy Functor 210 -- Contancy Functor
210 211
211 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I ) 212 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I )
212 KI { c₁'} {c₂'} {ℓ'} I = record { 213 KI { c₁'} {c₂'} {ℓ'} I = record {
213 FObj = λ a → K I a ; 214 FObj = λ a → K A I a ;
214 FMap = λ f → record { -- NTrans I A (K I a) (K I b) 215 FMap = λ f → record { -- NTrans I A (K A I a) (K A I b)
215 TMap = λ a → f ; 216 TMap = λ a → f ;
216 isNTrans = record { 217 isNTrans = record {
217 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f 218 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
218 } 219 }
219 } ; 220 } ;
222 ; identity = refl-hom 223 ; identity = refl-hom
223 ; distr = refl-hom 224 ; distr = refl-hom
224 } 225 }
225 } where 226 } where
226 commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) → 227 commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
227 A [ A [ FMap (K I b') f₁ o f ] ≈ A [ f o FMap (K I a') f₁ ] ] 228 A [ A [ FMap (K A I b') f₁ o f ] ≈ A [ f o FMap (K A I a') f₁ ] ]
228 commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin 229 commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin
229 FMap (K I b') f₁ o f 230 FMap (K A I b') f₁ o f
230 ≈⟨ idL ⟩ 231 ≈⟨ idL ⟩
231 f 232 f
232 ≈↑⟨ idR ⟩ 233 ≈↑⟨ idR ⟩
233 f o FMap (K I a') f₁ 234 f o FMap (K A I a') f₁
234 ∎ 235 ∎
235 236
236 237
237 --------- 238 ---------
238 -- 239 --
241 -- F = KI I : Functor A (A ^ I) 242 -- F = KI I : Functor A (A ^ I)
242 -- U = λ b → A0 (lim b {a0 b} {t0 b} 243 -- U = λ b → A0 (lim b {a0 b} {t0 b}
243 -- ε = λ b → T0 ( lim b {a0 b} {t0 b} ) 244 -- ε = λ b → T0 ( lim b {a0 b} {t0 b} )
244 245
245 limit2couniv : 246 limit2couniv :
246 ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 ) 247 ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 )
247 → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K I (a0 b) ) b ) 248 → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K A I (a0 b) ) b )
248 → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) ) 249 → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) )
249 limit2couniv lim a0 t0 = record { -- F U ε 250 limit2couniv lim a0 t0 = record { -- F U ε
250 _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η 251 _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η
251 iscoUniversalMapping = record { 252 iscoUniversalMapping = record {
252 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; 253 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
276 277
277 open coUniversalMapping 278 open coUniversalMapping
278 279
279 univ2limit : 280 univ2limit :
280 ( U : Obj (A ^ I ) → Obj A ) 281 ( U : Obj (A ^ I ) → Obj A )
281 ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K I (U b)) b ) 282 ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b )
282 ( univ : coUniversalMapping A (A ^ I) (KI I) U (ε) ) → 283 ( univ : coUniversalMapping A (A ^ I) (KI I) U (ε) ) →
283 ( Γ : Functor I A ) → Limit I Γ (U Γ) (ε Γ) 284 ( Γ : Functor I A ) → Limit A I Γ (U Γ) (ε Γ)
284 univ2limit U ε univ Γ = record { 285 univ2limit U ε univ Γ = record {
285 limit = λ a t → limit1 a t ; 286 limit = λ a t → limit1 a t ;
286 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; 287 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
287 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f 288 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
288 } where 289 } where
289 limit1 : (a : Obj A) → NTrans I A (K I a) Γ → Hom A a (U Γ) 290 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ)
290 limit1 a t = _*' univ {_} {a} t 291 limit1 a t = _*' univ {_} {a} t
291 t0f=t1 : {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} → 292 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
292 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ] 293 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
293 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin 294 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
294 TMap (ε Γ) i o limit1 a t 295 TMap (ε Γ) i o limit1 a t
295 ≈⟨⟩ 296 ≈⟨⟩
296 TMap (ε Γ) i o _*' univ {Γ} {a} t 297 TMap (ε Γ) i o _*' univ {Γ} {a} t
297 ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩ 298 ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩
298 TMap t i 299 TMap t i
299 ∎ 300 ∎
300 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (U Γ)} 301 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)}
301 → ( ∀ { i : Obj I } → A [ A [ TMap (ε Γ) i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ] 302 → ( ∀ { i : Obj I } → A [ A [ TMap (ε Γ) i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
302 limit-uniqueness1 {a} {t} {f} εf=t = let open ≈-Reasoning (A) in begin 303 limit-uniqueness1 {a} {t} {f} εf=t = let open ≈-Reasoning (A) in begin
303 _*' univ t 304 _*' univ t
304 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩ 305 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩
305 f 306 f
344 -- k ( product pi ) Γ f 345 -- k ( product pi ) Γ f
345 -- Γ f o ε i = ε j 346 -- Γ f o ε i = ε j
346 -- 347 --
347 -- 348 --
348 349
350 -- pi-ε -- : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )
351 -- → IProduct {c₁'} A (Obj I) p ai pi )
352 -- ( lim p : Obj A ) ( e : Hom A lim p )
353 -- ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
354 -- { i : Obj I } → { q : ( i : Obj I ) → Hom A p (FObj Γ i) } → A [ proj i ≈ q i ]
355 -- pi-ε prod lim p e proj {i} {q} = let open ≈-Reasoning (A) in begin
356 -- proj i
357 -- ≈↑⟨ idR ⟩
358 -- proj i o id1 A p
359 -- ≈⟨ cdr {!!} ⟩
360 -- proj i o product (prod p (FObj Γ) proj) q
361 -- ≈⟨ pif=q (prod p (FObj Γ) proj) q ⟩
362 -- q i
363 -- ∎
364
365
349 limit-ε : 366 limit-ε :
350 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) 367 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )
351 → IProduct {c₁'} A (Obj I) p ai pi ) 368 → IProduct {c₁'} A (Obj I) p ai pi )
352 ( lim p : Obj A ) ( e : Hom A lim p ) 369 ( lim p : Obj A ) ( e : Hom A lim p )
353 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → 370 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
354 NTrans I A (K I lim) Γ 371 NTrans I A (K A I lim) Γ
355 limit-ε prod lim p e proj = record { 372 limit-ε prod lim p e proj = record {
356 TMap = tmap ; 373 TMap = tmap ;
357 isNTrans = record { 374 isNTrans = record {
358 commute = commute1 375 commute = commute1
359 } 376 }
360 } where 377 } where
361 tmap : (i : Obj I) → Hom A (FObj (K I lim) i) (FObj Γ i) 378 tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
362 tmap i = A [ proj i o e ] 379 tmap i = A [ proj i o e ]
363 commute1 : {i j : Obj I} {f : Hom I i j} → 380 commute1 : {i j : Obj I} {f : Hom I i j} →
364 A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K I lim) f ] ] 381 A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ]
365 commute1 {i} {j} {f} = let open ≈-Reasoning (A) in begin 382 commute1 {i} {j} {f} = let open ≈-Reasoning (A) in begin
366 FMap Γ f o tmap i 383 FMap Γ f o tmap i
367 ≈⟨⟩ 384 ≈⟨⟩
368 FMap Γ f o ( proj i o e ) 385 FMap Γ f o ( proj i o e )
369 ≈⟨ assoc ⟩ 386 ≈⟨ assoc ⟩
371 ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ) proj ) {j} ) ⟩ 388 ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ) proj ) {j} ) ⟩
372 proj j o e 389 proj j o e
373 ≈↑⟨ idR ⟩ 390 ≈↑⟨ idR ⟩
374 (proj j o e ) o id1 A lim 391 (proj j o e ) o id1 A lim
375 ≈⟨⟩ 392 ≈⟨⟩
376 tmap j o FMap (K I lim) f 393 tmap j o FMap (K A I lim) f
377 ∎ 394 ∎
378 395
379 limit-from : 396 limit-from :
380 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) 397 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )
381 → IProduct {c₁'} A (Obj I) p ai pi ) 398 → IProduct {c₁'} A (Obj I) p ai pi )
382 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g ) 399 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g )
383 ( lim p : Obj A ) -- limit to be made 400 ( lim p : Obj A ) -- limit to be made
384 ( e : Hom A lim p ) -- existing of equalizer 401 ( e : Hom A lim p ) -- existing of equalizer
385 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually ) 402 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually )
386 → Limit I Γ lim ( limit-ε prod lim p e proj ) 403 → Limit A I Γ lim ( limit-ε prod lim p e proj )
387 limit-from prod eqa lim p e proj = record { 404 limit-from prod eqa lim p e proj = record {
388 limit = λ a t → limit1 a t ; 405 limit = λ a t → limit1 a t ;
389 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; 406 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
390 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f 407 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
391 } where 408 } where
392 limit1 : (a : Obj A) → NTrans I A (K I a) Γ → Hom A a lim 409 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
393 limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom 410 limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom
394 t0f=t1 : {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} → 411 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
395 A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ] 412 A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ]
396 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin 413 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
397 TMap (limit-ε prod lim p e proj ) i o limit1 a t 414 TMap (limit-ε prod lim p e proj ) i o limit1 a t
398 ≈⟨⟩ 415 ≈⟨⟩
399 ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom 416 ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom
402 ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩ 419 ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩
403 proj i o product (prod p (FObj Γ) proj) (TMap t) 420 proj i o product (prod p (FObj Γ) proj) (TMap t)
404 ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩ 421 ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩
405 TMap t i 422 TMap t i
406 ∎ 423 ∎
407 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K I a) Γ} {f : Hom A a lim} 424 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim}
408 → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) → 425 → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) →
409 A [ limit1 a t ≈ f ] 426 A [ limit1 a t ≈ f ]
410 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin 427 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin
411 limit1 a t 428 limit1 a t
412 ≈⟨⟩ 429 ≈⟨⟩
425 product (prod p (FObj Γ) proj) (TMap t) 442 product (prod p (FObj Γ) proj) (TMap t)
426 ∎ ) ⟩ 443 ∎ ) ⟩
427 f 444 f
428 ∎ 445 ∎
429 446
447 ----
448 --
449 -- Adjoint functor preserves limits
450 --
451 --
452
453 open import Category.Cat
454
455 ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B )
456 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) →
457 ( U : Functor B A) → NTrans I A ( K A I (FObj U lim) ) (U ○ Γ)
458 ta1 B Γ lim tb limit U = record {
459 TMap = TMap (Functor*Nat I A U tb) ;
460 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (A) in begin
461 FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a
462 ≈⟨ nat ( Functor*Nat I A U tb ) ⟩
463 TMap (Functor*Nat I A U tb) b o FMap (U ○ K B I lim) f
464 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
465 TMap (Functor*Nat I A U tb) b o FMap (K A I (FObj U lim)) f
466 ∎
467 } }
468
469 adjoint-preseve-limit :
470 { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B )
471 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) →
472 { U : Functor B A } { F : Functor A B }
473 { η : NTrans A A identityFunctor ( U ○ F ) }
474 { ε : NTrans B B ( F ○ U ) identityFunctor } →
475 ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb limit U )
476 adjoint-preseve-limit B Γ lim tb limit {U} {F} {η} {ε} adj = record {
477 limit = λ a t → limit1 a t ;
478 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
479 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
480 } where
481 ta = ta1 B Γ lim tb limit U
482 limit1 : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim)
483 limit1 a t = let open ≈-Reasoning (A) in ?
484 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {i : Obj I} →
485 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ]
486 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in ?
487 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {f : Hom A a (FObj U lim)}
488 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) →
489 A [ limit1 a t ≈ f ]
490 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in ?