Discrete categories are groupoids

@[instance_reducible]

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

Equations

• CategoryTheory.instGroupoidDiscrete = { toCategory := CategoryTheory.discreteCategory C, inv := fun {X Y : CategoryTheory.Discrete C} (h : X ⟶ Y) => { eq := ⋯ }, inv_comp := ⋯, comp_inv := ⋯ }

instance CategoryTheory.instIsGroupoidOfIsDiscrete {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] : IsGroupoid C