Towards a Cubical Type Theory without an Interval

DOI10.4230/LIPIcs.TYPES.2015.3zbMath1434.03035OpenAlexW2949164661MaRDI QIDQ4580224

Ambrus Kaposi, Thorsten Altenkirch

Publication date: 13 August 2018

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2018/8473/pdf/LIPIcs-TYPES-2015-3.pdf/

zbMATH Keywords

univalencehomotopy type theoryparametricity

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Related Items (1)

Unnamed Item

Uses Software

• cubicaltt

Cites Work

• Unnamed Item
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• Type theory in type theory using quotient inductive types
• A Computational Interpretation of Parametricity
• Big-step normalisation
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Type-theory in color
• Extensionality of lambda
• Computational higher-dimensional type theory
• A relationally parametric model of dependent type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• A presheaf model of parametric type theory

This page was built for publication: Towards a Cubical Type Theory without an Interval