Some necessary ingrediences in the end of the HoTT book. (In an old version, it was around p.44 and at the very end.)

A year ago I asked a relevant related question here

http://cstheory.stackexchange.com/questions/27400/minimal-specification-of-martin-l%C3%B6f-type-theory

Think about what would be a good order of introduction (using WAT) (see Outline). E.g. adding 5+3 would be among the very first things to do. For educational purposes, talking about $\to, \times$ before more intricate concepts is also a good idea. As I thought about before, going bottom (Hands on stuff) to top (abstract minimalistic stuff) with the typey/computational/constructive stuff should be a good idea. Then, for sets and cats, it's the other other way around.

\prod

And I mean “Stuff that eventually needs to be available to do basic computation”, otherwise the answer is “everything”.

notions to play around with

$\to$

$\lambda.$

${\mathbb N}$

$0, 1, 2, 3, 4, 5, 6, 7, 8, 9$

$+, *$

• Basic computational playgrounds like ${\mathbb N}\to{\mathbb N}$ and basic numerical LaTeX expressions should be a first starting point.
• As it's always easy to translate any syntax to something that's valuable TeX, the first step is to take must-have concepts in Intutionistic type theory and translate them to their LaTeX output.
• Before I don't know which dependent language(s) I'll map the dependent type aspect into, there is harm in introducing a broader spectrum of Basic notions (e.g. $A\to B$ is $\Pi_{x:A}B(x)$ for $x$-Independent $B$, but I'll want to have $\to$ from the get-go, I don't know the last Thing about how people check if $B$ is free of $x$, etc.)
• Of course, I'll want a write a fraction-of-LaTeX to WAT parser as well! The issue arising here is the fact that some languages overload their expressions, and the the parser must be intelligent. Even worse, in LaTeX operations like multiplication of numbers are not expressed with a particular syntax ($3\dots 7, 3\ 7, 3*7, \dots$)

WAT