module Cat.Skeletal where

# Skeletal Precategoriesπ

A precategory
$\mathcal{C}$
is **skeletal** if objects having *the property of being
isomorphic* are identical. The clunky rephrasing is proposital: if
we had merely said βisomorphic objects are identicalβ, then skeletality
sounds too much like univalence, from
which it is distinct. Instead, skeletality is defined as (equivalent to)
the existence of a map

$\| a \cong b \| \to a \equiv b\text{,}$

which we can more concisely summarise as β$(\| - \cong - \|, \| \mathrm{id}_{} \|)$ is an identity systemβ.

is-skeletal : β {o β} β Precategory o β β Type (o β β) is-skeletal C = is-identity-system (Ξ» x y β β₯ Isomorphism C x y β₯) (Ξ» x β inc (id-iso C)) path-from-has-isoβis-skeletal : β {o β} (C : Precategory o β) β (β {a b} β β₯ Isomorphism C a b β₯ β a β‘ b) β is-skeletal C path-from-has-isoβis-skeletal C sk = set-identity-system (Ξ» _ _ β squash) sk

Skeletality is much rarer than univalence in practice, and univalence is
the more useful condition, since it allows facts about isomorphism to
transfer to identity^{1}. Skeletality, in our sense, serves
as a point of comparison for *other* properties: if a property
implies skeletality, we can safely regard it as unnatural.

One of the reasons skeletality is unnatural is it implies the category is strict.

skeletalβstrict : is-skeletal C β is-strict C skeletalβstrict skel = identity-systemβhlevel 1 skel (Ξ» _ _ β squash)

Furthermore, skeletality does *not* imply univalence, as
objects in
$\mathcal{C}$
may have non-trivial automorphisms. The walking involution is the
simplest example of a non-univalent, skeletal precategory. In general,
we prefer to work with gaunt, not skeletal,
categories.

Indeed, it also allows general facts about identity to transfer to isomorphism!β©οΈ