scientific article; zbMATH DE number 7204300

DOI10.4230/LIPICS.CSL.2017.8MaRDI QIDQ5111175zbMATH OpenFDO

Authors Benedikt Ahrens, Peter Lefanu Lumsdaine, Vladimir Voevodsky

Publication date 26 May 2020

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2017.8

zbMATH Keywords

categorical semanticstype theoryunivalence axiom

Mathematics Subject Classification ID

Type theory (03B38) Logic in computer science (03B70) Metamathematics of constructive systems (03F50) Categorical semantics of formal languages (18C50) Topological categories, foundations of homotopy theory (55U40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Categorical structures for type theory in univalent foundations
• scientific article; zbMATH DE number 1512620
• Model structures on categories of models of type theories
• Homotopy type theory and Voevodsky's univalent foundations
• Homotopy type theory. Univalent foundations of mathematics
• Univalent semantics of constructive type theories
• Towards formalizing categorical models of type theory in type theory
• UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
• Categorical and algebraic aspects of Martin-Löf type theory
• Cubical methods in homotopy type theory and univalent foundations

Cited in

(8)

• Vladimir Aleksandrovich Voevodsky
• Categorical structures for type theory in univalent foundations
• scientific article; zbMATH DE number 7474655 (Why is no real title available?)
• Cubical methods in homotopy type theory and univalent foundations
• Displayed Categories
• Injective types in univalent mathematics
• A 2-categorical analysis of context comprehension
• Extending equational monadic reasoning with monad transformers

Describes a project that uses

Uses Software

• Coq

This page was built for publication:

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