Contents

category theory

# Contents

## Idea

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.

## Definitions

### In set-level foundations

###### Definition

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

Expanding out, this becomes

###### Definition

A gaunt category or stiff category is a category $C$ such that the set of isomorphisms $A \cong B$ between every two objects $A \in Ob(C)$ and $B \in Ob(C)$ of $C$ is a subsingleton, and there is an isomorphism $f:A \cong B$ if and only if $A = 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.

###### Definition

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

Expanded out, this becomes

###### Definition

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) \to (a \cong b)$

from the identity type between two objects $a$ and $b$ to the type of isomorphisms between $a$ and $b$ 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.

## Properties

### 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 $Set \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.

###### Theorem

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 : a \simeq b$, there is an equality $p : a = b$, relative to which $f$ equals the identity at $a$. Replacing the equality $p$ by an isomorphism $g : 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 : a \cong a$ be equal to the identity at $a$. 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 $C$, a groupoid $X$, and an essentially surjective functor $p \colon X \to C$. In this way, we can view categories as those flagged categories where $p$ is an equivalence onto the core of $C$, and strict categories as those flagged categories where $X$ 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.)