nLab gaunt category




A category is called gaunt if all its isomorphisms are in fact identities. This is a property of strict categories; that is, it is not invariant under equivalence of categories. See below for some related concepts that are invariant.

Every gaunt category is skeletal, but not conversely. Every gaunt category is also univalent; the converse holds in set-level foundations but not in the higher foundations where univalent categories are usually considered. More generally, gaunt categories are precisely the categories that are both strict and univalent.


In set-level foundations


A gaunt category or stiff category is a skeletal category CC whose core is thin.

Expanding out, this becomes


A gaunt category or stiff category is a category CC such that the set of isomorphisms ABA \cong B between every two objects AOb(C)A \in Ob(C) and BOb(C)B \in Ob(C) of CC is a subsingleton, and there is an isomorphism f:ABf:A \cong B if and only if A=BA = B.

In type theory

In a dependent type theory with some notion of identity type or path type, there is another definition of gaunt category available.


A gaunt category or stiff category is a strict univalent category.

Expanded out, this becomes


A gaunt category or stiff category is a category whose type of objects is 0-truncated and which additionally satisfies a condition called Rezk completeness: the canonical function

idtoiso:(a=b)(ab)idtoiso : (a=b) \to (a \cong b)

from the identity type between two objects aa and bb to the type of isomorphisms between aa and bb is an equivalence of types.

In set-level type theory, the type theoretic definition and the set-level definitions are equivalent to each other. For in this case, every identity type is a proposition/subsingleton. Thus, by the Rezk completeness condition, the set of isomorphisms is a subsingleton, and two objects which are isomorphic to each other are also equal to each other.



Relation to other properties of categories

Gaunt categories are necessarily skeletal; a skeletal category is gaunt iff every automorphism is an identity morphism. Consequently a thin gaunt category is skeletal, and since a thin skeletal category is a poset category a thin gaunt category is also a poset category.

Note that a gaunt category need not be thin, since we may have parallel non-isomorphisms which are not equal. Similarly, a thin category need not be gaunt since we may have isomorphisms that aren’t the identity.

The core of a gaunt category is a set.

Relation to complete Segal spaces

The nerve simplicial set of a category, regarded as a simplicial object in homotopy types under the inclusion SetGrpdSet \hookrightarrow \infty Grpd, is a complete Segal space precisely if the category is gaunt. More discussion of this is at Segal space – Examples – In Set.

In higher foundations

As noted above, in higher foundations the gaunt categories are precisely the strict and univalent categories. Thus, every property which is satisfied of strict categories and univalent categories apply to gaunt categories.

In addition, we have


The Rezk completion of a core-thin category is a gaunt category.

To make sense of the definition of a gaunt category, we need to use equality of objects: For every isomorphism f:abf : a \simeq b, there is an equality p:a=bp : a = b, relative to which ff equals the identity at aa. Replacing the equality pp by an isomorphism g:abg : a \simeq b, the resulting condition holds for all categories. This echoes how one might understand the definition in univalent foundations: the univalence condition for a univalent category is another way of saying that every isomorphism is an identity (and uniquely so).

Alternatively, we could avoid the equality on objects by requiring only that every automorphism f:aaf : a \cong a be equal to the identity at aa. This amounts to requiring that the core be a thin category, i.e., that parallel isomorphisms are equal. A category has this property if and only if it is equivalent to a gaunt one.

Incidentally, we may view both strict categories and categories up to equivalence as embedded in the type of flagged categories. Recall that a flagged category consists of a category CC, a groupoid XX, and an essentially surjective functor p:XCp \colon X \to C. In this way, we can view categories as those flagged categories where pp is an equivalence onto the core of CC, and strict categories as those flagged categories where XX is a set (up to homotopy: an “h-set”): see at category with an atlas. The intersection of categories-up-to-equivalence and strict categories within the type of flagged categories is then exactly this type of core-thin categories. (This is the semantics in Gpd of the fact that in homotopy type theory, the gaunt categories are precisely the strict and univalent categories.)

See also


The term “gaunt category” was apparently introduced in

in the context of a discussion of (infinity,n)-categories.

In the Elephant, gaunt categories are briefly mentioned under the name “stiff categories”, in the paragraph preceding B1.3.11 (about splitting of Grothendieck fibrations).

Last revised on February 1, 2024 at 12:30:59. See the history of this page for a list of all contributions to it.