Univalent semantics of constructive type theories

DOI10.1007/978-3-642-25379-9_7MaRDI QIDQ3100202zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(15)

• From reversible programs to univalent universes and back
• Univalent foundations of mathematics
• Categorical structures for type theory in univalent foundations
• scientific article; zbMATH DE number 2111733 (Why is no real title available?)
• An Ad-Hoc Semantics to Study Structural Properties of Types
• scientific article; zbMATH DE number 7204300 (Why is no real title available?)
• scientific article; zbMATH DE number 7269245 (Why is no real title available?)
• Stack semantics of type theory
• Injective types in univalent mathematics
• Univalence in locally Cartesian closed categories
• The equivalence of the torus and the product of two circles in homotopy type theory
• A dependently-typed construction of semi-simplicial types
• Combining higher-order logic with set theory formalizations
• A first-order theory of diagram chasing
• On basic semantics of untyped functional programs

Describes a project that uses

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)