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)

Equations

• 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)

Equations

• (_ : Subsingleton (x ⟶ y)) = (_ : 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

Equations

• One or more equations did not get rendered due to their size.