Contents

# Contents

## Idea

XTT is an set-level cubical type theory developed by Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. While it might seem that XTT should stand for “X type theory”, the authors have stated that XTT isn’t an acronym and doesn’t stand for anything.

XTT features boundary separation, which implies UIP as a theorem of XTT, rather than an axiom as in Martin-Löf type theory. As a result, it is an example of a cubical type theory which is not a homotopy type theory.

Additionally, XTT has regularity, canonicity, and certain higher inductive types like propositional truncation. It is an open question if it additionally has decidable type checking and normalization.