…am.Colimit.Representable

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 $\mathbf{Hom}$ -functors.

Let $\mathrm{Dia} : \mathcal{J} \to \mathcal{C}$ be some diagram in $\mathcal{C}$ . If $\mathrm{Dia}$ has a colimit $c$ , then that means that maps out of $c$ are in bijection with a product of maps $\pi_i$ , 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 = funext λ _ → Nat-path λ _ → C.idl _
  Lim[C[F-,=]] .F-∘ _ _ = funext λ _ → Nat-path λ _ → 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 = funext λ g → Nat-path λ _ →
    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} {α} = Nat-path λ j →
      nat-inv.invl ηₚ _ $ₚ _ ηₚ j ∙ C.idl _
    colim .σ-uniq {M} {α} {σ'} q = Nat-path λ j →
      nat-inv.inv .η _ (idnat-constr ∘nt ⌜ α ⌝)                               ≡⟨ ap! q ⟩
      nat-inv.inv .η _ ⌜ idnat-constr ∘nt (σ' ◂ !F) ∘nt cocone→unit Dia eta ⌝ ≡⟨ ap! (Nat-path λ _ → C.idl _) ⟩
      nat-inv.inv .η (M .F₀ tt) (const-nt (σ' .η j) ∘nt eta)                  ≡⟨ nat-inv.invr ηₚ _ $ₚ _ ⟩
      σ' .η tt ∎