module Cat.Diagram.Coproduct.Copower where


Let be a category admitting 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

is called a β€œpower”, we refer to the coproduct of many copies of an object indexed by a set as the copower of by and alternatively denote it If does indeed admit coproducts indexed by any set, then the copowering construction extends to a functor

The notion of copowering gives us slick terminology for a category which admits all coproducts, but not necessarily all colimits: Such a category is precisely one copowered over

  _βŠ—_ : Set β„“ β†’ Ob β†’ Ob
  X βŠ— A = coprods X (Ξ» _ β†’ A) .Ξ£F

Copowers satisfy a universal property: is a representing object for the functor that takes an object to the power of the set of morphisms from to in other words, we have a natural isomorphism

    : βˆ€ {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 and changing the underlying object by a morphism 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)

  : βˆ€ {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 _)