open import Cat.Prelude

module Cat.Strict where

Strict precategories🔗

We call a precategory strict if its type of objects is a Set.

is-strict : ∀ {o ℓ} → Precategory o ℓ → Type o
is-strict C = is-set ⌞ C ⌟

Strictness is a very strong condition to impose on categories, since it classifies the “categories-as-algebras”, or petit, view on categories, which regards categories themselves as set-level structures, which could be compared to monoids or groups. For example, the path category on a directed graph is naturally regarded as strict. Moreover, strict categories form a precategory.

This is in contrast with the “categories-as-universes”, or gros, view on categories. From this perspective, categories serve to organise objects at the set-level, like $\mathbf{Mon}$ or $\mathbf{Grp}$. These categories tend to be univalent, with a proper underlying groupoid of objects.