Naive cubical type theory

DOI10.1017/S096012952200007XMaRDI QIDQ5055495zbMATH OpenOpenAlexFDO

Authors Bruno Bentzen

Publication date 9 December 2022

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

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

zbMATH Keywords

cubical type theoryhomotopy type theoryinformal type theorynaive type theory

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Canonicity for cubical type theory
• On higher inductive types in cubical type theory
• Syntax and models of Cartesian cubical type theory
• Cubical methods in homotopy type theory and univalent foundations

Cites work

• A cubical model of homotopy type theory
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Cubical type theory: a constructive interpretation of the univalence axiom
• Homotopy theoretic models of identity types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 3450200 (Why is no real title available?)
• scientific article; zbMATH DE number 2110617 (Why is no real title available?)
• Naïve Type Theory
• On higher inductive types in cubical type theory
• Syntax and models of Cartesian cubical type theory
• UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
• Weak omega-categories from intensional type theory

Cited in

(1)

• scientific article; zbMATH DE number 2110617 (Why is no real title available?)

Describes a project that uses

Uses Software

• cart-cube
• cubicaltt
• GitHub

This page was built for publication: Naive cubical type theory

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