Natural models of homotopy type theory

DOI10.1017/S0960129516000268zbMath1456.03023arXiv1406.3219OpenAlexW2962920088MaRDI QIDQ3130300

Steven Awodey

Publication date: 11 January 2018

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1406.3219

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Type theory (03B38)

Related Items (14)

Bicategories in univalent foundations ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ A general framework for the semantics of type theory ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Unnamed Item ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The universal exponentiable arrow ⋮ Unnamed Item ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed

Cites Work

• Relating first-order set theories, toposes and categories of classes
• The identity type weak factorisation system
• Exponentiable morphisms, partial products and pullback complements
• Variations on the bagdomain theme
• Categorical properties of logical frameworks
• Topological and Simplicial Models of Identity Types
• The Local Universes Model
• Homotopy theoretic models of identity types
• Internal type theory
• Polynomial functors and polynomial monads
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Natural models of homotopy type theory