[GOAL]
x y : Path PUnit.unit PUnit.unit
⊢ x = y
[PROOFSTEP]
ext
[GOAL]
x y : FundamentalGroupoid PUnit
⊢ Subsingleton (x ⟶ y)
[PROOFSTEP]
convert_to Subsingleton (Path.Homotopic.Quotient PUnit.unit PUnit.unit)
[GOAL]
x y : FundamentalGroupoid PUnit
⊢ Subsingleton (Path.Homotopic.Quotient PUnit.unit PUnit.unit)
[PROOFSTEP]
apply Quotient.instSubsingletonQuotient
[GOAL]
x✝ : FundamentalGroupoid PUnit
⊢ (𝟭 (FundamentalGroupoid PUnit)).obj x✝ =
    (Functor.star (FundamentalGroupoid PUnit) ⋙ (Functor.const (Discrete PUnit)).obj PUnit.unit).obj x✝
[PROOFSTEP]
simp
