My blog posts

• Four proofs of the four lemma A pointless homological overcomplication.
• Quotients as identifications
• Binders Here, Binders There, Binders Everywhere disambiguating binders in system F and beyond
• Complex Numbers Are Matrices

My projects

• The Styff programming language online playground. Try it! (WARNING: abundoned project :/)
• MyOwnTT - an implementation of dependent type theory with dependent records.
• An example implementation for type checking system F using pure bidi.