Univalence as a principle of logic

DOI10.1016/j.indag.2018.01.011zbMath1437.03168OpenAlexW2811094863MaRDI QIDQ1788330

Steven Awodey

Publication date: 8 October 2018

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.indag.2018.01.011

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Metamathematics of constructive systems (03F50) Homotopical algebra, Quillen model categories, derivators (18N40) Type theory (03B38)

Related Items

Higher Structures in Homotopy Type Theory, Mathesis Universalis and Homotopy Type Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Set-theoretical invariance criteria for logicality
• Homotopy theoretic models of identity types
• What are logical notions?
• Cohesive Toposes and Cantor's 'lauter Einsen'
• Type Theory and Homotopy
• A Machine-Checked Proof of the Odd Order Theorem
• Homotopy Type Theory: Univalent Foundations of Mathematics