Stars
Eventually a practical 2-level TT-based compiler
Educational implementation of a subset of the JVM bytecode to illustrate imperative and object-oriented programming.
formalization of an equivariant cartesian cubical set model of type theory
being a particular fragment of Haskell, extended to a proof system
A proof assistant for higher-dimensional type theory
TeXpresso: live rendering and error reporting for LaTeX
A fancy diagnostics library that allows your compilers to exit with grace
Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos
An experimental proof assistant based on a type theory for synthetic ∞-categories.
Sioyek is a PDF viewer with a focus on textbooks and research papers
A new markup-based typesetting system that is powerful and easy to learn.
Lecture Notes for Algebra Lectures at the University of Bonn
Multimode simple type theory as an Agda library.
🧊 An indexed construction of semi-simplicial and semi-cubical sets
kerodon / kerodon-website
Forked from gerby-project/gerby-websiteTag-based webview of LaTeX documents
📜 marginalia.el - Marginalia in the minibuffer
Hacking synthetic Tait computability into Agda. Example: canonicity for MLTT.
A modern commutative diagram editor for the web.
A collection of tools for writing technical documents that mix Coq code and prose.
A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.
A LaTeX package to reproduce (an enhanced version of) the numbered paragraph style from classic French mathematics books.