open import Cat.Diagram.Colimit.Coproduct
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Naturality
open import Cat.Instances.Discrete
open import Cat.Instances.Product
open import Cat.Instances.Sets
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Reasoning

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

module Copowers
  {o ℓ} {C : Precategory o ℓ}
  (coprods : (S : Set ℓ) → has-coproducts-indexed-by C ∣ S ∣)
  where

  open Functor
  open Indexed-coproduct
  open Cat.Reasoning C

  _⊗_ : 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)

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

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

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

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

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  (S .is-tr)) F (colim _)