nLab initial object in an (infinity,1)-category

Idea

In a (infinity,1)-category, the notion of initial object known from ordinary category theory is relaxed in the homotopy theoretic sense to the suitable notion in (∞,1)-category theory:

instead of demanding that to any other object there is a unique morphism from the initial object, in a quasi-category there is a contractible infinity-groupoid of such morphisms, i.e. the morphism from the initial object is unique up to homotopy.

Incarnations

In simplicial type theory

Let $A$ be a type in simplicial type theory. An element $x:A$ is an initial object if for all elements $y:A$, the hom-type $\mathrm{hom}_A(x, y)$ is a contractible type.

If $A$ is a Segal type then this notion coincides with the usual notion of initial object in an (infinity,1)-category. However, the fact that this definition works for any type $A$ implies that initial objects should be definable in any simplicial infinity-groupoid or simplicial object in an (infinity,1)-category, not just the $(\infty,1)$-categories or category objects in an (infinity,1)-category.

Related concepts

• initial object, terminal object

• h-initial object

• initial object in a 2-category

• terminal object in an (infinity,1)-category

References

For more details see section 1.2.12, p. 45 in

• Jacob Lurie, Higher Topos Theory

Initial objects in $(\infty,1)$-categories are defined in

• Denis-Charles Cisinski, Bastiaan Cnossen, Hoang Kim Nguyen, Tashi Walde, section 5.5 of: Formalization of Higher Categories, work in progress (pdf)