Structures · Category theory

CategoryTheory.Limits.HasStrictInitialObjects

We say C has strict initial objects if every initial object is strict, i.e. given any morphism f : A ⟶ I where I is initial, then f is an isomorphism. Strictly speaking, this says that any initial object must be strict, rather than that strict initial objects exist.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Shape

One type argument · adds out