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

  • BiSikkel, Agda library formalizing a multimode logical framework