RedPRL

A formalization of the theory behind the mugen library

♾️ A library for universe levels and universe polymorphism

🩺 A library for compiler diagnostics

👹 A library for hierarchical names and lexical scoping

📚 A library for managing libraries and resolving unit paths

🦠 An experimental elaborator for dependent type theory using effects and handlers

🦠 Reusable components based on algebraic effects

🔙 Backward lists for OCaml

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

😎TT