Mathesis Universalis and Homotopy Type Theory

DOI10.1007/978-3-030-20447-1_3zbMath1469.03035OpenAlexW2981433211MaRDI QIDQ3305624

Steven Awodey

Publication date: 10 August 2020

Published in: Mathesis Universalis, Computability and Proof (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-20447-1_3

Mathematics Subject Classification ID

Topological categories, foundations of homotopy theory (55U40) Type theory (03B38)

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The identity type weak factorisation system
• The calculus of constructions
• A small complete category
• Univalence as a principle of logic
• A modern perspective on type theory. From its origins until today
• Weak omega-categories from intensional type theory
• Higher Inductive Types as Homotopy-Initial Algebras
• Topological and Simplicial Models of Identity Types
• The Local Universes Model
• Inductive Types in Homotopy Type Theory
• Types are weak ω -groupoids
• Natural models of homotopy type theory
• Homotopy-Initial Algebras in Type Theory
• Homotopy theoretic models of identity types
• Topological completeness for higher-order logic
• Propositions as [Types]
• Topological representation of the λ-calculus
• Impredicative Encodings of (Higher) Inductive Types
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: Mathesis Universalis and Homotopy Type Theory