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.

## Equations

- CategoryTheory.Groupoid.IsTotallyDisconnected C = ∀ (c d : C), (c ⟶ d) → c = d