Through the Oregon Programming Languages Summer School videos I became interested in Type Theory over a year ago, and in what little so-called spare time I have these days it has become my primary recreational interest.
I have presented a couple of different talks on the subject over the past few months. A presentation on Homotopy Type Theory which is derived from a prior talk I gave at Tachyus on Type Theory and Practical Application.
A note of caution to anyone diving into Type Theory through anything I have written. I have presented on Type Theory and Hott in particular because there is a lot of interest by programmers in this topic. Preparing and giving both talks was a learning opportunity for me. A lot of questions followed from the perspective of category theory, and fortunately there was usually someone with a background in that area willing to take them. There’s flagrant overreaching in my presentations. Calling path induction “the fundamental theorem of type theory” is way too provocative for a neophyte to attempt, and in introducing the axiom of univalence I did not set up nearly enough introduction for it to make sense. Specifically the equivalence operator needs quite a bit of introduction.
Both my presentations evoked lively discussion and stretched out to two hours. It is really too much to cover in one presentation, even for an introduction. Ideally a follow-up presentation (or two) would be outlined as follows.
- Cover the formation, introduction, elimination, and computation rules for the primary types…and perhaps some of the later specific types introduced in The Hott Book.1
- An in depth look at path induction.
- What is equivalence?
- Only then can function extensionality and univalence have the context necessary for introduction.
- …and cover sets in type theory and mere propositions.
Notes
[1] The HoTT Book, §1.5. This is all math-speak. I will attempt to translate into programmer-speak.
Formation Rule: How one forms a type, the representation syntax.
Introduction Rule: The constructor(s) for forming elements of the type.
Elimination Rule: How to use an element of the type, the usage syntax.
Computation Rule: a.k.a. β-reduction to the theorists. Simply put, using the constructor in an expression.