Neovim support for the Lean theorem prover

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

antifunext

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 markup-based typesetting system that is powerful and easy to learn.

Lecture Notes for Algebra Lectures at the University of Bonn

A Teeny Type Theory

Multimode simple type theory as an Agda library.

my phd thesis

🧊 An indexed construction of semi-simplicial and semi-cubical sets

Tag-based webview of LaTeX documents

📜 marginalia.el - Marginalia in the minibuffer

A dependent type theory with user defined data types

Hacking synthetic Tait computability into Agda. Example: canonicity for MLTT.

Documentation compiler for OCaml

A modern commutative diagram editor for the web.

A collection of tools for writing technical documents that mix Coq code and prose.