open import Cat.Instances.Discrete
open import Cat.Prelude
open import Cat.Strict

import Cat.Reasoning

open Cat.Reasoning using (Isomorphism ; id-iso)
open Precategory using (Ob)

module Cat.Skeletal where

Skeletal precategoriesπŸ”—

A precategory 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 β€œ 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 identity1. 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.

module _ {o β„“} (C : Precategory o β„“) where

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 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.

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