yeah it is a hard read. a relatively easier read is PLFA in Agda.