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.
A gaunt category or stiff category is a skeletal category whose core is thin.
Expanding out, this becomes
A gaunt category or stiff category is a category such that the set of isomorphisms between every two objects and of is a subsingleton, and there is an isomorphism if and only if .
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
from the identity type between two objects and to the type of isomorphisms between and 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.
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.
The nerve simplicial set of a category, regarded as a simplicial object in homotopy types under the inclusion , is a complete Segal space precisely if the category is gaunt. More discussion of this is at Segal space – Examples – In Set.
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 , there is an equality , relative to which equals the identity at . Replacing the equality by an isomorphism , 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 be equal to the identity at . 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 , a groupoid , and an essentially surjective functor . In this way, we can view categories as those flagged categories where is an equivalence onto the core of , and strict categories as those flagged categories where 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.)
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.