Higher Observational Type Theory

Working alternative to Cubical Type Theory. Has Definitional Univalance.

Status

No formal definition. No formal implementaiton. We don’t know if we can make Higher OTT.

Desiderata

Definitional Univalance

If you map from an equivalence to a equality and map back, then you end up with something that is ‘effectively equal’ but not Definitionally Equal

Can figure it out from pre-mathematical concepts

Effiecient

t[x\mapsto u] $$ is primitive when $t$ and $u$ are [[intervals]]. ## Firency Fibrency gives the $J$ computation. ## Concepts [[BCH Cube Category]] [[Parameticity Axiom]]