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 _