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 ⊥$ 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 1

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