Mercurial > hg > Members > kono > Proof > category

comparison src/Definitions.agda @ 1112:0e750446e463

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Nov 2023 08:49:21 +0900
parents 45de2b31bf02
children
comparison
equal deleted inserted replaced
1111:73c72679421c 1112:0e750446e463
238 } 238 }
239 } where 239 } where
240 commute : {a b : Obj A} {f : Hom A a b} 240 commute : {a b : Obj A} {f : Hom A a b}
241 → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ] 241 → C [ C [ ( FMap H (FMap F f )) o ( TMap n (FObj F a)) ] ≈ C [ (TMap n (FObj F b )) o (FMap G (FMap F f)) ] ]
242 commute {a} {b} {f} = IsNTrans.commute ( isNTrans n) 242 commute {a} {b} {f} = IsNTrans.commute ( isNTrans n)
243
244 record SObj {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (P : Obj A → Set ℓ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
245 field
246 s : Obj A
247 p : P s
248
249 FullSubCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (P : Obj A → Set ℓ ) → Category (suc c₁ ⊔ suc c₂ ⊔ suc ℓ) c₂ ℓ
250 FullSubCategory A P = record {
251 Obj = SObj A P
252 ; Hom = λ a b → Hom A (SObj.s a) (SObj.s b) -- full
253 ; _o_ = λ f g → A [ f o g ]
254 ; _≈_ = λ f g → A [ f ≈ g ]
255 ; Id = λ {a} → id1 A (SObj.s a)
256 ; isCategory = record {
257 isEquivalence = IsCategory.isEquivalence (Category.isCategory A )
258 ; identityL = idL
259 ; identityR = idR
260 ; o-resp-≈ = resp
261 ; associative = assoc
262 }
263 } where open ≈-Reasoning A
264
265 InclusiveFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (P : Obj A → Set ℓ ) → Functor (FullSubCategory A P) A
266 InclusiveFunctor A P = record {
267 FObj = λ x → SObj.s x
268 ; FMap = λ {a} {b} f → f
269 ; isFunctor = record {
270 ≈-cong = λ eq → eq
271 ; identity = refl-hom
272 ; distr = refl-hom
273 }
274 } where open ≈-Reasoning A
243 275
244 -- T ≃ (U_R ○ F_R) 276 -- T ≃ (U_R ○ F_R)
245 -- μ = U_R ε F_R 277 -- μ = U_R ε F_R
246 -- nat-ε 278 -- nat-ε
247 -- nat-η -- same as η but has different types 279 -- nat-η -- same as η but has different types
523 plimit : { Γ : Functor I A } → ( limita : Limit I A Γ ) → Limit I C (G ○ Γ ) 555 plimit : { Γ : Functor I A } → ( limita : Limit I A Γ ) → Limit I C (G ○ Γ )
524 plimit {Γ} limita = record { a0 = (FObj G (a0 limita )) 556 plimit {Γ} limita = record { a0 = (FObj G (a0 limita ))
525 ; t0 = LimitNat I A C Γ (a0 limita ) (t0 limita) G 557 ; t0 = LimitNat I A C Γ (a0 limita ) (t0 limita) G
526 ; isLimit = preserve Γ limita } 558 ; isLimit = preserve Γ limita }
527 559
528 record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 560 record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
529 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where 561 field
530 field 562 climit : { I : Category c₁' c₂' ℓ' } ( Γ : Functor I A ) → Limit I A Γ
531 climit : ( Γ : Functor I A ) → Limit I A Γ
532 cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct I A fi -- c₁ should be a free level 563 cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct I A fi -- c₁ should be a free level
533 cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g 564 cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g
534 open Limit 565 open Limit
535 limit-c : ( Γ : Functor I A ) → Obj A 566 limit-c : {I : Category c₁' c₂' ℓ' } ( Γ : Functor I A ) → Obj A
536 limit-c Γ = a0 ( climit Γ) 567 limit-c Γ = a0 ( climit Γ)
537 limit-u : ( Γ : Functor I A ) → NTrans I A ( K I A (limit-c Γ )) Γ 568 limit-u : {I : Category c₁' c₂' ℓ' } ( Γ : Functor I A ) → NTrans I A ( K I A (limit-c Γ )) Γ
538 limit-u Γ = t0 ( climit Γ) 569 limit-u Γ = t0 ( climit Γ)
539 open Equalizer 570 open Equalizer
540 equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A 571 equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A
541 equalizer-p f g = equalizer-c (cequalizer f g ) 572 equalizer-p f g = equalizer-c (cequalizer f g )
542 equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a 573 equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a