cart-cube

MaRDI QIDQ46473swMATHFDO

Official website https://github.com/dlicata335/cart-cube/

Source code repository https://github.com/dlicata335/cart-cube/

Cited in

(13)

• Model structure on the universe of all types in interval type theory
• Naive cubical type theory
• HoTT
• cubicaltt
• RedPRL
• Models of type theory based on Moore paths
• Cubical methods in homotopy type theory and univalent foundations
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Cubical Agda
• Constructive sheaf models of type theory
• Internal universes in models of homotopy type theory
• Syntax and models of Cartesian cubical type theory
• An introduction to univalent foundations for mathematicians

This page was built for software: cart-cube