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 Copowers {o β} {C : Precategory o β} (coprods : (S : Set β) β has-coproducts-indexed-by C β£ S β£) where open Functor open Indexed-coproduct open Cat.Reasoning C
_β_ : Set β β Ob β Ob X β A = coprods X (Ξ» _ β A) .Ξ£F
Copowers satisfy a universal property: is a representing object for the functor that takes an object to the th power of the set of morphisms from to ; in other words, we have a natural isomorphism .
copower-hom-iso : β {X A} β Hom-from C (X β A) β βΏ Hom-from (Sets β) X Fβ Hom-from C A copower-hom-iso {X} {A} = isoβisoβΏ (Ξ» _ β equivβiso (hom-iso (coprods X (Ξ» _ β A)))) (Ξ» _ β ext Ξ» _ _ β assoc _ _ _)
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 = Copowers.Copowering Ξ» S F β ColimitβIC _ (is-hlevel-suc 2 (S .is-tr)) F (colim _)