Towards a cubical type theory without an interval

DOI10.4230/LIPICS.TYPES.2015.3zbMATH1434.03035OpenAlexW2949164661MaRDI QIDQ4580224FDOQ4580224

Authors Thorsten Altenkirch, Ambrus Kaposi

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

univalenceparametricityhomotopy type theory

Mathematics Subject Classification ID

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

Recommendations

• Internal parametricity for cubical type theory
• Model structures on categories of models of type theories
• Cubical type theory: a constructive interpretation of the univalence axiom
• Canonicity for cubical type theory
• scientific article; zbMATH DE number 6694181

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• A computational interpretation of parametricity
• A presheaf model of parametric type theory
• A relationally parametric model of dependent type theory
• Big-step normalisation
• Computational higher-dimensional type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Extensionality of \(\lambda^*\)
• Homotopy type theory. Univalent foundations of mathematics
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• Type theory in type theory using quotient inductive types
• Type-theory in color

Cited in

(2)

• Internal parametricity for cubical type theory
• From cubes to twisted cubes via graph morphisms in type theory

Describes a project that uses

Uses Software

• cubicaltt

This page was built for publication: Towards a cubical type theory without an interval

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