mathlib documentation

algebraic_topology.fundamental_groupoid.punit

Fundamental groupoid of punit #

The fundamental groupoid of punit is naturally isomorphic to category_theory.discrete punit

@[protected, instance]
def path.subsingleton  :
subsingleton (path punit.star punit.star)