jsNarya: Higher-dimensional type theory in your browser

Narya is an experimental proof assistant for Higher/Parametric/Displayed Observational Type Theory; see the README for current features.
JsNarya is compiled with Js_of_ocaml to run in a browser. Currently only the command-line interactive mode is available, but you can copy and paste arbitrary code in the "Extra startup" box to be executed before starting interactive mode. Please report bugs.

Extra startup: