Intrinsically Correct Sorting in Cubical Agda.

Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide

Browse the full CPP paper archive.