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) (a : c ⟶ d), c = d