[Dewie3]

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.

[danghica]

You would still need to program in Agda though :) Cheers!