# Cubical Syntax for Reflection-Free Extensional Equality

## TL;DR

This paper introduces XTT, a cubical reconstruction of Observational Type Theory that supports function extensionality and UIP, with a focus on algebraic canonicity and practical decidability of typing.

## Contribution

It presents a novel cubical extension of type theory with a canonicity theorem and conjectures practical decidability of the typing relation.

## Key findings

- Establishes an algebraic canonicity theorem for boolean types.
- Introduces a cubical reconstruction of Observational Type Theory.
- Conjectures practical decidability of the typing relation.

## Abstract

We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-L\"of's intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity types principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel cubical extension (independently proposed by Awodey) of the logical families or categorical gluing argument inspired by Coquand and Shulman: every closed element of boolean type is derivably equal to either 'true' or 'false'.