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

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

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

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