open import Cat.Functor.Hom.Representable
open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Functor.Compose
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Colimit.Representable where


## Representability of colimitsπ

Since colimits are defined by universal property, we can also phrase the definition in terms of an equivalence between

module _
{o β}
{J : Precategory β β} {C : Precategory o β} {Dia : Functor J C}
where
private
module C = Cat.Reasoning C
open Functor
open _=>_
open Corepresentation
open Colimit
open is-lan


Let be some diagram in If has a colimit then that means that maps out of are in bijection with a product of maps subject to some conditions.

  Lim[C[F-,=]] : Functor C (Sets β)
Lim[C[F-,=]] .Fβ c = el (Dia => Const c) Nat-is-set
Lim[C[F-,=]] .Fβ f Ξ± = const-nt f βnt Ξ±
Lim[C[F-,=]] .F-id = ext Ξ» _ _ β C.idl _
Lim[C[F-,=]] .F-β _ _ = ext Ξ» _ _ β sym $C.assoc _ _ _ Hom-into-inj : β {c : C.Ob} (eta : Dia => Const c) β Hom-from C c => Lim[C[F-,=]] Hom-into-inj eta .Ξ· x f = const-nt f βnt eta Hom-into-inj eta .is-natural x y f = ext Ξ» g _ β sym$ C.assoc _ _ _

representsβis-colimit
: β {c : C.Ob} {eta : Dia => Const c}
β is-invertibleβΏ (Hom-into-inj eta)
β is-colimit Dia c eta
representsβis-colimit {c} {eta} nat-inv = colim where
module nat-inv = is-invertibleβΏ nat-inv

colim : is-colimit Dia c eta
colim .Ο {M} Ξ± =
homββ€-natural-trans \$ nat-inv.inv .Ξ· _ (idnat-constr βnt Ξ±)
colim .Ο-comm {M} {Ξ±} = ext Ξ» j β
unext nat-inv.invl _ _ j β C.idl _
colim .Ο-uniq {M} {Ξ±} {Ο'} q = ext Ξ» j β
nat-inv.inv .Ξ· _ (idnat-constr βnt β Ξ± β)                               β‘β¨ ap! q β©β‘
nat-inv.inv .Ξ· _ β idnat-constr βnt (Ο' β !F) βnt coconeβunit Dia eta β β‘β¨ ap! (ext Ξ» _ β C.idl _) β©β‘
nat-inv.inv .Ξ· (M .Fβ tt) (const-nt (Ο' .Ξ· j) βnt eta)                  β‘β¨ unext nat-inv.invr _ _ β©β‘
Ο' .Ξ· tt β