open import Cat.Diagram.Subterminal
open import Cat.Diagram.Initial
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Initial.Strict where

module _ {o h} (C : Precategory o h) where
  open Cat.Reasoning C
  open Initial

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 $X\to \perp$ then $X$ 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 

As maps out of initial objects are unique, it suffices to show that every map $\text{!‘}\circ f=\mathrm{id}$ for every $f:X\to \perp$ to establish that $\perp$ 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 $f,g:X\to \perp \text{,}$ it suffices to prove that $f\circ g^{-1}={\mathrm{id}}_{\perp }\text{;}$ but those are maps out of $\perp \text{,}$ 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 _