Egbert Rijke

HoTT-Intro. An introductory course to Homotopy Type Theory

GraphModel. We formalize aspects of the graph model of type theory

CategoryTheory_Course. Documents for the course on Category theory

OEIS-A000001. Agda

sequential_colimits. Lean

HoTT-Rosetta. Pairing natural language of the intro to HoTT book with agda formalization

hott_cmu80818. Companion code to CMU course on Homotopy Type Theory

EPIT-2020. EPIT 2020 - Spring School on Homotopy Type Theory

CMU. This repository contains projects (presentations, notes, etc...) that I do for my PhD

formally_etale. TeX

K-theory. This project is about formalizing some results in K-theory in homotopy type theory.

book. A textbook on informal homotopy type theory

notes-cubical. Notes on cubical sets

alg. Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.