Fundamental groupoid of punit

The fundamental groupoid of punit is naturally isomorphic to CategoryTheory.Discrete PUnit

instance Path.instSubsingletonPathPUnitInstTopologicalSpacePUnitUnit : Subsingleton (Path PUnit.unit PUnit.unit)

instance FundamentalGroupoid.instSubsingletonHomFundamentalGroupoidPUnitToQuiverToCategoryStructToCategoryInstGroupoidFundamentalGroupoidInstTopologicalSpacePUnit {x : FundamentalGroupoid PUnit.{u_1 + 1} } {y : FundamentalGroupoid PUnit.{u_1 + 1} } : Subsingleton (x ⟶ y)

def FundamentalGroupoid.punitEquivDiscretePUnit : FundamentalGroupoid PUnit.{u + 1} ≌ CategoryTheory.Discrete PUnit.{v + 1}

Equivalence of groupoids between fundamental groupoid of punit and punit