From cubes to twisted cubes via graph morphisms in type theory

DOI10.4230/LIPICS.TYPES.2019.5MaRDI QIDQ6079232zbMATH OpenFDO

Authors Nicolai Kraus

Publication date 27 October 2023

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

zbMATH Keywords

homotopy type theorycubical setsgraph morphismsdirected equality

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• A Constructive Model of Directed Univalence in Bicubical Sets
• Cubical methods in homotopy type theory and univalent foundations
• Towards a directed homotopy type theory
• Higher Structures in Homotopy Type Theory
• Cubical type theory: a constructive interpretation of the univalence axiom

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 1860105 (Why is no real title available?)
• scientific article; zbMATH DE number 3370546 (Why is no real title available?)
• 2-Dimensional Directed Type Theory
• A cubical model of homotopy type theory
• A model for the homotopy theory of homotopy theory
• A type theory for synthetic \(\infty\)-categories
• Cohomology of small categories
• Cubical type theory: a constructive interpretation of the univalence axiom
• Extending homotopy type theory with strict equality
• Geometric realisations of cubical sets with connections, and classifying spaces of categories
• Higher Topos Theory (AM-170)
• Homotopy type theory. Univalent foundations of mathematics
• The Frobenius condition, right properness, and uniform fibrations
• The univalence axiom for elegant Reedy presheaves
• Towards a cubical type theory without an interval
• Towards a directed homotopy type theory
• Univalence for inverse diagrams and homotopy canonicity
• Varieties of cubical sets

Cited in

(1)

• Transpension: the right adjoint to the Pi-type

This page was built for publication: From cubes to twisted cubes via graph morphisms in type theory

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