Only the two lines starting with ex1 for heterogeneous if and the two lines starting with ex2 for heterogeneous lists are directly comparable to the Python examples. The rest is just defining what a boolean is, what a natural number is, what a character is, what if is, what a list is, what a heterogeneous list is, etc., to provide a full foundation for the examples.

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.

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