module Cat.Diagram.Coproduct.Copower where
Copowersπ
Let be a category admitting -small indexed coproducts, for example a -cocomplete category. In the same way that (in ordinary arithmetic) the iterated product of a bunch of copies of the same factor
is called a βpowerβ, we refer to the coproduct of many copies of an object indexed by a -small set as the copower of by , and alternatively denote it . If does indeed admit coproducts indexed by any -small set, then the copowering construction extends to a functor .
The notion of copowering gives us slick terminology for a category which admits all -small coproducts, but not necessarily all -small colimits: Such a category is precisely one copowered over .
module _ {o β} {C : Precategory o β} (coprods : (S : Set β) (F : β£ S β£ β Precategory.Ob C) β Indexed-coproduct C F) where open Functor open is-indexed-coproduct open Indexed-coproduct open Cat.Reasoning C
_β_ : Set β β Ob β Ob X β A = coprods X (Ξ» _ β A) .Ξ£F
The action of the copowering functor is given by simultaneously changing the indexing along a function of sets and changing the underlying object by a morphism . This is functorial by the uniqueness properties of colimiting maps.
Copowering : Functor (Sets β ΓαΆ C) C Copowering .Fβ (X , A) = X β A Copowering .Fβ {X , A} {Y , B} (idx , obj) = coprods X (Ξ» _ β A) .match Ξ» i β coprods Y (Ξ» _ β B) .ΞΉ (idx i) β obj Copowering .F-id {X , A} = sym $ coprods X (Ξ» _ β A) .unique _ Ξ» i β sym id-comm Copowering .F-β {X , A} f g = sym $ coprods X (Ξ» _ β A) .unique _ Ξ» i β pullr (coprods _ _ .commute) β extendl (coprods _ _ .commute) cocompleteβcopowering : β {o β} {C : Precategory o β} β is-cocomplete β β C β Functor (Sets β ΓαΆ C) C cocompleteβcopowering colim = Copowering Ξ» S F β ColimitβIC _ (is-hlevel-suc 2 (S .is-tr)) F (colim _)