mathlib3 documentation

algebraic_topology.fundamental_groupoid.punit

Fundamental groupoid of punit #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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