Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
(** * 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.