(** * Discrete category *)
Require Import HoTT.Basics GroupoidCategory.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

(** 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.