Skip to content

MLTT Internalization

Choose a tag to compare

@5HT 5HT released this 04 Jul 01:14
  • Fibrant MLTT-style ΠΣ primitives with Leibniz equality in 500 LOC
  • Cofibrant CHM-style I primitives with pretypes hierarchy Vₙ in 500 LOC
  • Generalized Transport
  • Parser in 80 LOC
  • Lexer in 80 LOC