module Cat.Diagram.Initial.Strict where

Strict initial objects🔗

An initial object is said to be strict if every morphism into it is an isomorphism. This is a categorical generalization of the fact that if one can write a function then must itself be empty.

This is an instance of the more general notion of van Kampen colimits.

  is-strict-initial : Initial C  Type _
  is-strict-initial i =  x  (f : Hom x (i .bot))  is-invertible f

  record Strict-initial : Type (o  h) where
    field
      initial : Initial C
      has-is-strict : is-strict-initial initial

Strictness is a property of, not structure on, an initial object.

  is-strict-initial-is-prop :  i  is-prop (is-strict-initial i)
  is-strict-initial-is-prop i = hlevel 1

As maps out of initial objects are unique, it suffices to show that every map for every to establish that is a strict initial object.

  make-is-strict-initial
    : (i : Initial C)
     (∀ x  (f : Hom x (i .bot))  (¡ i)  f  id)
     is-strict-initial i
  make-is-strict-initial i p x f =
    make-invertible (¡ i) (¡-unique₂ i (f  ¡ i) id) (p x f)

Strict initial objects are subterminal objects: given two maps it suffices to prove that but those are maps out of so they are equal.

  strict-initial→subterminal
    :  {i : Initial C}
     is-strict-initial i
     is-subterminal C (i .bot)
  strict-initial→subterminal {i} s X f g =
    pre-invr.to (s _ g) (¡-unique₂ i _ id)  idl _