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Γ—β‹―Γ—a⏟n \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 XβŠ—AX \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ΞΊΓ—Cβ†’C\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.

module
  _ {o β„“} {C : Precategory o β„“}
  (coprods : (S : Set β„“) (F : ∣ S ∣ β†’ Precategory.Ob C) β†’ Indexed-coproduct C F)
  where

  open Functor
  open is-indexed-coproduct
  open Indexed-coproduct
  open Cat.Reasoning C

  _βŠ—_ : 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:X→Yf : X \to Y and changing the underlying object by a morphism g:A→Bg : 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)) F (colim _)