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ⁿ 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ⁿ 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} α =
      !constⁿ (nat-inv.inv .η _ (to-coconeⁿ α))
    colim .σ-comm {M} {α} = ext λ j → unext nat-inv.invl _ _ j
    colim .σ-uniq {M} {α} {σ'} q = ext λ j →
      nat-inv.inv .η _ (to-coconeⁿ ⌜ α ⌝)                  ≡⟨ ap! q ⟩
      nat-inv.inv .η _ ⌜ to-coconeⁿ ((σ' ◂ !F) ∘nt eta) ⌝  ≡⟨ ap! trivial! ⟩
      nat-inv.inv .η _ ((!constⁿ (σ' .η tt) ◂ !F) ∘nt eta) ≡⟨ unext nat-inv.invr _ _ ⟩
      σ' .η tt                                             ∎