Library HoTT.Categories.Category.Strict

Definition of a strict category

Require Export Category.Core.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.

Quoting the HoTT Book: Definition. A strict category is a precategory whose type of objects is a set.

Notation IsStrictCategory C := (IsHSet (object C)).

Record StrictCategory :=
  {
    precategory_strict :> PreCategory;
    isstrict_StrictCategory :> IsStrictCategory precategory_strict
  }.

Existing Instance isstrict_StrictCategory.