Fundamental groupoid of punit #
The fundamental groupoid of punit is naturally isomorphic to CategoryTheory.Discrete PUnit
Equations
instance
FundamentalGroupoid.instSubsingletonHomPUnit
{x : FundamentalGroupoid PUnit.{u_1 + 1} }
{y : FundamentalGroupoid PUnit.{u_1 + 1} }
:
Subsingleton (x ⟶ y)
Equations
- ⋯ = ⋯
@[simp]
theorem
FundamentalGroupoid.punitEquivDiscretePUnit_counitIso :
FundamentalGroupoid.punitEquivDiscretePUnit.counitIso = CategoryTheory.Iso.refl
(((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{v + 1} )).obj { as := PUnit.unit }).comp
(CategoryTheory.Functor.star (FundamentalGroupoid PUnit.{u + 1} )))
@[simp]
@[simp]
Equivalence of groupoids between fundamental groupoid of punit and punit
Equations
- One or more equations did not get rendered due to their size.