Mercurial > hg > Members > kono > Proof > category

comparison cat-utility.agda @ 691:917e51be9bbf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
change argument of Limit and K
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 09:56:40 +0900
parents 3d41a8edbf63
children 7a6ee564e3a8
comparison
equal deleted inserted replaced
690:3d41a8edbf63 691:917e51be9bbf
219 ----- 219 -----
220 -- 220 --
221 -- product on arbitrary index 221 -- product on arbitrary index
222 -- 222 --
223 223
224 record IsIProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) 224 record IsIProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ )
225 ( p : Obj A ) -- product 225 ( p : Obj A ) -- product
226 ( ai : I → Obj A ) -- families 226 ( ai : I → Obj A ) -- families
227 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections 227 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections
228 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where 228 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
229 field 229 field
247 qi i 247 qi i
248 ∎ ) ⟩ 248 ∎ ) ⟩
249 iproduct qi 249 iproduct qi
250 ∎ 250 ∎
251 251
252 record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) (ai : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where 252 record IProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ ) (ai : I → Obj A) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
253 field 253 field
254 iprod : Obj A 254 iprod : Obj A
255 pi : (i : I ) → Hom A iprod ( ai i ) 255 pi : (i : I ) → Hom A iprod ( ai i )
256 isIProduct : IsIProduct A I iprod ai pi 256 isIProduct : IsIProduct I A iprod ai pi
257 257
258 258
259 -- Pullback 259 -- Pullback
260 -- f 260 -- f
261 -- a ------→ c 261 -- a ------→ c
297 -- 297 --
298 ----- 298 -----
299 299
300 -- Constancy Functor 300 -- Constancy Functor
301 301
302 K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) 302 K : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( A : Category c₁'' c₂'' ℓ'' )
303 → ( a : Obj A ) → Functor I A 303 → ( a : Obj A ) → Functor I A
304 K A I a = record { 304 K I A a = record {
305 FObj = λ i → a ; 305 FObj = λ i → a ;
306 FMap = λ f → id1 A a ; 306 FMap = λ f → id1 A a ;
307 isFunctor = let open ≈-Reasoning (A) in record { 307 isFunctor = let open ≈-Reasoning (A) in record {
308 ≈-cong = λ f=g → refl-hom 308 ≈-cong = λ f=g → refl-hom
309 ; identity = refl-hom 309 ; identity = refl-hom
310 ; distr = sym idL 310 ; distr = sym idL
311 } 311 }
312 } 312 }
313 313
314 314
315 record IsLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 315 record IsLimit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
316 (a0 : Obj A ) (t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where 316 (a0 : Obj A ) (t0 : NTrans I A ( K I A a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
317 field 317 field
318 limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0 318 limit : ( a : Obj A ) → ( t : NTrans I A ( K I A a ) Γ ) → Hom A a a0
319 t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } → 319 t0f=t : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → ∀ { i : Obj I } →
320 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] 320 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ]
321 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → 321 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
322 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] 322 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ]
323 323
324 record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 324 record Limit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
325 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where 325 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
326 field 326 field
327 a0 : Obj A 327 a0 : Obj A
328 t0 : NTrans I A ( K A I a0 ) Γ 328 t0 : NTrans I A ( K I A a0 ) Γ
329 isLimit : IsLimit A I Γ a0 t0 329 isLimit : IsLimit I A Γ a0 t0
330 330
331 LimitNat : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} 331 LimitNat : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( B : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level}
332 ( C : Category c₁'' c₂'' ℓ'' ) 332 ( C : Category c₁'' c₂'' ℓ'' )
333 ( Γ : Functor I B ) 333 ( Γ : Functor I B )
334 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → 334 ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) →
335 ( U : Functor B C) → NTrans I C ( K C I (FObj U lim) ) (U ○ Γ) 335 ( U : Functor B C) → NTrans I C ( K I C (FObj U lim) ) (U ○ Γ)
336 LimitNat B I C Γ lim tb U = record { 336 LimitNat I B C Γ lim tb U = record {
337 TMap = TMap (Functor*Nat I C U tb) ; 337 TMap = TMap (Functor*Nat I C U tb) ;
338 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin 338 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (C) in begin
339 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a 339 FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a
340 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩ 340 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
341 TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f 341 TMap (Functor*Nat I C U tb) b o FMap (U ○ K I B lim) f
342 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ 342 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
343 TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f 343 TMap (Functor*Nat I C U tb) b o FMap (K I C (FObj U lim)) f
344 ∎ 344 ∎
345 } } 345 } }
346 346
347 open Limit 347 open Limit
348 record LimitPreserve { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 348 record LimitPreserve { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' )
349 { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' ) 349 { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' )
350 (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where 350 (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where
351 field 351 field
352 preserve : ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → 352 preserve : ( Γ : Functor I A ) → ( limita : Limit I A Γ ) →
353 IsLimit C I (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat A I C Γ (a0 limita ) (t0 limita) G ) 353 IsLimit I C (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat I A C Γ (a0 limita ) (t0 limita) G )
354 plimit : { Γ : Functor I A } → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ ) 354 plimit : { Γ : Functor I A } → ( limita : Limit I A Γ ) → Limit I C (G ○ Γ )
355 plimit {Γ} limita = record { a0 = (FObj G (a0 limita )) 355 plimit {Γ} limita = record { a0 = (FObj G (a0 limita ))
356 ; t0 = LimitNat A I C Γ (a0 limita ) (t0 limita) G 356 ; t0 = LimitNat I A C Γ (a0 limita ) (t0 limita) G
357 ; isLimit = preserve Γ limita } 357 ; isLimit = preserve Γ limita }
358 358
359 record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 359 record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' )
360 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where 360 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
361 field 361 field
362 climit : ( Γ : Functor I A ) → Limit A I Γ 362 climit : ( Γ : Functor I A ) → Limit I A Γ
363 363
364 record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 364 record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
365 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where 365 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
366 field 366 field
367 climit : ( Γ : Functor I A ) → Limit A I Γ 367 climit : ( Γ : Functor I A ) → Limit I A Γ
368 cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct A I fi -- c₁ should be a free level 368 cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct I A fi -- c₁ should be a free level
369 cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g 369 cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g
370 open Limit 370 open Limit
371 limit-c : ( Γ : Functor I A ) → Obj A 371 limit-c : ( Γ : Functor I A ) → Obj A
372 limit-c Γ = a0 ( climit Γ) 372 limit-c Γ = a0 ( climit Γ)
373 limit-u : ( Γ : Functor I A ) → NTrans I A ( K A I (limit-c Γ )) Γ 373 limit-u : ( Γ : Functor I A ) → NTrans I A ( K I A (limit-c Γ )) Γ
374 limit-u Γ = t0 ( climit Γ) 374 limit-u Γ = t0 ( climit Γ)
375 open Equalizer 375 open Equalizer
376 equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A 376 equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A
377 equalizer-p f g = equalizer-c (cequalizer f g ) 377 equalizer-p f g = equalizer-c (cequalizer f g )
378 equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a 378 equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a