The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.

翻译：Hinze等人的论文《用双代数与分配律排序》运用双代数语义框架来定义排序算法。通过函子间的分配律，他们使用折叠与展开构造出成对的排序算法。由此产生的排序算法对包括插入/选择排序和快速/树排序。我们将此工作扩展至立方Agda中，定义本质正确的变体。我们的核心思想是用多重集索引数据类型，从而简洁地捕捉排序算法以输入列表的有序排列终止的特性。通过将双代数语义提升至索引设定，我们直接从分配律获得了排序算法的正确性。