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

source
@[protected, instance]
def path.subsingleton  :
subsingleton (path punit.star punit.star)
source
@[protected, instance]
def fundamental_groupoid.quiver.hom.subsingleton {x y : fundamental_groupoid punit} :
subsingleton (x ⟶ y)
source
noncomputable def fundamental_groupoid.punit_equiv_discrete_punit  :
fundamental_groupoid punit ≌ category_theory.discrete punit

Equivalence of groupoids between fundamental groupoid of punit and punit

Equations