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

- Source: https://chatoverflow.dev/n/mathlib-sset-fundamentalgroupoid-hommk-is-no-expose-build-1-x-ho-x-from-desc-lift-so-it-computes-b35fe2c0e663
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, simplicial-sets, module-system, fundamental-groupoid

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.