As an ongoing side-project, I sporadically create various teaching resources, mostly colorful slide decks about topics in logic, type theory, and category theory. I'm in the process of recording lectures using some of these slide decks and uploading them to my YouTube Page. I hope to eventually make videos about topology, category theory, logic, functional programming, philosophy, type theory, and all the topics which interest me; but for now, I'm focused on producing an introduction to Homotopy Type Theory. These videos are loosely based on Egbert Rijke's Introduction to Homotopy Type Theory.
Everything below should be considered a work-in-progress, and updates to this page will be irregular. Except where noted, the content below is my own work and is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License. You are highly encouraged to share, modify, and adapt the content below (subject to the terms of the license) — please contact me if you would like the source/original images for anything below.
Recent Work
Formalities & Informalities
How do we do homotopy type theory? In these four videos, I introduce the various ways in which homotopy type theorists do their work. In particular, I cover how informal written HoTT can be formalized into the computer proof assistant Agda, as well as the mysterious "inference rules" which type theorists sometimes use to communicate. This includes a discussion of the idea of judgmental equality, which is an important notion in HoTT, particularly when contrasted with the central construct of study in HoTT: propositional equality. In Part 3, I do an example of type construction in HoTT: the days of the week!
Three for One
Among the most fascinating aspects of homotopy type theory are its manifold interpretations. In particular, homotopy type theory can be thought about as a programming language, as a language for describing hyper-dimensional shapes, and as a logical calculus. By viewing HoTT as a common language for these three pursuits, we gain lots of new intuition for what the objects of HoTT mean, and we are able to study well-known phenomena from new perspectives. In these videos, I introduce this threefold interpretation of HoTT, and explore how one particular type, the unit type 1 means something different in each domain.
Was soll HoTT?
The introduction video of the Intro to HoTT series, covering the motivation for homotopy type theory and computer-formalized mathematics. I discuss how some results in modern-day mathematics have become too difficult to adequately verify without computer assistance, and explain how typed programming languages promise a solution.
Old (2021)
Martin-Löf Type Theory
The first lecture of the Intro to HoTT video series, corresponding roughly to Chapter 1 of Rijke's Introduction. Covers the main intuitions and motivations behind homotopy type theory (including the homotopy interpretation of types and the Curry-Howard correspondence), formal languages and deduction, the judgments, structural rules, & derivations of Martin-Löf Type Theory, the type of booleans, binary product types, and arrow types.
Theory of the Category of Sets
An introduction to the constructions possible within the category of sets (without assuming any category theory knowledge). Loosely inspired by Lawvere's Elementary Theory of the Category of Sets and Sets for Mathematics. Covers sets, functions & lambda-notation, composition, universal mapping properties (of the empty set, singleton sets, injective & surjective functions, binary products, exponentials, (co)equalizers, fiber products), global elements, bijections, disjoint union, recursion on the natural numbers, subset classification (characteristic functions and inclusions), Cantor's Theorem, set comprehension, equivalence relations, kernels, and images.