Theorems · Inductive type · category theory

CategoryTheory.Limits.HasStrictInitialObjects

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop

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

Cited by

28 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.Category