open import Cat.Diagram.Coproduct.Indexed open import Cat.Diagram.Colimit.Base open import Cat.Instances.Discrete open import Cat.Instances.Product open import Cat.Prelude import Cat.Reasoning 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 .
_⊗_ : 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)) (Disc-adjunct F) (colim _)