Noughts & Crosses: Set Interpretation [Intro to HoTT, No. 5, Part 0]
Channel: jacobneu
Date: 2023-03-05

Links and more: https://intro-hott.video/videos/5/part0

In this video, we return to the homotopy interpretation and explore its simpler edge cases, sets! In particular, we look at an edge case of sets, the empty set.

Video site for the series: https://intro-hott.video
Youtube: https://www.youtube.com/playlist?list=PL245PKGUDdcN9-El9D7DRefwX4c9feiYq
Instagram: @Intro_HoTT
Twitter: @Intro_HoTT

Formalization links:
- Appeared in this video: https://github.com/jacobneu/HoTT-agda/blob/main/01-simpleTT.agda
- The formalization I'm developing for this video series: https://github.com/jacobneu/HoTT-agda
- The formalization it's based on (by Egbert Rijke, for his upcoming textbook): https://github.com/HoTT-Intro/Agda
- More up-to-date HoTT formalization in Agda: https://github.com/UniMath/agda-unimath

HoTT textbooks:
- The HoTT Book (2013) -- the original statement of HoTT: https://homotopytypetheory.org/book/
- Introduction to Homotopy Type Theory, by Egbert Rijke (to be released): https://ncatlab.org/nlab/show/Introduction+to+Homotopy+Type+Theory

Image/audio credits:
- "Wholesome" by Kevin MacLeod (incompetech.com); CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/)

Homotopy type theory (HoTT) is a new branch of type theory and a new foundation for mathematics. It serves as a common language for reasoning about computation (functional programming), about mathematical structure (synthetic homotopy theory and higher category theory), and about constructive logic. This Introduction to Homotopy Type Theory video lecture series is intended to explain what HoTT is, show how to work in HoTT (including how formalization in Agda works), and give intuition for why HoTT is the way it is. I don’t assume any particular background familiarity, but the more you know about mathematics, computer science, and logic, the more you’ll be able to get out of these videos. Enjoy!