module Cat.Diagram.Coproduct.Copower where

Copowers🔗

Let $C$ 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

n a \times a \times \dots \times a

is called a “power”, we refer to the coproduct $∐_{X} A$ of many copies of an object $X$ indexed by a $κ -small$ set $X$ as the copower of $A$ by $X,$ and alternatively denote it $X \otimes A .$ If $C$ does indeed admit coproducts indexed by any $κ -small$ set, then the copowering construction extends to a functor $Sets_{κ} \times C \to C .$

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 $Sets_{κ} .$

  _⊗_ : 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 th$ power of the set of morphisms from $A$ to $B;$ in other words, we have a natural isomorphism $Hom_{C} (X \otimes A, -) ≅ Hom_{Sets} (X, Hom_{C} (A, -)) .$

  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 .$ 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)

  ∐! : (Idx : Type ℓ) ⦃ hl : H-Level Idx 2 ⦄ (F : Idx → Ob) → Ob
  ∐! Idx F = ΣF (coprods (el! Idx) F)

  module ∐! (Idx : Type ℓ) ⦃ hl : H-Level Idx 2 ⦄ (F : Idx → Ob) =
    Indexed-coproduct (coprods (el! Idx) F)

  _⊗!_ : (Idx : Type ℓ) ⦃ hl : H-Level Idx 2 ⦄ → Ob → Ob
  I ⊗! X = el! I ⊗ X

  module ⊗! (Idx : Type ℓ) ⦃ hl : H-Level Idx 2 ⦄ (X : Ob) =
    Indexed-coproduct (coprods (el! Idx) (λ _ → X))