Sorting algorithms are fundamental to computer science, and their correctness criteria are well understood as rearranging elements of a list according to a specified total order on the underlying set of elements. As mathematical functions, they are functions on lists that perform combinatorial operations on the representation of the input list. In this paper, we study sorting algorithms conceptually as abstract sorting functions. There is a canonical surjection from the free monoid on a set (lists of elements) to the free commutative monoid on the same set (multisets of elements). We show that sorting functions determine a section (right inverse) to this surjection satisfying two axioms, that do not presuppose a total order on the underlying set. Then, we establish an equivalence between (decidable) total orders on the underlying set and correct sorting functions. The first part of the paper develops concepts from universal algebra from the point of view of functorial signatures, and gives constructions of free monoids and free commutative monoids in (univalent) type theory. Using these constructions, the second part of the paper develops the axiomatisation of sorting functions. The paper uses informal mathematical language, and comes with an accompanying formalisation in Cubical Agda.

翻译：排序算法是计算机科学的基础，其正确性准则被广泛理解为根据底层元素集上指定的全序关系对列表元素进行重排。作为数学函数，排序函数是对列表进行组合运算的函数，作用于输入列表的表征。本文从概念上将排序算法视为抽象排序函数进行研究。存在一个从集合上自由幺半群（元素列表）到同一集合上自由交换幺半群（元素多重集）的典范满射。我们证明排序函数确定了该满射的一个截面（右逆）且满足两个公理，这些公理并不预设底层集合上的全序关系。随后，我们建立了底层集合上的（可判定）全序关系与正确排序函数之间的等价性。论文第一部分从函子签名的视角发展泛代数概念，并在（单值）类型论中给出自由幺半群与自由交换幺半群的构造。基于这些构造，论文第二部分发展排序函数的公理化体系。本文采用非形式化的数学语言，并附带Cubical Agda的形式化实现。