Intro to HoTT No. 5, Part 3
17 May 2024
In this video, we conduct a formal development of product types in Agda, to complement our earlier informal developments (the product operation on homotopy spaces) and formalization in the HoTT deductive calculus. We use some function combinators to implement integer division in Agda and Haskell, running into some trouble with nontermination along the way.
Intro to HoTT No. 5, Part 2
13 November 2023
In this video, we conduct a formal development of product types in the HoTT deductive calculus, formalizing our informal work from the previous video. This provides an occasion to refine our intuitions for what Beta and Eta Computation rules mean.
Intro to HoTT No. 5, Part 1
20 August 2023
In this video, we take an informal look at what it means to "multiply" homotopy spaces. These "product types" play a central role in type theory, especially in the logic interpretation (as we'll discuss in a future video).
Intro to HoTT No. 5, Part 0
05 March 2023
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.
Intro to HoTT No. 4, Part 1
02 November 2022
In this video, we discuss the deductive rules governing arrow types: the application rule, the lambda abstraction rule, and the β & η rules.
Intro to HoTT No. 4, Part 0
12 October 2022
In this video, we incorporate into type theory a central feature of logic: implications. Along the way, we encounter the work of the ancient Greek philosopher Theophrastus, the modern work of Brouwer, Heyting, and Kolmogorov, and end up doing computer programming. Quite a journey!
Intro to HoTT No. 3, Part 1
30 June 2022
Boolean logic is an important part of computer science, both at the hardware level and the software level. Can we do boolean logic in HoTT? Of course we can! In this video, I give our first example of the iteration and computation rules for a type, which are how we use types. With booleans, this corresponds to gate-like constructs called multiplexers and to the ubiquitous 'if-then-else' construction of programming languages.
Intro to HoTT No. 3, Part 0
20 June 2022
Boolean logic is an important part of computer science, both at the hardware level and the software level. Can we do boolean logic in HoTT? Of course we can! This video shows how to recreate the logic of boolean circuits and logic gates, both in informal HoTT and in our Agda formalization of HoTT.
Intro to HoTT No. 2, Part 3
09 June 2022
In this video, I bring together everything covered in Parts 0, 1, and 2 with an example: the days of the week!
Intro to HoTT No. 2, Part 2
27 May 2022
An essential piece of HoTT is judgmental equality, which is how we state that two things are "equal by definition". In this video, I explain (what I consider to be) the most helpful intuition for judgmental equality: computational confluence. Two terms (or types) in HoTT are judgmentally equal if they can be computed to the same thing. This turns out to be a fruitful way to think of judgmental equality, particularly because computer formalization is important to us. Later on, we'll improve upon judgmental equality to get another notion of equality, propositional equality, which is the central object of study in homotopy type theory.
Intro to HoTT No. 2, Part 1
20 May 2022
How do we do Homotopy Type Theory? In this video, I cover some of the fundamentals of working in Agda (the computer formalization system we'll be using in these videos) and the basic concepts of HoTT as a formal language: judgments, inference rules, formation and introduction.
Intro to HoTT No. 2, Part 0
20 May 2022
How do we do Homotopy Type Theory? This is another question with three answers: homotopy type theorists will "dress" their work in three different styles -- informal reasoning, computer formalization, and as inference rules in a deductive system. In these videos, I describe these three styles of HoTT and how a successful homotopy type theorist navigates between them.
Intro to HoTT No. 1, Part 3
30 April 2022
What does homotopy type theory mean? This video presents our third answer: HoTT is a logical calculus for constructively proving statements (especially mathematical claims). This is by way of the famed "Curry-Howard Correspondence", which connects type theory with constructive logic. Along the way, we encounter important notions like proof relevance, unique existence, and (un)inhabitedness. We also go through our first example in Agda, and meet one of the main characters of homotopy type theory: refl.
Intro to HoTT No. 1, Part 2
25 April 2022
What does homotopy type theory mean? This video presents the next answer: HoTT is a language for describing spaces. Under this interpretation, the unit type 1 represents the space consisting of just a single point. This video informally introduces the idea of "contractibility", which we'll rigorously define later and use extensively throughout HoTT.
Intro to HoTT No. 1, Part 1
06 April 2022
What does homotopy type theory mean? This video presents the first answer: HoTT is a typed programming language. Under this interpretation, the unit type 1 is the type of zero-tuples, a standard feature in many typed programming languages.
Intro to HoTT No. 1, Part 0
04 April 2022
What does homotopy type theory mean? This is a question which has three distinct answers, connecting the language of HoTT to the rich worlds of functional programming, homotopy theory, and constructive logic.
Intro to HoTT No. 0
05 March 2022
What is homotopy type theory good for? In this video, I discuss the ideas of type-checking and formalized mathematics, and begin to describe how HoTT promises a new future for mathematics.
