mathlib3

192819b4 - feat(category_theory/punit): A groupoid is equivalent to punit iff it has a unique arrow between any two objects (#12726)

feat(category_theory/punit): A groupoid is equivalent to punit iff it has a unique arrow between any two objects (#12726) In terms of topology, when this is used with the fundamental groupoid, it means that a space is simply connected (we still need to define this) if and only if any two paths between the same points are homotopic, and contractible spaces are simply connected.