Univalent Semantics of Constructive Type Theories

DOI10.1007/978-3-642-25379-9_7zbMath1250.03121OpenAlexW188158278MaRDI QIDQ3100202

Vladimir Voevodsky

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_7

zbMATH Keywords

Martin-Löf identity typespolymorphic type theoriestype-theoretic foundations of mathematicsunivalent semantics

Mathematics Subject Classification ID

Related Items (3)

The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory ⋮ Combining higher-order logic with set theory formalizations ⋮ Univalence in locally Cartesian closed categories

Uses Software

• Coq

This page was built for publication: Univalent Semantics of Constructive Type Theories