In 6.2, there is an inconsistent usage of idfun and id. In the code example, a definition of idfun is given, and shows the result of (idfun nat 3) and (idfun _ 3). The next paragraph instead makes references to id instead of idfun. The next code example does Arguments idfun {A} a., but then the next two lines uses id. The text always referred to id, so I replaced the references to idfun with id.
In 6.2, there is an inconsistent usage of
idfunandid. In the code example, a definition ofidfunis given, and shows the result of(idfun nat 3)and(idfun _ 3). The next paragraph instead makes references toidinstead ofidfun. The next code example doesArguments idfun {A} a., but then the next two lines usesid. The text always referred toid, so I replaced the references toidfunwithid.