open import Cat.Instances.Shape.Initial
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Constant
open import Cat.Diagram.Initial
open import Cat.Prelude

module Cat.Diagram.Colimit.Initial {o h} (C : Precategory o h) where

open Precategory C

open Initial
open Functor
open _=>_

Initial objects are colimitsšŸ”—

An initial object is equivalently defined as a colimit of the empty diagram.

is-colimitā†’is-initial
  : āˆ€ {T : Ob} {eta : Ā”F => Const T}
  ā†’ is-colimit {C = C} Ā”F T eta
  ā†’ is-initial C T
is-colimitā†’is-initial colim Y = record where
  module colim = is-colimit colim

  centre  = colim.universal (Ī» ()) Ī» ()
  paths _ = colim.unique _ _ _ Ī» ()

is-initialā†’is-colimit : āˆ€ {T : Ob} {F : Functor āŠ„Cat C} ā†’ is-initial C T ā†’ is-colimit {C = C} F T Ā”nt
is-initialā†’is-colimit {T} {F} init = to-is-colimitp mc Ī» {} where
  open make-is-colimit
  mc : make-is-colimit F T
  mc .Ļˆ ()
  mc .commutes ()
  mc .universal _ _ = init _ .centre
  mc .factors {}
  mc .unique _ _ _ _ = init _ .paths _

Colimitā†’Initial : Colimit {C = C} Ā”F ā†’ Initial C
Colimitā†’Initial colim .bot = Colimit.coapex colim
Colimitā†’Initial colim .hasāŠ„ = is-colimitā†’is-initial (Colimit.has-colimit colim)

Initialā†’Colimit : āˆ€ {F : Functor āŠ„Cat C} ā†’ Initial C ā†’ Colimit {C = C} F
Initialā†’Colimit init = to-colimit (is-initialā†’is-colimit (init .hasāŠ„))