Towards a cubical type theory without an interval

DOI10.4230/LIPICS.TYPES.2015.3zbMATH Open1434.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/

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 Keywords

univalenceparametricityhomotopy type theory

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

• Title not available (Why is that?)
• Internal parametricity for cubical type theory

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)