Naive cubical type theory

DOI10.1017/S096012952200007XOpenAlexW2985011261MaRDI QIDQ5055495

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

homotopy type theorycubical type theoryinformal type theorynaive type theory

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• cubicaltt
• GitHub
• cart-cube

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A cubical model of homotopy type theory
• Weak omega-categories from intensional type theory
• Homotopy theoretic models of identity types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Syntax and models of Cartesian cubical type theory
• On Higher Inductive Types in Cubical Type Theory
• UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Naïve Type Theory

This page was built for publication: Naive cubical type theory