This file defines a few basic properties of groupoids.
theorem
CategoryTheory.Groupoid.isThin_iff
(C : Type u_1)
[CategoryTheory.Groupoid C]
:
Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)
A subgroupoid is totally disconnected if it only has loops.