Univalent semantics of constructive type theories

DOI10.1007/978-3-642-25379-9_7zbMATH Open1250.03121OpenAlexW188158278MaRDI QIDQ3100202FDOQ3100202

Authors: 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

Recommendations

• Homotopy Type Theory
• The simplicial model of univalent foundations (after Voevodsky)
• Univalent foundations of mathematics
• Homotopy type theory
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory

zbMATH Keywords

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

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Topological categories, foundations of homotopy theory (55U40)

Cited In (10)

• The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory
• Title not available (Why is that?)
• On basic semantics of untyped functional programs
• Univalence in locally Cartesian closed categories
• Combining higher-order logic with set theory formalizations
• Title not available (Why is that?)
• Injective types in univalent mathematics
• Univalent foundations of mathematics
• Categorical structures for type theory in univalent foundations
• Title not available (Why is that?)

Uses Software

• Coq

This page was built for publication: Univalent semantics of constructive type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100202)