He explicitly gives standard machinery like the a boolean type and natural numbers, presumably to show more clearly what the parts are built up from. You probably wouldn't need to write all of that to use HList at a later point.