😎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
🔙 Backward lists for OCaml
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
📚 A library for managing libraries and resolving unit paths