Intrinsically Correct Sorting in Cubical Agda. - Cass Alexandru; Vikraman Choudhury; Jurriaan Rot; Niels van der Weide (CPP, 2025)