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

  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 ∎