RedPRL

😎TT

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

🩺 A library for compiler diagnostics

🦠 Reusable components based on algebraic effects

♾️ A library for universe levels and universe polymorphism

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

👹 A library for hierarchical names and lexical scoping

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

🔙 Backward lists for OCaml

📚 A library for managing libraries and resolving unit paths