The authors of "Observational equality, now!" write: > We have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system. However I can find no trace of that implementation. Any hint? Thanks, JP.