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 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

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: 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

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

  β! : (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))

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