Univalence, set theory and mechanized proof boundaries
Research context
theory comparison · conditional · As of 2026-10-10
Univalence states that the canonical map from identity of types in a universe to equivalence of types is itself an equivalence.
Key knowledge
Univalence states that the canonical map from identity of types in a universe to equivalence of types is itself an equivalence. A higher inductive circle adds a point and a loop, with dependent elimination rules. These provide a structural foundation different from ZFC's sets and membership; neither framework is an empirical theory competing to fit data. Relative semantic models support particular consistency claims, while a proof assistant verifies a formal statement relative to its exact axioms and trusted checker.
Values and equations
idtoeqv:(A=_U B)→Equiv(A,B) is an equivalence
- U
- Specified univalent universe
- A,B
- Types in U
- Equiv(A,B)
- Type of equivalences between A and B
Conditions and scope
- Univalence is an additional principle for a specified universe, not a theorem of arbitrary intensional type theory.
- The HoTT rules, ZFC axioms and Lean's actual kernel theory are distinct systems; Lean is not automatically a HoTT implementation.
- Machine checking does not verify that the formalized theorem faithfully expresses the intended informal claim.
Sources · 2
References
Sources retain their recorded scope. A source link alone does not establish verification of every statement.
Evidence and review
Author checked this English statement, displayed equation where present and stated hypotheses against these source locations: Chapters 1–3 type/identity rules, §2.10 axiom 2.10.3, §6.4 circle and higher inductive types; appendices on semantics; Theorem statement meaning, kernel checks, axiom audits and native evaluation trust; current page checked 10 October 2026. The check is bounded to the recorded claims; no complete proof reconstruction, software proof replay or universal literature completeness is claimed.
2026-10-10 · Author source-body/statement/equation/domain check, with graph associations scoped individually. Separate independent content/source/inventory review is required before branch closure.
Entry details
Permanent link to this entry ↗- Record identity
- research-math-univalence-foundation-comparison
- Revision
- research.1
- Structured reference record
- Postgraduate & research reference