Harrison's HoPLaAR Agda implementation of Harrison, [2009] "Handbook of Practical Logic and Automated Reasoning" Based on the cubical-mini, agdarsec-cm and prettyng-cm libraries.