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 C\mathcal{C} be a category admitting κ\kappa-small indexed coproducts, for example a κ\kappa-cocomplete category. In the same way that (in ordinary arithmetic) the iterated product of a bunch of copies of the same factor

a×a××an \underbrace{a \times a \times \dots \times a}_{n}

is called a “power”, we refer to the coproduct XA\coprod_{X} A of many copies of an object XX indexed by a κ\kappa-small set XX as the copower of AA by XX, and alternatively denote it XAX \otimes A. If C\mathcal{C} does indeed admit coproducts indexed by any κ\kappa-small set, then the copowering construction extends to a functor Setsκ×CC{{\mathbf{Sets}}}_\kappa \times \mathcal{C} \to \mathcal{C}.

The notion of copowering gives us slick terminology for a category which admits all κ\kappa-small coproducts, but not necessarily all κ\kappa-small colimits: Such a category is precisely one copowered over Setsκ{{\mathbf{Sets}}}_\kappa.

  _⊗_ : 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 f:XYf : X \to Y and changing the underlying object by a morphism g:ABg : A \to B. 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 _)