xtt
xtt copied to clipboard
mb64
A simple implementation of XTT, "A cubical language for Bishop sets"
XTT, probably
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
>
Features
- Pi types
- Sigma types
- Path types
coe,com- Yeah that's about it, inductives (naturals, booleans) are still TO DO
mb64