3 problems

Let $\BCTT{}$ denote bicubical type theory, a variant of simplicial type theory based on two layers of cubical type theory, with one interval for homotopy type theory and another f…

Canonicity conjecture. Adding these rules suffices to preserve canonicity.

In a type theory with UIP or $n$-truncatedness introduced only as a path equality, one considers refining the theory while retaining the surrounding type-theoretic structure. Stric…