Discrete categories are groupoids

instance CategoryTheory.instGroupoidDiscrete {C : Type u_1} : CategoryTheory.Groupoid (CategoryTheory.Discrete C)

Equations

• CategoryTheory.instGroupoidDiscrete = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.Discrete C} (h : X ⟶ Y) => { down := { down := ⋯ } }) ⋯ ⋯