This is my attempt at implementing XTT, from the papers "A cubical language for Bishop sets" and "Cubical syntax for reflection-free extensional equality".

Check out some examples in text.xtt, run them with

$ dune exec ./xtt.exe test.xtt

and run a (super minimal) REPL with

$ dune exec ./xtt.exe
> Π (A : Set) (x : A) → pathp i.A x x
<stdin> is well-typed!
it : Set
it = Π (A : Set) → Π (x : A) → pathp i.A x x
>

• Pi types
• Sigma types
• Path types
• coe, com
• Yeah that's about it, inductives (naturals, booleans) are still TO DO