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.
(** * Discrete category *)
Require Import HoTT.Basics GroupoidCategory.Core.
Set Implicit Arguments.
Generalizable All Variables.
(** A discrete category is a groupoid which is a 0-type *)
Module Export Core.
Definition discrete_category X `{IsHSet X} := groupoid_category X.
Arguments discrete_category X {_} / .
End Core.