This file defines a few basic properties of groupoids.

theorem CategoryTheory.Groupoid.isThin_iff (C : Type u_1) [Groupoid C] : Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)

def CategoryTheory.Groupoid.IsTotallyDisconnected (C : Type u_1) [Groupoid C] : Prop

A subgroupoid is totally disconnected if it only has loops.

Equations

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