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

Idea

In a (infinity,1)-category, the notion of terminal 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 from any other object there is a unique morphism into the terminal object, in a quasi-category there is a contractible infinity-groupoid of such morphisms, i.e. the morphism to the terminal object is unique up to homotopy.

Incarnations

In quasi-categoires

Let $C$ be a quasi-category and $c \in C$ one of its objects (a vertex in the corresponding simplicial set). The object $c$ is a terminal object in $C$ if the following equivalent conditions hold:

• The projection from the over quasi-category $C_{/c} \to C$ is a trivial fibration of simplicial sets.

• For every object $d$ of $C$ the right hom Kan-complex into $c$ is contractible:

$$Hom_C^R(d,c) \simeq {*} \,.$$

In simplicial type theory

Let $A$ be a type in simplicial type theory. An element $y:A$ is a terminal object if for all elements $x: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 terminal object in an (infinity,1)-category. However, the fact that this definition works for any type $A$ implies that terminal 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-terminal object

• terminal object in a 2-category

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

References

A quick survey of terminal objects in quasicategories is on page 159 of

• André Joyal, The theory of quasicategories and its applications, lectures at Simplicial Methods in Higher Categories, (pdf)

For more details see definition 1.2.12.3, p. 46 in

• Jacob Lurie, Higher Topos Theory

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

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