As an ongoing side-project, I sporadically create various teaching resources, mostly colorful explainer videos, which I upload 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!
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.
YouTube
youtube.com/@jacobneu-videosA Generalized Algebraic Theory of Directed Equality
jacobneu.phd/docs/resources
To accompany my PhD thesis, I made a website, jacobneu.phd, documenting the ideas behind it. I've started to create some accompanying YouTube videos. See the website (specifically its 'Resources' page) for more!
Intro to HoTT
(2022—Present)
From early on in my PhD studies, I've been producing an introduction to Homotopy Type Theory. These videos are loosely based on Egbert Rijke's Introduction to Homotopy Type Theory, and includes demonstrations of the Agda theorem prover.
Designs
FroCoS-ITP-TABLEAUX 2025
Main site
The 2025 instance of the FroCoS, ITP and TABLEAUX conferences (and accompanying Lean and Rocq workshops) took place at Reykjavik University, where I was a postdoc. I was heavily involved in the organization and running of the conference, and was responsible for editing & uploading the talk recordings after the conference. See here for the page I put together listing all the talks, slides, and recordings. I also designed the programme booklet—click the image on the right to see it.
FP Lab (University of Nottingham)
While I was in the FP Lab at Nottingham (for my PhD studies), I designed a logo for the group (and ordered some custom coffee mugs with the logo!). I was also asked to design a poster for the group, based on content put together by Tom de Jong. Click on the images to the right for the full-size posters.
Heyting Day 2025
I designed this poster for Heyting Day 2025 — Models of intuitionism and computability. Thanks to Tom de Jong for the oppotunity, and for giving feedback on draft designs.
Old videos
(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.