module Cat.Diagram.Coproduct.Copower where

Copowers🔗

Let $\mathcal{C}$ be a category admitting $\kappa \text{-small}$ indexed coproducts, for example a $\kappa \text{-}$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 ${\coprod }_{X}A$ of many copies of an object $X$ indexed by a $\kappa \text{-small}$ set $X$ as the copower of $A$ by $X\text{,}$ and alternatively denote it $X\otimes A\text{.}$ If $\mathcal{C}$ does indeed admit coproducts indexed by any $\kappa \text{-small}$ set, then the copowering construction extends to a functor ${\mathbf{Sets}}_{\kappa }\times \mathcal{C}\to \mathcal{C}\text{.}$

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

  _⊗_ : Set ℓ → Ob → Ob
  X ⊗ A = coprods X (λ _ → A) .ΣF

Copowers satisfy a universal property: $X\otimes A$ is a representing object for the functor that takes an object $B$ to the $X\text{th}$ power of the set of morphisms from $A$ to $B\text{;}$ in other words, we have a natural isomorphism ${\mathbf{Hom}}_{\mathcal{C}}(X\otimes A,-)\cong {\mathbf{Hom}}_{\mathbf{Sets}}(X,{\mathbf{Hom}}_{\mathcal{C}}(A,-))\text{.}$

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