Prototype implementation of the mathematical framework, with basic user interface, user documentation and gallery of examples of type theories.

  • Andromeda, a proof checker for user-definable dependently-typed theories

  • Narya, a proof assistant for higher-dimensional type theory

  • Lambdapi, a proof assistant for dependent type theory modulo user-defined rewriting rules