Mike Shulman

catlog. Categorical logic from a categorical point of view

ohtt. H.O.T.T. using rewriting in Agda

cohesivett. Cohesive type theory

dirtt. Directed type theory for formal category theory

basictex. My basic LaTeX macros and BibTeX file.

Coq-HoTT. Homotopy type theory

hott-categories. Categories and the Rezk completion formalized in HoTT

agda-infinity-categories. Infinity categories in agda

ddcalc. Notes on calculus

cubicaltt. Experimental implementation of Cubical Type Theory

syntop. Constructive topology

agda-nr-cats. (n,r)-categories in agda

math494. Lean

book. A textbook on informal homotopy type theory

Homotopy. Homotopy type theory

pgm. TeX

emacs_chrome. A Chromium "clone" of It's All Text for spawning an editor to edit text areas in browsers. Based on David Hilley's original Chromium extension.