I'm a bit sad the he doesn't mention univalent foundations, which is based on ∞-groupoids instead of sets.