diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/Cocomplete/Finitely/Bundle.agda | 19 | ||||
| -rw-r--r-- | Category/Cocomplete/Finitely/Product.agda | 83 | ||||
| -rw-r--r-- | Category/Instance/FinitelyCocompletes.agda | 369 | ||||
| -rw-r--r-- | Category/Instance/One/Properties.agda | 35 | ||||
| -rw-r--r-- | Category/Instance/Properties/FinitelyCocompletes.agda | 208 |
5 files changed, 709 insertions, 5 deletions
diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda index af40895..74f434f 100644 --- a/Category/Cocomplete/Finitely/Bundle.agda +++ b/Category/Cocomplete/Finitely/Bundle.agda @@ -1,12 +1,12 @@ {-# OPTIONS --without-K --safe #-} module Category.Cocomplete.Finitely.Bundle where -open import Level +open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) open import Categories.Category.Core using (Category) open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete) open import Category.Cocomplete.Finitely.SymmetricMonoidal using (module FinitelyCocompleteSymmetricMonoidal) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) - +open import Level using (_⊔_; suc) record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where @@ -17,11 +17,20 @@ record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where open Category U public open FinitelyCocomplete finCo public - open FinitelyCocompleteSymmetricMonoidal finCo using (+-monoidal; +-symmetric) + open FinitelyCocompleteSymmetricMonoidal finCo + using () + renaming (+-monoidal to monoidal; +-symmetric to symmetric) + public symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e symmetricMonoidalCategory = record { U = U - ; monoidal = +-monoidal - ; symmetric = +-symmetric + ; monoidal = monoidal + ; symmetric = symmetric + } + + cocartesianCategory : CocartesianCategory o ℓ e + cocartesianCategory = record + { U = U + ; cocartesian = cocartesian } diff --git a/Category/Cocomplete/Finitely/Product.agda b/Category/Cocomplete/Finitely/Product.agda new file mode 100644 index 0000000..25dc346 --- /dev/null +++ b/Category/Cocomplete/Finitely/Product.agda @@ -0,0 +1,83 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core using (Category) +open import Level using (Level) + +module Category.Cocomplete.Finitely.Product {o ℓ e : Level} {𝒞 𝒟 : Category o ℓ e} where + +open import Categories.Category using (_[_,_]) +open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete) +open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts) +open import Categories.Category.Product using (Product) +open import Categories.Diagram.Coequalizer using (Coequalizer) +open import Categories.Object.Coproduct using (Coproduct) +open import Categories.Object.Initial using (IsInitial; Initial) +open import Data.Product.Base using (_,_; _×_; dmap; zip; map) + +Initial-× : Initial 𝒞 → Initial 𝒟 → Initial (Product 𝒞 𝒟) +Initial-× initial-𝒞 initial-𝒟 = record + { ⊥ = 𝒞.⊥ , 𝒟.⊥ + ; ⊥-is-initial = record + { ! = 𝒞.! , 𝒟.! + ; !-unique = dmap 𝒞.!-unique 𝒟.!-unique + } + } + where + module 𝒞 = Initial initial-𝒞 + module 𝒟 = Initial initial-𝒟 + +Coproducts-× : BinaryCoproducts 𝒞 → BinaryCoproducts 𝒟 → BinaryCoproducts (Product 𝒞 𝒟) +Coproducts-× coproducts-𝒞 coproducts-𝒟 = record { coproduct = coproduct } + where + coproduct : ∀ {(A₁ , B₁) (A₂ , B₂) : _ × _} → Coproduct (Product 𝒞 𝒟) (A₁ , B₁) (A₂ , B₂) + coproduct = record + { A+B = 𝒞.A+B , 𝒟.A+B + ; i₁ = 𝒞.i₁ , 𝒟.i₁ + ; i₂ = 𝒞.i₂ , 𝒟.i₂ + ; [_,_] = zip 𝒞.[_,_] 𝒟.[_,_] + ; inject₁ = 𝒞.inject₁ , 𝒟.inject₁ + ; inject₂ = 𝒞.inject₂ , 𝒟.inject₂ + ; unique = zip 𝒞.unique 𝒟.unique + } + where + module Coprod {𝒞} (coprods : BinaryCoproducts 𝒞) where + open BinaryCoproducts coprods using (coproduct) + open coproduct public + module 𝒞 = Coprod coproducts-𝒞 + module 𝒟 = Coprod coproducts-𝒟 + +Coequalizer-× + : (∀ {A} {B} (f g : 𝒞 [ A , B ]) → Coequalizer 𝒞 f g) + → (∀ {A} {B} (f g : 𝒟 [ A , B ]) → Coequalizer 𝒟 f g) + → ∀ {A} {B} {C} {D} ((f₁ , g₁) (f₂ , g₂) : 𝒞 [ A , B ] × 𝒟 [ C , D ]) + → Coequalizer (Product 𝒞 𝒟) (f₁ , g₁) (f₂ , g₂) +Coequalizer-× coequalizer-𝒞 coequalizer-𝒟 (f₁ , g₁) (f₂ , g₂) = record + { arr = 𝒞.arr , 𝒟.arr + ; isCoequalizer = record + { equality = 𝒞.equality , 𝒟.equality + ; coequalize = map 𝒞.coequalize 𝒟.coequalize + ; universal = 𝒞.universal , 𝒟.universal + ; unique = map 𝒞.unique 𝒟.unique + } + } + where + module 𝒞 = Coequalizer (coequalizer-𝒞 f₁ f₂) + module 𝒟 = Coequalizer (coequalizer-𝒟 g₁ g₂) + +Cocartesian-× : Cocartesian 𝒞 → Cocartesian 𝒟 → Cocartesian (Product 𝒞 𝒟) +Cocartesian-× cocartesian-𝒞 cocartesian-𝒟 = record + { initial = Initial-× 𝒞.initial 𝒟.initial + ; coproducts = Coproducts-× 𝒞.coproducts 𝒟.coproducts + } + where + module 𝒞 = Cocartesian cocartesian-𝒞 + module 𝒟 = Cocartesian cocartesian-𝒟 + +FinitelyCocomplete-× : FinitelyCocomplete 𝒞 → FinitelyCocomplete 𝒟 → FinitelyCocomplete (Product 𝒞 𝒟) +FinitelyCocomplete-× finitelyCocomplete-𝒞 finitelyCocomplete-𝒟 = record + { cocartesian = Cocartesian-× 𝒞.cocartesian 𝒟.cocartesian + ; coequalizer = Coequalizer-× 𝒞.coequalizer 𝒟.coequalizer + } + where + module 𝒞 = FinitelyCocomplete finitelyCocomplete-𝒞 + module 𝒟 = FinitelyCocomplete finitelyCocomplete-𝒟 diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda new file mode 100644 index 0000000..0847165 --- /dev/null +++ b/Category/Instance/FinitelyCocompletes.agda @@ -0,0 +1,369 @@ +{-# OPTIONS --without-K --safe #-} +open import Level using (Level) +module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where + +open import Categories.Category using (_[_,_]) +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Helper using (categoryHelper) +open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products) +open import Categories.Category.Core using (Category) +open import Categories.Category.Instance.Cats using (Cats) +open import Categories.Category.Instance.One using (One; One-⊤) +open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat) +open import Categories.Diagram.Coequalizer using (IsCoequalizer) +open import Categories.Functor using (Functor) renaming (id to idF) +open import Categories.Object.Coproduct using (IsCoproduct) +open import Categories.Object.Initial using (IsInitial) +open import Categories.Object.Product.Core using (Product) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×) +open import Category.Instance.One.Properties using (One-FinitelyCocomplete) +open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′) +open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact) +open import Function.Base using (id; flip) +open import Level using (Level; suc; _⊔_) + +FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) +FinitelyCocompletes = categoryHelper record + { Obj = FinitelyCocompleteCategory o ℓ e + ; _⇒_ = RightExactFunctor + ; _≈_ = λ F G → REF.F F ≃ REF.F G + ; id = idREF + ; _∘_ = ∘-RightExactFunctor + ; assoc = λ {_ _ _ _ F G H} → associator (REF.F F) (REF.F G) (REF.F H) + ; identityˡ = unitorˡ + ; identityʳ = unitorʳ + ; equiv = record + { refl = ≃.refl + ; sym = ≃.sym + ; trans = ≃.trans + } + ; ∘-resp-≈ = _ⓘₕ_ + } + where + module REF = RightExactFunctor + +One-FCC : FinitelyCocompleteCategory o ℓ e +One-FCC = record + { U = One + ; finCo = One-FinitelyCocomplete + } + +_×_ + : FinitelyCocompleteCategory o ℓ e + → FinitelyCocompleteCategory o ℓ e + → FinitelyCocompleteCategory o ℓ e +_×_ 𝒞 𝒟 = record + { U = ProductCat 𝒞.U 𝒟.U + ; finCo = FinitelyCocomplete-× 𝒞.finCo 𝒟.finCo + } + where + module 𝒞 = FinitelyCocompleteCategory 𝒞 + module 𝒟 = FinitelyCocompleteCategory 𝒟 + +module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where + + private + module 𝒞 = FinitelyCocompleteCategory 𝒞 + module 𝒟 = FinitelyCocompleteCategory 𝒟 + module 𝒞×𝒟 = FinitelyCocompleteCategory (𝒞 × 𝒟) + + πˡ-RightExact : IsRightExact (𝒞 × 𝒟) 𝒞 πˡ + πˡ-RightExact = record + { F-resp-⊥ = F-resp-⊥ + ; F-resp-+ = F-resp-+ + ; F-resp-coeq = F-resp-coeq + } + where + F-resp-⊥ + : {(A , B) : 𝒞×𝒟.Obj} + → IsInitial 𝒞×𝒟.U (A , B) + → IsInitial 𝒞.U A + F-resp-⊥ {A , B} initial = record + { ! = λ { {C} → proj₁ (! {C , B}) } + ; !-unique = λ { f → proj₁ (!-unique (f , 𝒟.id)) } + } + where + open IsInitial initial + F-resp-+ + : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj} + {(i₁-c , i₁-d) : 𝒞×𝒟.U [ (C₁ , D₁) , (C₃ , D₃) ]} + {(i₂-c , i₂-d) : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]} + → IsCoproduct (ProductCat 𝒞.U 𝒟.U) (i₁-c , i₁-d) (i₂-c , i₂-d) + → IsCoproduct 𝒞.U i₁-c i₂-c + F-resp-+ {_} {_} {_} {i₁-c , i₁-d} {i₂-c , i₂-d} isCoproduct = record + { [_,_] = λ { h₁ h₂ → proj₁ (copairing (h₁ , i₁-d) (h₂ , i₂-d)) } + ; inject₁ = proj₁ inject₁ + ; inject₂ = proj₁ inject₂ + ; unique = λ { eq₁ eq₂ → proj₁ (unique (eq₁ , 𝒟.identityˡ) (eq₂ , 𝒟.identityˡ)) } + } + where + open IsCoproduct isCoproduct renaming ([_,_] to copairing) + F-resp-coeq + : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj} + {f g : 𝒞×𝒟.U [ (C₁ , D₁) , (C₂ , D₂) ]} + {h : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]} + → IsCoequalizer (ProductCat 𝒞.U 𝒟.U) f g h + → IsCoequalizer 𝒞.U (proj₁ f) (proj₁ g) (proj₁ h) + F-resp-coeq isCoequalizer = record + { equality = proj₁ equality + ; coequalize = λ { eq → proj₁ (coequalize (eq , proj₂ equality)) } + ; universal = proj₁ universal + ; unique = λ { eq → proj₁ (unique (eq , 𝒟.Equiv.sym 𝒟.identityˡ)) } + } + where + open IsCoequalizer isCoequalizer + + πʳ-RightExact : IsRightExact (𝒞 × 𝒟) 𝒟 πʳ + πʳ-RightExact = record + { F-resp-⊥ = F-resp-⊥ + ; F-resp-+ = F-resp-+ + ; F-resp-coeq = F-resp-coeq + } + where + F-resp-⊥ + : {(A , B) : 𝒞×𝒟.Obj} + → IsInitial 𝒞×𝒟.U (A , B) + → IsInitial 𝒟.U B + F-resp-⊥ {A , B} initial = record + { ! = λ { {C} → proj₂ (! {A , C}) } + ; !-unique = λ { f → proj₂ (!-unique (𝒞.id , f)) } + } + where + open IsInitial initial + F-resp-+ + : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj} + {(i₁-c , i₁-d) : 𝒞×𝒟.U [ (C₁ , D₁) , (C₃ , D₃) ]} + {(i₂-c , i₂-d) : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]} + → IsCoproduct 𝒞×𝒟.U (i₁-c , i₁-d) (i₂-c , i₂-d) + → IsCoproduct 𝒟.U i₁-d i₂-d + F-resp-+ {_} {_} {_} {i₁-c , i₁-d} {i₂-c , i₂-d} isCoproduct = record + { [_,_] = λ { h₁ h₂ → proj₂ (copairing (i₁-c , h₁) (i₂-c , h₂)) } + ; inject₁ = proj₂ inject₁ + ; inject₂ = proj₂ inject₂ + ; unique = λ { eq₁ eq₂ → proj₂ (unique (𝒞.identityˡ , eq₁) (𝒞.identityˡ , eq₂)) } + } + where + open IsCoproduct isCoproduct renaming ([_,_] to copairing) + F-resp-coeq + : {(C₁ , D₁) (C₂ , D₂) (C₃ , D₃) : 𝒞×𝒟.Obj} + {f g : 𝒞×𝒟.U [ (C₁ , D₁) , (C₂ , D₂) ]} + {h : 𝒞×𝒟.U [ (C₂ , D₂) , (C₃ , D₃) ]} + → IsCoequalizer 𝒞×𝒟.U f g h + → IsCoequalizer 𝒟.U (proj₂ f) (proj₂ g) (proj₂ h) + F-resp-coeq isCoequalizer = record + { equality = proj₂ equality + ; coequalize = λ { eq → proj₂ (coequalize (proj₁ equality , eq)) } + ; universal = proj₂ universal + ; unique = λ { eq → proj₂ (unique (𝒞.Equiv.sym 𝒞.identityˡ , eq)) } + } + where + open IsCoequalizer isCoequalizer + +module _ where + + open FinitelyCocompleteCategory using (U) + + IsRightExact-※ + : {𝒞 𝒟 ℰ : FinitelyCocompleteCategory o ℓ e} + (F : Functor (U 𝒞) (U 𝒟)) + (G : Functor (U 𝒞) (U ℰ)) + → IsRightExact 𝒞 𝒟 F + → IsRightExact 𝒞 ℰ G + → IsRightExact 𝒞 (𝒟 × ℰ) (F ※ G) + IsRightExact-※ {𝒞} {𝒟} {ℰ} F G isRightExact-F isRightExact-G = record + { F-resp-⊥ = F-resp-⊥′ + ; F-resp-+ = F-resp-+′ + ; F-resp-coeq = F-resp-coeq′ + } + where + module 𝒞 = FinitelyCocompleteCategory 𝒞 + module 𝒟 = FinitelyCocompleteCategory 𝒟 + module ℰ = FinitelyCocompleteCategory ℰ + open IsRightExact isRightExact-F + open IsRightExact isRightExact-G renaming (F-resp-⊥ to G-resp-⊥; F-resp-+ to G-resp-+; F-resp-coeq to G-resp-coeq) + module F = Functor F + module G = Functor G + F-resp-⊥′ + : {A : 𝒞.Obj} + → IsInitial 𝒞.U A + → IsInitial (ProductCat 𝒟.U ℰ.U) (F.₀ A , G.₀ A) + F-resp-⊥′ A-isInitial = record + { ! = F[A]-isInitial.! , G[A]-isInitial.! + ; !-unique = dmap F[A]-isInitial.!-unique G[A]-isInitial.!-unique + } + where + module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial) + module G[A]-isInitial = IsInitial (G-resp-⊥ A-isInitial) + F-resp-+′ + : {A B C : 𝒞.Obj} {i₁ : 𝒞.U [ A , C ]} {i₂ : 𝒞.U [ B , C ]} + → IsCoproduct 𝒞.U i₁ i₂ + → IsCoproduct (ProductCat 𝒟.U ℰ.U) (F.₁ i₁ , G.₁ i₁) (F.₁ i₂ , G.₁ i₂) + F-resp-+′ {A} {B} {A+B} A+B-isCoproduct = record + { [_,_] = zip′ F[A+B]-isCoproduct.[_,_] G[A+B]-isCoproduct.[_,_] + ; inject₁ = F[A+B]-isCoproduct.inject₁ , G[A+B]-isCoproduct.inject₁ + ; inject₂ = F[A+B]-isCoproduct.inject₂ , G[A+B]-isCoproduct.inject₂ + ; unique = zip′ F[A+B]-isCoproduct.unique G[A+B]-isCoproduct.unique + } + where + module F[A+B]-isCoproduct = IsCoproduct (F-resp-+ A+B-isCoproduct) + module G[A+B]-isCoproduct = IsCoproduct (G-resp-+ A+B-isCoproduct) + F-resp-coeq′ + : {A B C : 𝒞.Obj} {f g : 𝒞.U [ A , B ]} {h : 𝒞.U [ B , C ]} + → IsCoequalizer 𝒞.U f g h + → IsCoequalizer (ProductCat 𝒟.U ℰ.U) (F.₁ f , G.₁ f) (F.₁ g , G.₁ g) (F.₁ h , G.₁ h) + F-resp-coeq′ h-isCoequalizer = record + { equality = F[h]-isCoequalizer.equality , G[h]-isCoequalizer.equality + ; coequalize = map F[h]-isCoequalizer.coequalize G[h]-isCoequalizer.coequalize + ; universal = F[h]-isCoequalizer.universal , G[h]-isCoequalizer.universal + ; unique = map F[h]-isCoequalizer.unique G[h]-isCoequalizer.unique + } + where + module F[h]-isCoequalizer = IsCoequalizer (F-resp-coeq h-isCoequalizer) + module G[h]-isCoequalizer = IsCoequalizer (G-resp-coeq h-isCoequalizer) + + IsRightExact-⁂ + : {𝒜 ℬ 𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e} + (F : Functor (U 𝒜) (U 𝒞)) + (G : Functor (U ℬ) (U 𝒟)) + → IsRightExact 𝒜 𝒞 F + → IsRightExact ℬ 𝒟 G + → IsRightExact (𝒜 × ℬ) (𝒞 × 𝒟) (F ⁂ G) + IsRightExact-⁂ {𝒜} {ℬ} {𝒞} {𝒟} F G isRightExact-F isRightExact-G = record + { F-resp-⊥ = F-resp-⊥′ + ; F-resp-+ = F-resp-+′ + ; F-resp-coeq = F-resp-coeq′ + } + where + module 𝒜 = FinitelyCocompleteCategory 𝒜 + module ℬ = FinitelyCocompleteCategory ℬ + module 𝒞 = FinitelyCocompleteCategory 𝒞 + module 𝒟 = FinitelyCocompleteCategory 𝒟 + module 𝒜×ℬ = FinitelyCocompleteCategory (𝒜 × ℬ) + module 𝒞×𝒟 = FinitelyCocompleteCategory (𝒞 × 𝒟) + open IsRightExact isRightExact-F + open IsRightExact isRightExact-G renaming (F-resp-⊥ to G-resp-⊥; F-resp-+ to G-resp-+; F-resp-coeq to G-resp-coeq) + module F = Functor F + module G = Functor G + F-resp-⊥′ + : {(A , B) : 𝒜×ℬ.Obj} + → IsInitial 𝒜×ℬ.U (A , B) + → IsInitial 𝒞×𝒟.U (F.₀ A , G.₀ B) + F-resp-⊥′ {A , B} A,B-isInitial = record + { ! = F[A]-isInitial.! , G[B]-isInitial.! + ; !-unique = dmap F[A]-isInitial.!-unique G[B]-isInitial.!-unique + } + where + module A,B-isInitial = IsInitial A,B-isInitial + A-isInitial : IsInitial 𝒜.U A + A-isInitial = record + { ! = λ { {X} → proj₁ (A,B-isInitial.! {X , B}) } + ; !-unique = λ { f → proj₁ (A,B-isInitial.!-unique (f , ℬ.id)) } + } + B-isInitial : IsInitial ℬ.U B + B-isInitial = record + { ! = λ { {X} → proj₂ (A,B-isInitial.! {A , X}) } + ; !-unique = λ { f → proj₂ (A,B-isInitial.!-unique (𝒜.id , f)) } + } + module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial) + module G[B]-isInitial = IsInitial (G-resp-⊥ B-isInitial) + F-resp-+′ + : {A B C : 𝒜×ℬ.Obj} {(i₁ , i₁′) : 𝒜×ℬ.U [ A , C ]} {(i₂ , i₂′) : 𝒜×ℬ.U [ B , C ]} + → IsCoproduct 𝒜×ℬ.U (i₁ , i₁′) (i₂ , i₂′) + → IsCoproduct 𝒞×𝒟.U (F.₁ i₁ , G.₁ i₁′) (F.₁ i₂ , G.₁ i₂′) + F-resp-+′ {A} {B} {A+B} {i₁ , i₁′} {i₂ , i₂′} A+B,A+B′-isCoproduct = record + { [_,_] = zip′ F[A+B]-isCoproduct.[_,_] G[A+B′]-isCoproduct.[_,_] + ; inject₁ = F[A+B]-isCoproduct.inject₁ , G[A+B′]-isCoproduct.inject₁ + ; inject₂ = F[A+B]-isCoproduct.inject₂ , G[A+B′]-isCoproduct.inject₂ + ; unique = zip′ F[A+B]-isCoproduct.unique G[A+B′]-isCoproduct.unique + } + where + module A+B,A+B′-isCoproduct = IsCoproduct A+B,A+B′-isCoproduct + A+B-isCoproduct : IsCoproduct 𝒜.U i₁ i₂ + A+B-isCoproduct = record + { [_,_] = λ { f g → proj₁ (A+B,A+B′-isCoproduct.[ (f , i₁′) , (g , i₂′) ]) } + ; inject₁ = proj₁ A+B,A+B′-isCoproduct.inject₁ + ; inject₂ = proj₁ A+B,A+B′-isCoproduct.inject₂ + ; unique = λ { ≈f ≈g → proj₁ (A+B,A+B′-isCoproduct.unique (≈f , ℬ.identityˡ) (≈g , ℬ.identityˡ)) } + } + A+B′-isCoproduct : IsCoproduct ℬ.U i₁′ i₂′ + A+B′-isCoproduct = record + { [_,_] = λ { f g → proj₂ (A+B,A+B′-isCoproduct.[ (i₁ , f) , (i₂ , g) ]) } + ; inject₁ = proj₂ A+B,A+B′-isCoproduct.inject₁ + ; inject₂ = proj₂ A+B,A+B′-isCoproduct.inject₂ + ; unique = λ { ≈f ≈g → proj₂ (A+B,A+B′-isCoproduct.unique (𝒜.identityˡ , ≈f) (𝒜.identityˡ , ≈g)) } + } + module F[A+B]-isCoproduct = IsCoproduct (F-resp-+ A+B-isCoproduct) + module G[A+B′]-isCoproduct = IsCoproduct (G-resp-+ A+B′-isCoproduct) + F-resp-coeq′ + : {A B C : 𝒜×ℬ.Obj} {(f , f′) (g , g′) : 𝒜×ℬ.U [ A , B ]} {(h , h′) : 𝒜×ℬ.U [ B , C ]} + → IsCoequalizer 𝒜×ℬ.U (f , f′) (g , g′) (h , h′) + → IsCoequalizer 𝒞×𝒟.U (F.₁ f , G.₁ f′) (F.₁ g , G.₁ g′) (F.₁ h , G.₁ h′) + F-resp-coeq′ {_} {_} {_} {f , f′} {g , g′} {h , h′} h,h′-isCoequalizer = record + { equality = F[h]-isCoequalizer.equality , G[h′]-isCoequalizer.equality + ; coequalize = map F[h]-isCoequalizer.coequalize G[h′]-isCoequalizer.coequalize + ; universal = F[h]-isCoequalizer.universal , G[h′]-isCoequalizer.universal + ; unique = map F[h]-isCoequalizer.unique G[h′]-isCoequalizer.unique + } + where + module h,h′-isCoequalizer = IsCoequalizer h,h′-isCoequalizer + h-isCoequalizer : IsCoequalizer 𝒜.U f g h + h-isCoequalizer = record + { equality = proj₁ h,h′-isCoequalizer.equality + ; coequalize = λ { eq → proj₁ (h,h′-isCoequalizer.coequalize (eq , proj₂ h,h′-isCoequalizer.equality)) } + ; universal = proj₁ h,h′-isCoequalizer.universal + ; unique = λ { ≈h → proj₁ (h,h′-isCoequalizer.unique (≈h , ℬ.Equiv.sym ℬ.identityˡ)) } + } + h′-isCoequalizer : IsCoequalizer ℬ.U f′ g′ h′ + h′-isCoequalizer = record + { equality = proj₂ h,h′-isCoequalizer.equality + ; coequalize = λ { eq′ → proj₂ (h,h′-isCoequalizer.coequalize (proj₁ h,h′-isCoequalizer.equality , eq′)) } + ; universal = proj₂ h,h′-isCoequalizer.universal + ; unique = λ { ≈h′ → proj₂ (h,h′-isCoequalizer.unique (𝒜.Equiv.sym 𝒜.identityˡ , ≈h′)) } + } + + module F[h]-isCoequalizer = IsCoequalizer (F-resp-coeq h-isCoequalizer) + module G[h′]-isCoequalizer = IsCoequalizer (G-resp-coeq h′-isCoequalizer) +_×₁_ + : {𝒜 ℬ 𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e} + → RightExactFunctor 𝒜 𝒞 + → RightExactFunctor ℬ 𝒟 + → RightExactFunctor (𝒜 × ℬ) (𝒞 × 𝒟) +F ×₁ G = record + { F = F.F ⁂ G.F + ; isRightExact = IsRightExact-⁂ F.F G.F F.isRightExact G.isRightExact + } + where + module F = RightExactFunctor F + module G = RightExactFunctor G + +FinitelyCocompletes-Products : {𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e} → Product FinitelyCocompletes 𝒞 𝒟 +FinitelyCocompletes-Products {𝒞} {𝒟} = record + { A×B = 𝒞 × 𝒟 + ; π₁ = rightexact πˡ (πˡ-RightExact 𝒞 𝒟) + ; π₂ = rightexact πʳ (πʳ-RightExact 𝒞 𝒟) + ; ⟨_,_⟩ = λ { (rightexact F isF) (rightexact G isG) → rightexact (F ※ G) (IsRightExact-※ F G isF isG) } + ; project₁ = λ { {_} {rightexact F _} {rightexact G _} → Cats.project₁ {h = F} {i = G} } + ; project₂ = λ { {_} {rightexact F _} {rightexact G _} → Cats.project₂ {h = F} {i = G} } + ; unique = Cats.unique + } + where + module 𝒞 = FinitelyCocompleteCategory 𝒞 + module 𝒟 = FinitelyCocompleteCategory 𝒟 + module Cats = BinaryProducts Products.Cats-has-all + +FinitelyCocompletes-BinaryProducts : BinaryProducts FinitelyCocompletes +FinitelyCocompletes-BinaryProducts = record + { product = FinitelyCocompletes-Products + } + +FinitelyCocompletes-Cartesian : Cartesian FinitelyCocompletes +FinitelyCocompletes-Cartesian = record + { terminal = record + { ⊤ = One-FCC + ; ⊤-is-terminal = _ + } + ; products = FinitelyCocompletes-BinaryProducts + } diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda new file mode 100644 index 0000000..1452669 --- /dev/null +++ b/Category/Instance/One/Properties.agda @@ -0,0 +1,35 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Category.Instance.One.Properties {o ℓ e : Level} where + +open import Categories.Category.Core using (Category) +open import Categories.Category.Instance.One using () renaming (One to One′) + +One : Category o ℓ e +One = One′ + +open import Categories.Category.Cocartesian One using (Cocartesian) +open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete) +open import Categories.Object.Initial One using (Initial) +open import Categories.Category.Cocartesian One using (BinaryCoproducts) + + +One-Initial : Initial +One-Initial = _ + +One-BinaryCoproducts : BinaryCoproducts +One-BinaryCoproducts = _ + +One-Cocartesian : Cocartesian +One-Cocartesian = record + { initial = One-Initial + ; coproducts = One-BinaryCoproducts + } + +One-FinitelyCocomplete : FinitelyCocomplete +One-FinitelyCocomplete = record + { cocartesian = One-Cocartesian + ; coequalizer = _ + } diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda new file mode 100644 index 0000000..9f848f4 --- /dev/null +++ b/Category/Instance/Properties/FinitelyCocompletes.agda @@ -0,0 +1,208 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where + +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_) +open import Categories.Diagram.Coequalizer using (IsCoequalizer) +open import Categories.Functor.Core using (Functor) +open import Categories.Functor using (_∘F_) renaming (id to idF) +open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct) +open import Categories.Object.Initial using (IsInitial) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_) +open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) +open import Functor.Exact using (IsRightExact; RightExactFunctor) +open import Level using (_⊔_; suc) + +FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) +FinitelyCocompletes-CC = record + { U = FinitelyCocompletes + ; cartesian = FinitelyCocompletes-Cartesian + } + +module FinCoCom = CartesianCategory FinitelyCocompletes-CC +open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) -- hiding (unique) + +module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where + + private + module 𝒞 = FinitelyCocompleteCategory 𝒞 + module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 × 𝒞) + + open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-) + open Equiv + module -+- = Functor -+- + + +-resp-⊥ + : {(A , B) : 𝒞×𝒞.Obj} + → IsInitial 𝒞×𝒞.U (A , B) + → IsInitial 𝒞.U (A + B) + +-resp-⊥ {A , B} A,B-isInitial = record + { ! = [ A-isInitial.! , B-isInitial.! ] + ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) } + } + where + open IsRightExact + open RightExactFunctor + module A-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₁ {𝒞} {𝒞})) A,B-isInitial) + module B-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₂ {𝒞} {𝒞})) A,B-isInitial) + + +-resp-+ + : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} + {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)} + {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} + → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂) + → IsCoproduct 𝒞.U (i₁-₁ +₁ i₁-₂) (i₂-₁ +₁ i₂-₂) + +-resp-+ {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {i₁-₁ , i₁-₂} {i₂-₁ , i₂-₂} isCoproduct = record + { [_,_] = λ { h₁ h₂ → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] } + ; inject₁ = inject₁ + ; inject₂ = inject₂ + ; unique = unique + } + where + open IsRightExact + open RightExactFunctor + module Coprod₁ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₁ {𝒞} {𝒞})) isCoproduct)) + module Coprod₂ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₂ {𝒞} {𝒞})) isCoproduct)) + open 𝒞 using ([]-cong₂; []∘+₁; +-g-η; +₁∘i₁; +₁∘i₂) + open 𝒞 using (Obj; _≈_; module HomReasoning; assoc) + open HomReasoning + open ⇒-Reasoning 𝒞.U + inject₁ + : {X : Obj} + {h₁ : A₁ + A₂ ⇒ X} + {h₂ : B₁ + B₂ ⇒ X} + → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁ + inject₁ {_} {h₁} {h₂} = begin + [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈⟨ []∘+₁ ⟩ + [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₁-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₁-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₁ Coprod₂.inject₁ ⟩ + [ h₁ ∘ i₁ , h₁ ∘ i₂ ] ≈⟨ +-g-η ⟩ + h₁ ∎ + inject₂ + : {X : Obj} + {h₁ : A₁ + A₂ ⇒ X} + {h₂ : B₁ + B₂ ⇒ X} + → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂ + inject₂ {_} {h₁} {h₂} = begin + [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈⟨ []∘+₁ ⟩ + [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₂-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₂-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₂ Coprod₂.inject₂ ⟩ + [ h₂ ∘ i₁ , h₂ ∘ i₂ ] ≈⟨ +-g-η ⟩ + h₂ ∎ + unique + : {X : Obj} + {i : C₁ + C₂ ⇒ X} + {h₁ : A₁ + A₂ ⇒ X} + {h₂ : B₁ + B₂ ⇒ X} + (eq₁ : i ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁) + (eq₂ : i ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂) + → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈ i + unique {X} {i} {h₁} {h₂} eq₁ eq₂ = begin + [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (Coprod₁.unique eq₁-₁ eq₂-₁) (Coprod₂.unique eq₁-₂ eq₂-₂) ⟩ + [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ +-g-η ⟩ + i ∎ + where + eq₁-₁ : (i ∘ i₁) ∘ i₁-₁ ≈ h₁ ∘ i₁ + eq₁-₁ = begin + (i ∘ i₁) ∘ i₁-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ + i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₁ ≈⟨ pullˡ eq₁ ⟩ + h₁ ∘ i₁ ∎ + eq₂-₁ : (i ∘ i₁) ∘ i₂-₁ ≈ h₂ ∘ i₁ + eq₂-₁ = begin + (i ∘ i₁) ∘ i₂-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ + i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₁ ≈⟨ pullˡ eq₂ ⟩ + h₂ ∘ i₁ ∎ + eq₁-₂ : (i ∘ i₂) ∘ i₁-₂ ≈ h₁ ∘ i₂ + eq₁-₂ = begin + (i ∘ i₂) ∘ i₁-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ + i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₂ ≈⟨ pullˡ eq₁ ⟩ + h₁ ∘ i₂ ∎ + eq₂-₂ : (i ∘ i₂) ∘ i₂-₂ ≈ h₂ ∘ i₂ + eq₂-₂ = begin + (i ∘ i₂) ∘ i₂-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ + i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₂ ≈⟨ pullˡ eq₂ ⟩ + h₂ ∘ i₂ ∎ + + +-resp-coeq + : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} + {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)} + {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} + → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) + → IsCoequalizer 𝒞.U (f₁ +₁ f₂) (g₁ +₁ g₂) (h₁ +₁ h₂) + +-resp-coeq {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {f₁ , f₂} {g₁ , g₂} {h₁ , h₂} isCoeq = record + { equality = sym -+-.homomorphism ○ []-cong₂ (refl⟩∘⟨ Coeq₁.equality) (refl⟩∘⟨ Coeq₂.equality) ○ -+-.homomorphism + ; coequalize = coequalize + ; universal = universal _ + ; unique = uniq _ + } + where + open IsRightExact + open RightExactFunctor + module Coeq₁ = IsCoequalizer (F-resp-coeq (isRightExact (π₁ {𝒞} {𝒞})) isCoeq) + module Coeq₂ = IsCoequalizer (F-resp-coeq (isRightExact (π₂ {𝒞} {𝒞})) isCoeq) + open 𝒞 using ([]-cong₂; +₁∘i₁; +₁∘i₂; []∘+₁; +-g-η) + open 𝒞 using (Obj; _≈_; module HomReasoning; assoc; sym-assoc) + open 𝒞.HomReasoning + open ⇒-Reasoning 𝒞.U + + module _ {X : Obj} {k : B₁ + B₂ ⇒ X} (eq : k ∘ (f₁ +₁ f₂) ≈ k ∘ (g₁ +₁ g₂)) where + + eq₁ : (k ∘ i₁) ∘ f₁ ≈ (k ∘ i₁) ∘ g₁ + eq₁ = begin + (k ∘ i₁) ∘ f₁ ≈⟨ pushʳ +₁∘i₁ ⟨ + k ∘ (f₁ +₁ f₂) ∘ i₁ ≈⟨ extendʳ eq ⟩ + k ∘ (g₁ +₁ g₂) ∘ i₁ ≈⟨ pushʳ +₁∘i₁ ⟩ + (k ∘ i₁) ∘ g₁ ∎ + + eq₂ : (k ∘ i₂) ∘ f₂ ≈ (k ∘ i₂) ∘ g₂ + eq₂ = begin + (k ∘ i₂) ∘ f₂ ≈⟨ pushʳ +₁∘i₂ ⟨ + k ∘ (f₁ +₁ f₂) ∘ i₂ ≈⟨ extendʳ eq ⟩ + k ∘ (g₁ +₁ g₂) ∘ i₂ ≈⟨ pushʳ +₁∘i₂ ⟩ + (k ∘ i₂) ∘ g₂ ∎ + + coequalize : C₁ + C₂ ⇒ X + coequalize = [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] + + universal : k ≈ coequalize ∘ (h₁ +₁ h₂) + universal = begin + k ≈⟨ +-g-η ⟨ + [ k ∘ i₁ , k ∘ i₂ ] ≈⟨ []-cong₂ Coeq₁.universal Coeq₂.universal ⟩ + [ Coeq₁.coequalize eq₁ ∘ h₁ , Coeq₂.coequalize eq₂ ∘ h₂ ] ≈⟨ []∘+₁ ⟨ + coequalize ∘ (h₁ +₁ h₂) ∎ + + uniq : {i : C₁ + C₂ ⇒ X} → k ≈ i ∘ (h₁ +₁ h₂) → i ≈ coequalize + uniq {i} eq′ = begin + i ≈⟨ +-g-η ⟨ + [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ []-cong₂ (Coeq₁.unique eq₁′) (Coeq₂.unique eq₂′) ⟩ + [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] ∎ + where + eq₁′ : k ∘ i₁ ≈ (i ∘ i₁) ∘ h₁ + eq₁′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₁ + eq₂′ : k ∘ i₂ ≈ (i ∘ i₂) ∘ h₂ + eq₂′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₂ + +module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where + + open FinCoCom using (_⇒_; _∘_; id) + module 𝒞 = FinitelyCocompleteCategory 𝒞 + + -+- : 𝒞 × 𝒞 ⇒ 𝒞 + -+- = record + { F = 𝒞.-+- + ; isRightExact = record + { F-resp-⊥ = +-resp-⊥ 𝒞 + ; F-resp-+ = +-resp-+ 𝒞 + ; F-resp-coeq = +-resp-coeq 𝒞 + } + } + + [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 + [x+y]+z = -+- ∘ (-+- ×₁ id) + + x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 + x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ |