[sosudo]

Update HoTTLean from Lean v4.25.0-rc2 to Lean and Mathlib v4.34.1. The port covers SynthLean, the groupoid model, and both natural and unstructured model semantics. lake test now checks all five test modules, including the previously omitted unit-type interpretation in the groupoid model.

• Adapt category wrappers, pullback proofs, metaprogramming APIs, and quoted typechecker proofs to the new dependencies. Reuse Mathlib's free groupoid construction while retaining compatibility names.
• Generalize the unstructured interpreter to independent object and morphism universes, as needed by the groupoid interpretation.
• Add regression coverage for generated functor_map lemmas, nested reassoc/simp attributes, and the term elaborator with independent universes.
• Use theorem for proposition-valued declarations, remove redundant tactics and instance parameters, and apply Mathlib formatting conventions.
• Keep the README's existing structure while updating dependencies, build commands, and tested examples. Remove migration reports and generated website output from the proposed tree, and run style checks on pull requests as well as pushes.

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 -R -Kenv=dev build HoTTLean:docs (then restore the unchanged default manifest).
• Build the three compatibility modules not reached by the default targets: Groupoid, Localization.Predicate, and MorphismProperty.Basic under HoTTLean.ForMathlib.CategoryTheory.
• Mathlib text-based style linters, legacy indentation/arrow-spacing checks, the repository's line-length and precise-import checks, and git diff --check.

Existing unfinished proofs in HoTTLean.ForPoly remain. This change adds no production proof holes or axioms.

[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.