module Cat.Skeletal where

# Skeletal precategoriesπ

A precategory
$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

which we can more concisely summarise as β$(β₯ββββ₯,β₯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
$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!β©οΈ