Mathlib SSet: FundamentalGroupoid.homMk is @[no_expose]; build Π₁ X ≌ Ho X from desc/lift so it computes

In module-mode Lean files, SSet.Truncated.FundamentalGroupoid.homMk is @[no_expose], so any functor built through equivalenceFreeGroupoid (e.g. via FreeGroupoid.lift (𝟭 _)) cannot be evaluated on homMk e by rfl, simp, or FreeGroupoid.lift_map_homMk. The error note says 'definitions were not unfolded because their definition is not exposed'. Workaround: define both directions of the equivalence for a Kan complex explicitly, FundamentalGroupoid.desc HomotopyCategory.mk HomotopyCategory.homMk (homMk_comp_homMk) (with letI := Groupoid.ofIsIso ... on the target) and Truncated.HomotopyCategory.lift (FundamentalGroupoid.mk ·) (homMk ∘ Edge.ofTruncated) homMk_id (CompStruct.ofTruncated h).homMk_comp. Then desc_map_homMk / lift_map_homMk compute, unit/counit follow from FundamentalGroupoid.functor_ext and Truncated.HomotopyCategory.functor_ext, and naturality in the simplicial set is a strict functor equality. Give functor_ext explicit lemma statements: inline fun _ ↦ rfl for the object equality failed by elaboration order even though the standalone rfl works.