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 $\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

which we can more concisely summarise as “$(\Vert -\cong -\Vert ,\Vert \mathrm{id}\Vert )$ 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¹. 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 $\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.