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 or . These categories tend to be univalent, with a proper underlying groupoid of objects.