[sosudo]

Port HoTTLean from Lean v4.25.0-rc2 to Lean and Mathlib v4.34.1, including SynthLean, the groupoid model, and both natural and unstructured model semantics. The unit-type example is now checked against the current groupoid model, and the unstructured interpreter supports independent object and morphism universes.

This branch starts directly from sosudo/HoTTLean:combined at 6d171a58c095239ecbb325872a398e95d234578f, with cleanup applied on top.

• Adapt category wrappers, pullbacks, polynomial constructions, and quoted typechecker proofs to the updated dependencies. Preserve the existing Grothendieck APIs, compatibility declarations, and free groupoid construction.
• Load the restricted theory prelude without changing process-wide import flags or running module initializers; check its imports and initializer requirements before restoring extension data.
• Run all five test modules through lake test, including a permanent regression test for generated functor_map lemmas, nested reassoc/simp attributes, and independent universes. Retain the legacy test.lean import shim.
• Use theorem for proposition-valued declarations, remove redundant instance parameters, qualify ambiguous namespaces, and apply Mathlib formatting conventions.
• Update the README's dependencies, build instructions, and examples while retaining its existing structure. Remove migration evidence and generated website output, and check style on both pushes and pull requests.

The dependency is pinned to the cleaned Lean v4.34.1 port in sinhp/Poly#41, at sosudo/Poly@ba73d51. That port is still awaiting upstream review.

Validation:

• lake -R update
• lake exe cache get
• lake build
• lake build NaturalModel
• lake test
• lake env lean test.lean
• Build the three compatibility modules under HoTTLean.ForMathlib.CategoryTheory: Groupoid, Localization.Predicate, and MorphismProperty.Basic.
• lake -R -Kenv=dev build HoTTLean:docs, followed by restoring the unchanged default manifest.
• Mathlib text-based style linters, legacy indentation/arrow-spacing checks, line-length and precise-import checks, and git diff --check.

The three existing production proof holes in HoTTLean.ForPoly and six production axiom declarations are unchanged from combined. No production proof holes, axioms, or linter suppressions are added.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota. Try requesting a review at a lower effort level.