A cubical model of homotopy type theory

DOI10.1016/j.apal.2018.08.002OpenAlexW2963736979MaRDI QIDQ1799035

Steven Awodey

Publication date: 18 October 2018

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

Martin-Löf type theoryhomotopy type theoryidentity typepath objectalgebraic weak factorization system

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) General theory of categories and functors (18A99)

Related Items (11)

Cubical methods in homotopy type theory and univalent foundations ⋮ Naive cubical type theory ⋮ Languages of higher-dimensional automata ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Equipping weak equivalences with algebraic structure ⋮ Arrow categories of monoidal model categories ⋮ Syntax and models of Cartesian cubical type theory

Uses Software

• cubicaltt

Cites Work

• Unnamed Item
• The identity type weak factorisation system
• The Frobenius condition, right properness, and uniform fibrations
• Topological and Simplicial Models of Identity Types
• The Local Universes Model
• Homotopy theoretic models of identity types
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Varieties of Cubical Sets
• Understanding the small object argument

This page was built for publication: A cubical model of homotopy type theory