Symmetries in Sorting

Symmetries in Sorting Vikraman Choudhury # University of Strathclyde, Glasgow, United Kingdom Wind Wong # Vrije Universiteit Amsterdam, Netherlands Abstract 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 axiomatization of sorting functions. The paper uses informal mathematical language, and comes with an accompanying formalisation in Cubical Agda. 2012 ACM Subject Classification Theory of computation →Type theory; Theory of computation →Logic and verification; Theory of computation →Constructive mathematics Keywords and phrases universal algebra, type theory, homotopy type theory, cubical Agda, constructive mathematics, univalent mathematics, sorting, combinatorics, formalisation Supplementary Material Formalisation:windtf/agda-symmetries [9] Funding Vikraman Choudhury: Supported by the EU Marie-Skłodowska-Curie action “ReGraDeCS”, grant №101106046. Wind Wong: Supported by the European Research Council Starting Grant for the project “SecuStack”, funded under the European Union’s Horizon Europe grant №101115046. Acknowledgements This project was carried out as part of Wind Wong’s undergraduate thesis at University of Glasgow, supervised by Simon Gay. We are grateful to Simon for his guidance and support. We are also grateful to Fredrik Nordvall Forsberg, and the reviewers of the HoTT/UF 2024 meeting, for their helpful comments and suggestions. 1 Introduction Consider a puzzle about sorting, inspired by Dijkstra’s Dutch National Flag problem [ 12 , Ch.14]. Suppose there are balls of three colors, corresponding to the colors of the Dutch flag: red, white, and blue. {, , } Given an unordered list (bag) of such balls, how many ways can you sort them into the Dutch flag? *,,,,,,,+ 2 Symmetries in Sorting Obviously there is only one way, decided by the order the colors appear in the Dutch flag: red <white <blue. [,,,,,,,] What if we are avid enjoyers of vexillology who also want to consider other flags? We might ask: how many ways can we sort our unordered list of balls? We know there are exactly 3! = 6 permutations of {red,white,blue} , so there are 6 possible orderings we can define. In fact, there are exactly 6 such categories of tricolor flags (see Wikipedia). We have no allegiance to any of the countries presented by the flags, hypothetical or otherwise – this is purely a matter of combinatorics. We posit that, because there are exactly 6 orderings, we can only define 6 extensionally correct sorting functions. Formally, there is a bijection between the set of orderings on a carrier set 𝐴 and the set of correct sorting functions on lists of 𝐴 . In fact, a sorting function can be correctly axiomatized just from this point of view, which is our main contribution. Outline and Contributions In§2, we describe a formalisation of universal algebra developed from the point of view of functorial signatures, the definition and universal property of free algebras, and algebras satisfying an equational theory. In § 3, we give constructions of free monoids, and proofs of their universal property. Following this, in § 4, we add symmetry to each representation of free monoids, and extend the proofs of universal property from free monoids to free commutative monoids. These are standard constructions that we formalise conceptually by formal combinatorics. In § 5, we build on the previous constructions and study sorting functions. The main result connects total orders, sorting, and symmetry, by proving an equivalence between decidable total orders on a carrier set 𝐴, and correct sorting functions on lists of 𝐴. Finally, § 6discusses related and future work. The three main parts of the paper may be read independently. Readers interested in the formalisation of universal algebra may start from § 2. Readers interested in the constructions of free monoids and free commutative monoids may skip ahead to §§ 3and 4. If the reader already believes in the existence of free algebras for monoids and commutative monoids, they can directly skip to the application section on sorting, in § 5. Although the formalisation is a contribution in itself, the purpose of the paper is not to directly discuss the formalisation, but to present the results in un-formalised form (in type-theoretic foundations), so the ideas are accessible to a wider audience. All the results of this paper are formalised in Cubical Agda, and the formalisation artifact is available at [9]. 2 Universal Algebra We first develop some basic notions from universal algebra and equational logic [ 5 ], which gives us a vocabulary and framework to express our results in. The point of view we take is the standard category-theoretic approach to universal algebra, which predates the Lawvere theory or abstract clone point of view. We keep a running example of monoids in mind, while explaining and defining the abstract concepts. V. Choudhury and W. Wong 3 2.1 Algebras ▶ Definition 1 ( Ó Signature).A signature, denoted 𝜎 , is a (dependent) pair consisting of a set of operations, op:Set, and an arity function for each operation, ar:op →Set. ▶ Example 2. A premonoid is a set with an identity element (a nullary operation), and a binary multiplication operation, with signature 𝜎Mon ≔(Fin2, 𝜆{0↦→ Fin0; 1 ↦→ Fin2}). Every signature 𝜎induces a signature functor 𝐹𝜎on Set. ▶Definition 3 (ÓSignature functor). 𝑋↦→ (𝑜:op) × 𝑋ar(𝑜)𝑋𝑓 −→ 𝑌↦→ (𝑜:op) × 𝑋ar(𝑜)(𝑜,−◦ 𝑓) −−−−−−→ (𝑜:op) × 𝑌ar(𝑜) ▶ Example 4. The signature functor for monoids, 𝐹𝜎Mon , assigns to a carrier set 𝑋 , the set of inputs for each operation. Expanding the dependent product on Fin2 , we obtain a coproduct of sets: 𝐹𝜎Mon (𝑋) ≃ 𝑋Fin0+𝑋Fin2≃1+𝑋×𝑋. A 𝜎 -structure is given by a carrier set, with functions interpreting each operation symbol. The signature functor applied to a carrier set gives the inputs to each operation, and the output is simply a map back to the carrier set. These two pieces of data constitute an algebra for the 𝐹𝜎 functor. We write 𝔛 for a 𝜎 -structure with carrier set 𝑋 , following the model-theoretic notational convention. ▶ Definition 5 ( Ó Structure).A 𝜎 -structure 𝔛 is an 𝐹𝜎 -algebra, that is, a pair consisting of a carrier set 𝑋, and an algebra map 𝛼𝑋:𝐹𝜎(𝑋) → 𝑋. ▶Example 6. Concretely, an 𝐹𝜎Mon -algebra has the type 𝛼𝑋:𝐹𝜎Mon (𝑋) → 𝑋≃ (1+𝑋×𝑋) → 𝑋≃ (1→𝑋)×(𝑋×𝑋→𝑋) which is the pair of functions interpreting the two operations. Natural numbers N with ( 0 ,+) or (1,×) are examples of monoid structures. ▶ Definition 7 ( Ó𝜎 -Homomorphism).A homomorphism between 𝜎 -structures 𝔛 and 𝔜 is a morphism of 𝐹𝜎 -algebras, that is, a map 𝑓:𝑋→𝑌 making the following diagram commute: 𝐹𝜎(𝑋)𝑋 𝐹𝜎(𝑌)𝑌 𝛼𝑋 𝐹𝜎(𝑓)𝑓 𝛼𝑌 ▶ Example 8. Given two monoids 𝔛 and 𝔜 , the top half denotes: 1+ (𝑋×𝑋)𝛼𝑋 −−→ 𝑋𝑓 −→ 𝑌 , which applies 𝑓 to the output of each operation, and the bottom half denotes the map: 1+ (𝑋×𝑋)𝐹𝜎Mon (𝑓) −−−−−−−−→ 1+ (𝑌×𝑌)𝛼𝑌 −−→ 𝑌 . In other words, a homomorphism between 𝑋 and 𝑌 is a map 𝑓 on the carrier sets that commutes with the interpretation of the monoid operations, or simply, preserves the monoid structure. For a fixed signature 𝜎 , the category of 𝐹𝜎 -algebras and their morphisms form a category of algebras, written 𝐹𝜎-Alg , or simply, 𝜎-Alg , given by the obvious definitions of identity and composition of the underlying functions. 4 Symmetries in Sorting 2.2 Free Algebras The concrete category 𝜎-Alg of structured sets and structure-preserving maps admits a forgetful functor 𝑈:𝜎-Alg →Set . In our notation, 𝑈(𝔛) is simply 𝑋 , a fact we exploit to simplify our notation, and formalisation. The left adjoint to this forgetful functor is the free algebra construction, also known as the term algebra (or the absolutely free algebra without equations). We rephrase this in more concrete terms. ▶Definition 9 (ÓFree Algebras).A free 𝜎-algebra construction consists of the following: a set 𝐹(𝑋), for every set 𝑋, a𝜎-structure on 𝐹(𝑋), written as 𝔉(𝑋), a universal map 𝜂𝑋:𝑋→𝐹(𝑋), for every 𝑋, such that, for any 𝜎 -algebra 𝔜 , the operation assigning to each homomorphism 𝑓:𝔛→𝔜 , the map 𝑓◦𝜂𝑋:𝑋→𝑌(or, post-composition with 𝜂𝑋), is an equivalence. In other words, we ask for a bijection between the set of homomorphisms out of the free algebra to any other algebra, and the set of functions from the carrier set of the free algebra to the carrier set of the other algebra. There should be no more data in homomorphisms out of the free algebra than there is in functions out of the carrier set, which is the property of freeness. The inverse operation to post-composing with 𝜂𝑋 extends a function to a homomorphism. Note that the free algebra on the empty set 𝔉( 0 ) is inhabited by all the constant symbols in the signature. ▶ Definition 10 ( Ó Universal extension).The universal extension of a function 𝑓:𝑋→𝑌 to a homomorphism out of the free 𝜎 -algebra on 𝑋 is written as 𝑓♯:𝔉(𝑋) → 𝔜 . It satisfies the identities: 𝑓♯◦𝜂𝑋=𝑓,𝜂𝑋♯=id𝔉(𝑋), and (𝑔♯◦𝑓)♯=𝑔♯◦𝑓♯. Free algebra constructions are canonically equivalent. ▶ Proposition 11 ( Ó ).If 𝔉(𝑋) and 𝔊(𝑋) are free 𝜎 -algebras on 𝑋 , then 𝔉(𝑋) ≃ 𝔊(𝑋) in 𝜎-Alg, naturally in 𝑋, via the canonical extensions. Proof. By extending 𝜂𝑋 for each free construction, we have maps in each direction: 𝐺·𝜂𝑋♯:𝔉(𝑋) → 𝔊(𝑋) , and vice versa. Finally, using Definition 10, we have 𝐹·𝜂𝑋♯◦𝐺·𝜂𝑋♯= (𝐹·𝜂𝑋♯◦𝐺·𝜂𝑋)♯=𝐹·𝜂𝑋♯=id𝔉(𝑋).◀ ▶Proposition 12. The free algebra construction gives a monad on Set. Proof. 𝐹 is an endofunctor on Set where the action on functions is given by 𝑋𝑓 −→ 𝑌↦→ 𝐹(𝑋)(𝜂𝑌◦𝑓)♯ −−−−−−−→ 𝐹(𝑌) . The monad unit is given by 𝜂 , and multiplication given by 𝜇𝑋≔ 𝐹(𝐹(𝑋)) id𝐹(𝑋)♯ −−−−−−→ 𝐹(𝑋).◀ ▶Proposition 13. The following properties of free algebras on 0, 1, and coproducts hold: 𝜎-Alg(𝔉(0),𝔛)is contractible, if 𝜎has one constant symbol, then 𝔉(0)is contractible, the type of algebra structures on 1is contractible, 𝔉(𝑋+𝑌) is the coproduct of 𝔉(𝑋) and 𝔉(𝑌) in 𝜎-Alg : 𝜎-Alg(𝔉(𝑋+𝑌),ℨ) ≃ 𝜎-Alg(𝔉(𝑋),ℨ) × 𝜎-Alg(𝔉(𝑌),ℨ). Proof. 𝐹 being a left adjoint, preserves coproducts. This makes 𝔉( 0 ) initial in 𝜎-Alg . 𝔉( 1 ) → 1is contractible because 1is terminal in Set.◀ V. Choudhury and W. Wong 5 We have discussed specifications of free algebras, but not actually given a construction. In type theory, free constructions are often given by inductive types, where the constructors are the pieces of data that freely generate the structure, and the type-theoretic induction principle enforces the category-theoretic universal property. ▶ Definition 14 ( Ó Construction of Free 𝜎 -algebras).The free 𝜎 -algebra on a type 𝑋 is given by the inductive type Tree(𝑋), generated by two constructors: leaf :𝑋→Tree(𝑋) node:𝐹𝜎(Tree(𝑋)) → Tree(𝑋) The constructors leaf and node are the generators for the universal map, and the algebra map, respectively. Together, they describe the type of abstract syntax trees for terms in the signature 𝜎 – the leaves are the free variables, and the nodes are the branching operations of the tree, marked by the operations in 𝜎. ▶Example 15. A tree for 𝜎Mon with the carrier set Nwould look like: 2 1 1 + + 𝑒 ▶Proposition 16 (Ó).(Tree(𝑋),leaf)is the free 𝜎-algebra on 𝑋. 2.3 Equations The algebraic framework described so far only captures operations, not equations. These algebras are lawless (or wild or absolutely free) – 𝐹𝜎Mon -algebras are premonoids rather than monoids, and 𝔉𝜎Mon -algebras are free premonoids, not free monoids, since they are missing the unit and associativity laws. For example, by associativity, these two trees of (N,+) should be identified as equal. 2 1 1 + + 2 1 1 + + To impose equations on the generated abstract syntax trees, we adopt the point of view of equational logic. ▶ Definition 17 ( Ó Equational Signature).An equational signature, denoted 𝜀 , is a (dependent) pair consisting of: a set of names for equations, eq:Set , and an arity of free variables for each equation, fv:eq →Set. ▶ Example 18. The equational signature for monoids 𝜀Mon is: (Fin3, 𝜆{ 0 ↦→ Fin1 ; 1 ↦→ Fin1 ; 2 ↦→ Fin3}) . The three equations are the left and right unit laws, and the associativity law – a 3-element set of names {unitl,unitr,assoc} . The two unit laws use one free variable, and the associativity law uses three free variables. Similar to the term signature functor in Definition 3, this produces an equational signature functor on Set. 6 Symmetries in Sorting ▶Definition 19 (ÓEq. Signature Functor). 𝑋↦→ (𝑒:eq) × 𝑋fv(𝑒)𝑋𝑓 −→ 𝑌↦→ (𝑒:eq) × 𝑋ar(𝑒)(𝑒,−◦ 𝑓) −−−−−−→ (𝑒:eq) × 𝑌ar(𝑒) To build equations out of this, we use the 𝜎 -operations and construct trees for the left and right-hand sides of each equation using the free variables available. ▶ Definition 20 ( Ó System of Equations).A system of equations over a signature (𝜎, 𝜀) is a pair of natural transformations: 𝓁,𝓇:𝐹𝜀⇒𝔉𝜎. For any set (of variables) 𝑉 , this gives a pair of functions 𝓁𝑉,𝓇𝑉:𝐹𝜀(𝑉) → 𝔉𝜎(𝑉) , and naturality ensures correctness of renaming. ▶Example 21. Given 𝑥:𝑉,𝓁𝑉(unitl,(𝑥)),𝓇𝑉(unitl,(𝑥)) are defined as: 𝑒 𝑥 • 𝑥 Given 𝑥:𝑉,𝓁𝑉(unitr,(𝑥)),𝓇𝑉(unitr,(𝑥)) are defined as: 𝑥 𝑒 • 𝑥 Given 𝑥, 𝑦, 𝑧 :𝑉,𝓁𝑉(assocr,(𝑥, 𝑦, 𝑧)),𝓇𝑉(assocr,(𝑥, 𝑦, 𝑧)) are defined as: 𝑥 𝑦 𝑧 • • 𝑥 𝑦 𝑧 • • Finally, we say how a given 𝜎 -structure 𝔛 satisfies the system of equations 𝑇(𝜎,𝜀) . We need to assign a value to each free variable in the equation in the carrier set, using a valuation function 𝜌:𝑉→𝑋 . Given such an assignment, we evaluate the left and right trees of the equation, by extending 𝜌 with Definition 10, that is by construction, a homomorphism from 𝔉(𝑉)to 𝔛. To satisfy an equation, these two evaluations should agree. ▶ Definition 22 ( Ó Satisfaction 𝔛⊨𝑇 ).A 𝜎 -structure 𝔛 satisfies the system of equations 𝑇(𝜎,𝜀)if for every set 𝑉, and every assignment 𝜌:𝑉→𝑋,𝜌♯is a (co)fork: 𝐹𝜀(𝑉)𝔉(𝑉)𝔛 𝜌♯ 𝓁𝑉 𝓇𝑉 Given a signature (𝜎, 𝜀) with a system of equations 𝑇(𝜎,𝜀) , the 𝜎 -algebras satisfying 𝑇(𝜎,𝜀) , or varieties, form a full subcategory of 𝜎-Alg . While free algebras exist for any signature 𝜎 as in Definition 14, constructions of free varieties for arbitrary systems of equations require non-constructive principles [ 6 , § 7, pg.142], in particular, the arity sets need to be projective – we do not pursue this matter further. We have a rudimentary framework for universal algebra and equational logic, which gives us enough tools to develop the next sections. V. Choudhury and W. Wong 7 3 Constructions of Free Monoids In this section, we consider various constructions of free monoids in type theory, with proofs of their universal property. Since each construction satisfies the same categorical universal property, by Proposition 11, these are canonically equivalent (hence equal, by univalence) as types (and as monoids), allowing us to transport proofs between them. Using the universal property allows us to define and prove our programs correct in one go, which we use in § 5. 3.1 Lists Cons-lists are simple inductive datatypes, well-known to functional programmers, and are a common representation of free monoids in programming languages. More generally, they correspond to list objects [10,20] and algebraically-free monoids [17] in category theory. ▶Definition 23 (ÓLists).List(A)is generated by the following constructors: nil:List(𝐴) −:: −:𝐴→List(𝐴) → List(𝐴) The (universal) generators map is the singleton: 𝜂𝐴(𝑎)≔[𝑎] ≡ 𝑎:: nil , the identity element is the empty list nil, and the monoid multiplication ++ is given by list concatenation. ▶ Definition 24 (Concatenation).We define the concatenation operation ++:List(𝐴) → List(𝐴) → List(𝐴), by recursion on the first argument: nil ++ys =ys (𝑥:: xs) ++ ys =𝑥:: (xs ++ ys) The proof that ++ satisfies monoid laws is straightforward (see the formalisation for details). ▶ Definition 25 (Universal extension).For any monoid 𝔛 , and given a map 𝑓:𝐴→𝑋 , we define the extension 𝑓♯:List(𝐴) → 𝔛by recursion on the list: 𝑓♯(nil)=𝑒 𝑓♯(𝑥:: xs)=𝑓(𝑥) • 𝑓♯(xs) ▶ Proposition 26 ( Ó ). (−)♯ lifts a function 𝑓:𝐴→𝑋 to a monoid homomorphism 𝑓♯:List(𝐴) → 𝔛. Proof. To show that 𝑓♯ is a monoid homomorphism, we need to show 𝑓♯(xs ++ ys)=𝑓♯(xs) • 𝑓♯(ys). We can do so by induction on xs. Case nil : 𝑓♯(nil ++ys)=𝑓♯(ys) , and 𝑓♯(nil) • 𝑓♯(ys)=𝑒•𝑓♯(ys)=𝑓♯(ys) by definition of (−)♯. Therefore, we have 𝑓♯(nil ++ys)=𝑓♯(nil) • 𝑓♯(ys). 8 Symmetries in Sorting Case 𝑥:: xs: 𝑓♯((𝑥:: xs) ++ ys) =𝑓♯(([𝑥] ++ xs) ++ ys)by definition of concatenation =𝑓♯([𝑥] ++ (xs ++ ys)) by associativity =𝑓♯(𝑥:: (xs ++ 𝑦𝑠)) by definition of concatenation =𝑓(𝑥) • 𝑓♯(xs ++ ys)by definition of (−)♯ =𝑓(𝑥)•(𝑓♯(xs) • 𝑓♯(ys)) by induction =(𝑓(𝑥) • 𝑓♯(xs)) • 𝑓♯(ys)by associativity =𝑓♯(𝑥:: xs) • 𝑓♯(ys)by definition of (−)♯ Therefore, (−)♯does correctly lift a function to a monoid homomorphism. ◀ ▶Proposition 27 (ÓUniversal property for List).(List(𝐴), 𝜂𝐴)is the free monoid on 𝐴. Proof. To show that (−)♯ is an inverse to −◦𝜂𝐴 , we first show (−)♯ is the right inverse to −◦𝜂𝐴 . For all 𝑓 and 𝑥 , (𝑓♯◦𝜂𝐴)(𝑥)=𝑓♯(𝑥:: nil)=𝑓(𝑥) • 𝑒=𝑓(𝑥) , therefore by function extensionality, for any 𝑓,𝑓♯◦𝜂𝐴=𝑓, and (−◦𝜂𝐴)◦(−)♯=𝑖𝑑. To show (−)♯ is the left inverse to −◦𝜂𝐴 , we need to prove for any monoid homomorphism 𝑓:List(𝐴) → 𝔛,(𝑓◦𝜂𝐴)♯(xs)=𝑓(xs). We can do so by induction on xs. Case nil : (𝑓◦𝜂𝐴)♯(nil)=𝑒 by definition of the (−)♯ operation, and 𝑓(nil)=𝑒 by homomorphism properties of 𝑓. Therefore, (𝑓◦𝜂𝐴)♯(nil)=𝑓(nil). Case 𝑥:: xs: (𝑓◦𝜂𝐴)♯(𝑥:: xs) =(𝑓◦𝜂𝐴)(𝑥)•(𝑓◦𝜂𝐴)♯(xs)by definition of (−)♯ =(𝑓◦𝜂𝐴)(𝑥) • 𝑓(xs)by induction =𝑓([𝑥]) • 𝑓(xs)by definition of 𝜂𝐴 =𝑓([𝑥] ++ xs)by homomorphism properties of 𝑓 =𝑓(𝑥:: xs)by definition of concatenation By function extensionality, (−)♯◦ (−◦𝜂𝐴)=𝑖𝑑 . Therefore, (−)♯ and (−) ◦ [_] are inverse of each other. We have now shown that (−) ◦ 𝜂𝐴 is an equivalence from monoid homomorphisms List(𝐴) → 𝔛 to set functions 𝐴→𝑋 , and its inverse is given by (−)♯ , which maps set functions 𝐴→𝑋 to monoid homomorphisms List(𝐴) → 𝔛 . Therefore, List is indeed the free monoid. ◀ 3.2 Arrays An alternate (non-inductive) representation of the free monoid on a carrier set, or alphabet 𝐴 , is 𝐴∗ , the set of all finite strings or sequences of characters drawn from 𝐴 , as in [ 13 ]. We call this an array, which is a pair of a natural number 𝑛 , denoting the length of the array, and a lookup (or index) function Finn→𝐴 , mapping indices to elements of 𝐴 . In type theory, this is also understood as a container [ 1 ], where the type of shapes is a 𝑛:N , and the type of positions for each shape is Finn, where the array elements are stored. V. Choudhury and W. Wong 9 ▶Definition 28 (ÓArrays). Array(𝐴)≔(𝑛:N)×(Finn→𝐴) For example, ( 3 , 𝜆{ 0 ↦→ 3 , 1 ↦→ 1 , 2 ↦→ 2 }) represents the same list as [ 3 , 1 , 2 ] . The (universal) generators map is the singleton: 𝜂𝐴(𝑎)=( 1 , 𝜆{ 0 ↦→ 𝑎}) , the identity element is ( 0 , 𝜆{}) and the monoid operation ++ is given by array concatenation. ▶Lemma 29 (Ó).Zero-length arrays (0, 𝑓 )are contractible. Proof. We need to show 𝑓:Fin0→𝐴 is equal to 𝜆{} . By function extensionality this amounts to showing for all 𝑥: 0, 𝑓(𝑥)=(𝜆{})(𝑥) , which holds by absurdity elimination on 𝑥 . Therefore, any array (0, 𝑓 )is equal to (0, 𝜆{}).◀ ▶ Definition 30 ( Ó Concatenation).The concatenation operation ++ , is defined below, where ⊕:(Finn→𝐴)→(Finm→𝐴)→(Finn+m→𝐴)combines the two lookup functions. (𝑛, 𝑓 ) ++ (𝑚, 𝑔)=(𝑛+𝑚, 𝑓 ⊕𝑔) ( 𝑓⊕𝑔)(𝑘)=(𝑓(𝑘)if 𝑘 < 𝑛 𝑔(𝑘−𝑛)otherwise ▶Proposition 31 (Ó).(Array(𝐴),++) is a monoid. Proof. To show Array satisfies left unit, we want to show (0, 𝜆{}) ++ (𝑛, 𝑓 )=(𝑛, 𝑓 ). (0, 𝜆{}) ++ (𝑛, 𝑓 )=(0+𝑛, 𝜆{} ⊕ 𝑓) (𝜆{} ⊕ 𝑓)(𝑘)=((𝜆{})(𝑘)if 𝑘 < 0 𝑓(𝑘−0)otherwise It is trivial to see the length matches: 0 +𝑛=𝑛 . We also need to show 𝜆{} ⊕ 𝑓=𝑓 . Since 𝑛 < 0for any 𝑛:N is impossible, (𝜆{} ⊕ 𝑓)(𝑘) would always reduce to 𝑓(𝑘− 0 )=𝑓(𝑘) , therefore (0, 𝜆{}) ++ (𝑛, 𝑓 )=(𝑛, 𝑓 ). To show Array satisfies right unit, we want to show (𝑛, 𝑓 ) ++ (0, 𝜆{}) =(𝑛, 𝑓 ). (𝑛, 𝑓 ) ++ (0, 𝜆{}) =(𝑛+0, 𝑓 ⊕𝜆{}) (𝑓⊕𝜆{})(𝑘)=(𝑓(𝑘)if 𝑘 < 𝑛 (𝜆{})(𝑘−0)otherwise It is trivial to see the length matches: 𝑛+ 0 =𝑛 . We also need to show 𝑓⊕𝜆{} =𝑓 . We note that the type of 𝑓⊕𝜆{} is Finn+0→𝐴 , therefore 𝑘 is of the type Finn+0 . Since Finn+0Finn , it must always hold that 𝑘 < 𝑛 , therefore (𝑓⊕𝜆{})(𝑘) must always reduce to 𝑓(𝑘) . Thus, (𝑛, 𝑓 ) ++ (0, 𝜆{}) =(𝑛, 𝑓 ). For associativity, we want to show for any array (𝑛, 𝑓 ) , (𝑚, 𝑔) , (𝑜, ℎ) , ((𝑛, 𝑓 ) ++ (𝑚, 𝑔)) ++ (𝑜, ℎ)=(𝑛, 𝑓 ) ++ ((𝑚, 𝑔) ++ (𝑜, ℎ)). 16 Symmetries in Sorting swap , such as reflexivity, transitivity, symmetry, congruence and such all comes directly by construction, whereas with Perm we would have to prove these properties manually. We can also use the many combinatorics defined in the standard library for equational reasoning, making the handling of SList equalities a lot simpler. 4.4 Bag Alternatively, we can also quotient Array by symmetries to get commutativity. This construction is first considered in [ 3 ] and [ 19 ], partially considered in [ 7 ], and in in [ 16 ], who gave a similar construction, where only the index function is quotiented, instead of the entire array. [ 11 ] also considered Bag as a setoid relation on List in an intensional MLTT setting. [ 16 ] prove that their version of Bag is the free commutative monoid by equivalence to the other HIT constructions. We give a direct proof of its universal property instead, using our general recipe. ▶Definition 47 (ÓBag).Bags are defined as arrays quotiented by bag equivalence ≈: (𝑛, 𝑓 )≈(𝑚, 𝑔)≔(𝜎:Finn ∼ −→ Finm)×(𝑓=𝑔◦𝜎) Bag(𝐴)≔Array(𝐴)≈ Note that by a pigeonhole argument, 𝜎 may only be constructed when 𝑛=𝑚 . In other words, we are quotienting by an automorphism on the indices, and its action on the elements. We have already shown Array to be the free monoid in § 3.2. By Proposition 40, it suffices to show that ≈ satisfies the axioms of permutation relations to establish that Bag is the free commutative monoid. ▶Proposition 48 (Ó).≈is a equivalence relation. Proof. We can show any array xs is related to itself by the identity isomorphism, therefore ≈ is reflexive. If xs ≈ys by 𝜎 , we can show ys ≈xs by 𝜎−1 , therefore ≈ is symmetric. If xs ≈ys by 𝜎and ys ≈zs by 𝜙, we can show xs ≈zs by 𝜎◦𝜙, therefore ≈is transitive. ◀ ▶Proposition 49 (Ó).≈is congruent wrt to ++. Proof. Given (𝑛, 𝑓 )≈(𝑚, 𝑔) by 𝜎 and (𝑢, 𝑝)≈(𝑣, 𝑞) by 𝜙 , we want to show (𝑛, 𝑓 ) ++ (𝑢, 𝑝) ≈ (𝑚, 𝑔) ++ (𝑣, 𝑞)by some 𝜏. We construct 𝜏as follows: 𝜏≔Finn+u ∼ −→ Finn+Finu 𝜎, 𝜙 −−−−→ Finm+Finv ∼ −→ Finm+v which operationally performs: {0,1, . . . , 𝑛 −1,𝑛, 𝑛 +1, . . . , 𝑛 +𝑢−1} {𝜎(0), 𝜎(1). . . , 𝜎(𝑛−1),𝜙(0), 𝜙(1), . . . , 𝜙(𝑢−1)} 𝜎,𝜙 . ◀ ▶Proposition 50 (Ó).≈respects commutativity. Proof. We want to show for any arrays (𝑛, 𝑓 ) and (𝑚, 𝑔) , (𝑛, 𝑓 )•(𝑚, 𝑔)≈(𝑚, 𝑔)•(𝑛, 𝑓 ) by some 𝜙. We use formal combinators (see [8]) to define 𝜙: 𝜙≔Finn+m ∼ −→ Finn+Finm swap+ −−−−→ Finm+Finn ∼ −→ Finm+n V. Choudhury and W. Wong 17 which operationally performs: {0,1, . . . , 𝑛 −1,𝑛, 𝑛 +1, . . . , 𝑛 +𝑚−1} {𝑛, 𝑛 +1. . . , 𝑛 +𝑚−1,0,1, . . . , 𝑛 −1} 𝜙. ◀ To show that 𝑓♯ is invariant under permutation: for all 𝜙:Finn ∼ −→ Finn , 𝑓♯(𝑛, 𝑖)=𝑓♯(𝑛, 𝑖 ◦𝜙) , we need some formal combinators for punching in and punching out indices. These operations are borrowed from [21] and developed further in [8] for studying permutation codes. ▶ Lemma 51 ( Ó ).Given 𝜙:FinS(n) ∼ −→ FinS(n) , there is a permutation 𝜏:FinS(n) ∼ −→ FinS(n) such that 𝜏(0)=0, and 𝑓♯(𝑆(𝑛), 𝑖 ◦𝜙)=𝑓♯(𝑆(𝑛), 𝑖 ◦𝜏). Proof. Let 𝑘be 𝜙−1(0), and 𝑘+𝑗=𝑆(𝑛), we construct 𝜏: 𝜏≔FinS(n) 𝜙 −→ FinS(n) ∼ −→ Fink+j ∼ −→ Fink+Finj swap+ −−−−→ Finj+Fink ∼ −→ Finj+k ∼ −→ FinS(n) {0,1,2, . . . , 𝑘, 𝑘 +1, 𝑘 +2, . . .} {𝑥, 𝑦, 𝑧, . . . , 0, 𝑢, 𝑣, . . .} 𝜙 {0,1,2, . . . , 𝑘, 𝑘 +1, 𝑘 +2, . . .} {0, 𝑢, 𝑣, . . . , 𝑥, 𝑦, 𝑧, . . .} 𝜏 It is trivial to show 𝑓♯(𝑆(𝑛), 𝑖 ◦𝜙)=𝑓♯(𝑆(𝑛), 𝑖 ◦𝜏) , since the only operation on indices in 𝜏 is swap+ . It suffices to show (𝑆(𝑛), 𝑖 ◦𝜙) can be decomposed into two arrays such that (𝑆(𝑛), 𝑖 ◦𝜙)=(𝑘, 𝑔) ++ ( 𝑗, ℎ) for some 𝑔 and ℎ . Since the image of 𝑓♯ is a commutative monoid, and 𝑓♯ is a homomorphism, 𝑓♯((𝑘, 𝑔) ++ ( 𝑗, ℎ)) =𝑓♯(𝑘, 𝑔) • 𝑓♯(𝑗, ℎ)=𝑓♯(𝑗, ℎ) • 𝑓♯(𝑘, 𝑔)= 𝑓♯(( 𝑗, ℎ) ++ (𝑘, 𝑔)), thereby proving 𝑓♯(𝑆(𝑛), 𝑖 ◦𝜙)=𝑓♯(𝑆(𝑛), 𝑖 ◦𝜏). ◀ ▶ Lemma 52 ( Ó ).Given 𝜏:FinS(n) ∼ −→ FinS(n) where 𝜏( 0 )= 0, there is a 𝜓:Finn ∼ −→ Finn such that 𝜏◦𝑆=𝑆◦𝜓. Proof. We construct 𝜓 as 𝜓(𝑥)=𝜏(𝑆(𝑥)) − 1. Since 𝜏 maps only 0 to 0 by assumption, ∀𝑥. 𝜏(𝑆(𝑥)) > 0, therefore the (− 1 ) is well defined. This is the special case for 𝑘= 0in the punch-in and punch-out equivalence for Lehmer codes in [8]. {0,1,2,3, . . .} {0,𝑥, 𝑦, 𝑧 . . .} 𝜏 {0,1,2, . . .} {𝑥−1, 𝑦 −1, 𝑧 −1. . .} 𝜓 ◀ ▶Theorem 53 (ÓPermutation invariance).For all 𝜙:Finn ∼ −→ Finn,𝑓♯(𝑛, 𝑖)=𝑓♯(𝑛, 𝑖 ◦𝜙). Proof. By induction on 𝑛. At 𝑛=0,𝑓♯(0, 𝑖)=𝑓♯(0, 𝑖 ◦𝜙)=𝑒. At 𝑛=𝑆(𝑚), 𝑓♯(𝑆(𝑚), 𝑖 ◦𝜙) =𝑓♯(𝑆(𝑚), 𝑖 ◦𝜏)by Lemma 51 =𝑓(𝑖(𝜏(0))) • 𝑓♯(𝑚, 𝑖 ◦𝜏◦𝑆)by definition of (−)♯ =𝑓(𝑖(0)) • 𝑓♯(𝑚, 𝑖 ◦𝜏◦𝑆)by construction of 𝜏 =𝑓(𝑖(0)) • 𝑓♯(𝑚, 𝑖 ◦𝑆◦𝜓)by Lemma 52 =𝑓(𝑖(0)) • 𝑓♯(𝑚, 𝑖 ◦𝑆)induction =𝑓♯(𝑆(𝑚), 𝑖)by definition of (−)♯ 18 Symmetries in Sorting ◀ Unlike PList and SList , Bag and its underlying construction Array are not inductively defined, making it difficult to do induction on them. For example, in the proof of Proposition 36, both Lemmas 32 and 33 are needed to do induction on Array , as opposed to List and its quotients, where we can do induction simply by pattern matching. Much like PList , when defining functions on Bag , we need to show they respect ≈ , i.e. as ≈bs →𝑓(as)=𝑓(bs) . Notably, this is much more difficult than PList or SList – with PList and SList we only need to consider swapping adjacent elements, while with Bag we need to consider all possible permutations. For example, in the proof of Theorem 53, we need to first construct a 𝜏 which satisfies 𝜏(0)=0and prove 𝑓♯(𝑛, 𝑖 ◦𝜎)=𝑓♯(𝑛, 𝑖 ◦𝜏)before we can apply induction. Since Array and Bag are not simple data types, the definition of the monoid operation on them ++ are necessarily more complicated, and unlike List , PList and SList , constructions of Array and Bag via ++ often would not normalize into a very simple form, but would instead expand into giant trees of terms. This makes it such that when working with Array and Bag we need to be very careful or otherwise Agda would be stuck trying to display the normalized form of Array and Bag in the goal and context menu. Type-checking also becomes a lengthy process that tests if the user possesses the virtue of patience. However, performing arbitrary partitioning with Array and Bag is much easier than List , SList , PList . For example, one can simply use the combinator Finn+m ∼ −→ Finn+Finm to partition the array, then perform operations on the partitions such as swapping in Proposition 50, or perform operations on the partitions individually such as two individual permutation in Proposition 49. This makes it such that when defining divide-and-conquer algorithms such as merge sort, Bag and Array are more natural to work with than List , SList , and PList. 5 Sorting Functions We will now put to work the universal properties of our types of (ordered) lists and unordered lists, to define operations on them systematically, which are mathematically sound, and reason about them. First, we explore definitions of various operations on both free monoids and free commutative monoids. By univalence (and the structure identity principle), everything henceforth holds for any presentation of free monoids and free commutative monoids. We use F (𝐴) to denote the free monoid or free commutative monoid on 𝐴 , L(𝐴) to exclusively denote the free monoid construction, and M(𝐴) to exclusively denote the free commutative monoid construction. For example length is a common operation defined inductively for List , but usually, properties about length , such as, length(xs++ys)=length(xs)+length(ys) , are proven separately after defining it. In our framework of free algebras, where the (−)♯ operation is a correctby-construction homomorphism, we can define operations like length directly by universal extension, which also gives us a proof that they are homomorphisms for free. A further application of the universal property is to prove that two different types are equal, by showing they both satisfy the same universal property as in Proposition 11, which is desirable especially when proving a direct equivalence between the two types turns out to be a difficult exercise in combinatorics. V. Choudhury and W. Wong 19 5.1 Prelude Any presentation of free monoids or free commutative monoids has a length:F (𝐴) → N function, where N carries the additive monoid structure ( 0 ,+) , which is also a commutative monoid structure since addition is commutative. ▶Definition 54 (Ólength).The length homomorphism is defined as (𝜆𝑥. 1)♯:F (𝐴) → N. Further, any presentation of free monoids or free commutative monoids has an element membership predicate −∈−:𝐴→ F (𝐴) → hProp, for any set 𝐴. Here, we use the fact that hProp forms a (commutative) monoid under disjunction and falsehood (⊥,∨). ▶ Definition 55 ( Ó Membership ∈ ).The membership predicate on a set 𝐴 for any element 𝑥:𝐴is 𝑥∈−≔よ𝐴(𝑥)♯:F (𝐴) → hProp, where we define よ𝐴(𝑥)≔𝜆𝑦. 𝑥 =𝑦:𝐴→hProp. よ is formally the Yoneda map under the “types are groupoids” correspondence, where 𝑥:𝐴 is being sent to its representable in the Hom-groupoid (formed by the identity type), of type hProp . Note that the proofs of (commutative) monoid laws for hProp use equality, which requires the use of univalence (or at least, propositional extensionality). By construction, this membership predicate satisfies its homomorphic properties, which are colloquially the properties of inductively defined de Bruijn indices. We note that hProp is actually one type level higher than 𝐴 . To make the type level explicit, 𝐴 is of type level ℓ , and since hPropℓ is the type of all types 𝑋:Setℓ that are mere propositions, hPropℓ has type level ℓ+ 1. We do not assume any propositional resizing axioms [24], and use level polymorphism (−)♯in our formalisation to accommodate this. Any presentation of free (commutative) monoids F (𝐴) also supports the Any and All predicates, which allow lifting a predicate 𝐴→hProp (on 𝐴 ), to any or all elements of xs:F (𝐴) , respectively. We note that hProp forms a (commutative) monoid in two different ways: (⊥,∨) and (⊤,∧) (disjunction and conjunction), which are the two different ways of getting Any and All, respectively, by extension. ▶Definition 56 (Any and All). Any(𝑃)≔𝑃♯:F (𝐴)→(hProp,⊥,∨) All(𝑃)≔𝑃♯:F (𝐴)→(hProp,⊤,∧) Note that Cubical Agda has problems with indexing over HITs [ 22 , 2 , § 8] hence it is preferable to program with our universal properties, such as when defining Any and All , because the indexed-inductive definitions of these predicates get stuck on transp terms. There is a head function on lists, which is a function that returns the first element of a non-empty list. Formally, this is a monoid homomorphism from L(𝐴)to 1+𝐴. ▶ Definition 57 ( Óhead ).The head homomorphism is defined as head ≔inr♯:L(𝐴) → 1 +𝐴 , where the monoid structure on 1 +𝐴 has unit 𝑒≔inl(★): 1 +𝐴 , and multiplication picks the leftmost element that is defined. inl(★) ⊕ 𝑏≔𝑏 inr(𝑎) ⊕ 𝑏≔inr(𝑎) This monoid operation ⊕ is not commutative, since swapping the input arguments to ⊕ would return the leftmost or rightmost element. To make it commutative would require a canonical way to pick between a choice of two elements – this leads us to the next section. 20 Symmetries in Sorting 5.2 Total orders First, we recall the axioms of a total order or linear order ≤on a set 𝐴. ▶ Definition 58 ( Ó Total order).A total order on a set 𝐴 is a relation ≤:𝐴→𝐴→hProp that satisfies: reflexivity: 𝑥≤𝑥, transitivity: if 𝑥≤𝑦and 𝑦≤𝑧, then 𝑥≤𝑧, antisymmetry: if 𝑥≤𝑦and 𝑦≤𝑥, then 𝑥=𝑦, totality: ∀𝑥, 𝑦, either 𝑥≤𝑦or 𝑦≤𝑥. Adecidable total order requires the ≤relation to be decidable: decidable totality: ∀𝑥, 𝑦, we have 𝑥≤𝑦+ ¬(𝑥≤𝑦). Note that either-or means a (truncated) logical disjunction. In the context of this paper, we want to make a distinction between “decidable total order” and “total order”. The decidability axiom strengthens the totality axiom, where we have either 𝑥≤𝑦 or 𝑦≤𝑥 merely as a proposition, but decidability allows us to produce a witness if 𝑥≤𝑦is true. ▶ Proposition 59 ( Ó ).In a decidable total order, it holds that ∀𝑥, 𝑦, (𝑥≤𝑦)+(𝑦≤𝑥) . Further, this makes 𝐴discrete, that is ∀𝑥, 𝑦, (𝑥=𝑦)+(𝑥≠𝑦). Proof. We decide if 𝑥≤𝑦and 𝑦≤𝑥, and by cases: if 𝑥≤𝑦and 𝑦≤𝑥: by antisymmetry, 𝑥=𝑦. if ¬(𝑥≤𝑦)and 𝑦≤𝑥: assuming 𝑥=𝑦leads to a contradiction, hence 𝑥≠𝑦. if 𝑥≤𝑦and ¬(𝑦≤𝑥): similar to the previous case. if ¬(𝑥≤𝑦) and ¬(𝑦≤𝑥) : by totality, either 𝑥≤𝑦 or 𝑦≤𝑥 , which leads to a contradiction. ◀ We also recall the axioms of a strict total order <on 𝐴. ▶ Definition 60 ( Ó Strict total order).A strict total order on a set 𝐴 is a relation <:𝐴→ 𝐴→hProp that satisfies: irreflexivity: ¬(𝑥 < 𝑥), transitivity: if 𝑥 < 𝑦 and 𝑦 < 𝑧, then 𝑥 < 𝑧, asymmetry: if 𝑥 < 𝑦, then ¬(𝑦 < 𝑥), cotransitivity: ∀𝑥, 𝑦, 𝑧, if 𝑥 < 𝑧, then either 𝑥 < 𝑦 or 𝑦 < 𝑧. connectedness: ∀𝑥, 𝑦, if ¬(𝑥 < 𝑦)and ¬(𝑦 < 𝑥), then 𝑥=𝑦. Adecidable strict total order requires the <relation to be decidable: decidability: ∀𝑥, 𝑦, we have 𝑥 < 𝑦 + ¬(𝑥 < 𝑦). ▶ Proposition 61 ( Ó ).In a decidable strict total order, it holds that ∀𝑥, 𝑦, (𝑥 < 𝑦)+(𝑦 < 𝑥) . Further, this makes 𝐴discrete, that is ∀𝑥, 𝑦, (𝑥=𝑦)+(𝑥≠𝑦). Proof. We decide if 𝑥 < 𝑦 and 𝑦 < 𝑥, and by cases: if ¬(𝑥 < 𝑦)and ¬(𝑦 < 𝑥): by connectedness, 𝑥=𝑦. if 𝑥 < 𝑦 or 𝑦 < 𝑥: by irreflexivity, 𝑥≠𝑦. ◀ V. Choudhury and W. Wong 21 ▶ Proposition 62 ( Ó ).The set of decidable strict total orders on 𝐴 and the set of decidable total orders on 𝐴are equivalent. Proof sketch. Given a decidable total order ≤ on 𝐴 , by Proposition 59, we map it to a decidable strict total order < on 𝐴 by 𝑥 < 𝑦 ≔(𝑥≤𝑦)×(𝑥≠𝑦) . Vice versa, by Proposition 61 given a decidable strict total order < on 𝐴 , we map it to a decidable total order ≤ on 𝐴 by 𝑥≤𝑦≔(𝑥 < 𝑦)+(𝑥=𝑦). These maps are inverses of each other. ◀ An equivalent way of defining a total order is using a binary meet operation, without starting from an ordering relation. ▶ Definition 63 ( Ó Meet semi-lattice).A meet semi-lattice is a set 𝐴 with a binary operation −⊓−:𝐴→𝐴→𝐴that is: idempotent: 𝑥⊓𝑥=𝑥, associative: (𝑥⊓𝑦) ⊓ 𝑧=𝑥⊓ (𝑦⊓𝑧), commutative: 𝑥⊓𝑦=𝑦⊓𝑥. Astrongly-connected meet semi-lattice further satisfies: strong-connectedness: ∀𝑥, 𝑦, either 𝑥⊓𝑦=𝑥or 𝑥⊓𝑦=𝑦. Adecidable strongly-connected meet semi-lattice strengthens this to: decidable strong-connectedness: ∀𝑥, 𝑦, (𝑥⊓𝑦=𝑥)+(𝑥⊓𝑦=𝑦). ▶ Proposition 64 ( Ó ).A total order ≤ on a set 𝐴 is equivalent to a strongly-connected meet semi-lattice structure on 𝐴 . Further, a decidable total order on 𝐴 induces a decidable strongly-connected meet semi-lattice structure on 𝐴. Proof sketch. Given a (mere) total order ≤ on a set 𝐴 , we define 𝑥⊓𝑦≔if 𝑥≤𝑦then 𝑥else 𝑦 . Crucially, this map is locally-constant, allowing us to eliminate from an hProp to an hSet . Meets satisfy the universal property of products, that is, 𝑐≤𝑎⊓𝑏⇔𝑐≤𝑎∧𝑐≤𝑏 , and the axioms follow by calculation using よ -arguments. Conversely, given a meet semi-lattice, we define 𝑥≤𝑦≔𝑥⊓𝑦=𝑥 , which defines an hProp -valued total ordering relation. If the total order is decidable, we use the discreteness of 𝐴 from Proposition 59 to constructively define the meet operation. The converse does not hold however, as a decidable strongly-connected meet semi-lattice does not imply discreteness of 𝐴. Thus, we do not have a full equivalence in the decidable case. ◀ Finally, tying this back to Definition 57, we have the following for free commutative monoids. ▶ Definition 65 ( Óhead ).Assume a total order ≤ on a set 𝐴 . We define a commutative monoid structure on 1+𝐴, with unit 𝑒≔inl(★): 1 +𝐴, and multiplication defined as: inl(★) ⊕ 𝑏≔𝑏 inr(𝑎) ⊕ inl(★)≔inr(𝑎) inr(𝑎) ⊕ inr(𝑏)≔inr(𝑎⊓𝑏). This gives a homomorphism head ≔inr♯:M(𝐴) → 1+𝐴 , which picks out the least element of the free commutative monoid. 22 Symmetries in Sorting L(𝐴) M(𝐴) 𝔰 𝔮 Figure 1 Relationship of L(𝐴)and M(𝐴) 5.3 Sorting functions The free commutative monoid is also a monoid, hence, there is a canonical monoid homomorphism 𝔮:L(𝐴) → M(𝐴) , which is given by 𝜂𝐴♯ , the extension of the unit 𝜂𝐴:𝐴→ M(𝐴) . Since M(𝐴) is (upto equivalence), a quotient of L(𝐴) by symmetries (or a permutation relation), it is a surjection (in particular, a regular epimorphism in Set as constructed in type theory). Concretely, 𝔮 simply includes the elements of L(𝐴) into equivalence classes of lists in M(𝐴) , which “forgets” the order that was imposed by the indexing of the list. Classically, assuming the Axiom of Choice would allow us to construct a section (rightinverse, in Set ) to the surjection 𝔮 , that is, a function 𝔰:M(𝐴) → L(𝐴) such that ∀𝑥. 𝔮(𝔰(𝑥)) = 𝑥 . Or in informal terms, given the surjective inclusion into the quotient, a section (uniformly) picks out a canonical representative for each equivalence class. The core question we want to study is the existence of 𝔰 in a constructive setting, or equivalently, whether the order factored out by the symmetry quotient can be constructively recovered. Viewing the quotienting relation as a permutation relation (from § 4.1), a section 𝔰 to 𝔮 has to pick out canonical representatives of equivalence classes generated by permutations. Using SList as an example, 𝔰(𝑥:: 𝑦:: xs)= 𝔰(𝑦:: 𝑥:: xs) for any 𝑥, 𝑦 :𝐴 and xs:SList(𝐴) , by swap . Since ∀xs.𝔮(𝔰(xs)) =xs , 𝔰 must preserve all the elements of xs . It cannot be a trivial function such as 𝜆xs.[] – it must produce a permutation of the elements of 𝔰 . But to place these elements side-by-side in the list, 𝔰 must somehow impose an order on 𝐴 (invariant under permutation), turning unordered lists of 𝐴 into ordered lists of 𝐴 . Axiom of Choice (AC) giving us a section 𝔰 to 𝔮 “for free” is analagous to how AC implies the well-ordering principle, which states every set can be well-ordered. Thus, if AC was assumed, we could easily recover an order on 𝐴 from the section 𝔰 . Instead we study how to constructively define such a section, and in fact, that is exactly the extensional view of a sorting algorithm, and the implications of its existence is that 𝐴can be ordered, or sorted. 5.3.1 Section from Order ▶ Proposition 66 ( Ó ).Assume a decidable total order on 𝐴 . There is a sort function 𝔰:M(𝐴) → L(𝐴)which constructs a section to 𝔮:L(𝐴)↠M(𝐴) Proof sketch. We may construct such a sort function by implementing any sorting algorithm. In our formalisiation we chose insertion sort, because it can be defined easily using the inductive structure of SList(𝐴) and List(𝐴) . To implement other sorting algorithms like mergesort, other representations such as Bag and Array would be preferable, as explained in§4.4. To see how this proposition holds: 𝔮(𝔰(xs)) first orders an unordered list xs by 𝔰 , then discards the order again by 𝔮 – imposing and then forgetting an order on xs simply permutes its elements, which proves 𝔮◦𝔰 = id.◀ 5.3.2 Order from Section The previous section allowed us to construct a section, but an arbitrary section may not be a sorting function. To show a section is indeed a sort function, we need to show the section V. Choudhury and W. Wong 23 imposes some total order on 𝐴 which it sorts by. Indeed, just by the virtue of 𝔰 being a section, we can almost construct a total-order on the carrier set. ▶Definition 67 (Óleast).Given a section 𝔰, we define: 𝑥≼𝔰𝑦≔head(𝔰(*𝑥, 𝑦+)) =inr(𝑥). That is, we take the two-element bag *𝑥, 𝑦+ , “sort” it by 𝔰 , and test if the head element is 𝑥 . Note, this is equivalent to 𝑥≼𝔰𝑦≔𝑠*𝑥, 𝑦+=[𝑥, 𝑦] , because 𝔰 preserves length, and the second element is forced to be 𝑦. ▶Proposition 68 (Ó).≼𝔰is reflexive, antisymmetric, and total. Proof. For all 𝑥 , least(*𝑥, 𝑥+) must be inr(𝑥) , therefore 𝑥≼𝔰𝑥 , giving reflexivity. For all 𝑥 and 𝑦 , given 𝑥≼𝔰𝑦 and 𝑦≼𝔰𝑥 , we have least(*𝑥, 𝑦+)=inr(𝑥) and least(*𝑦, 𝑥+)=inr(𝑦) . Since *𝑥, 𝑦+=*𝑦, 𝑥+ , least(*𝑥, 𝑦+)=least(*𝑦, 𝑥+) , therefore we have 𝑥=𝑦 , giving antisymmetry. For all 𝑥 and 𝑦 , least(*𝑥, 𝑦+) is merely either inr(𝑥) or inr(𝑦) , therefore we have merely either 𝑥≼𝔰𝑦or 𝑦≼𝔰𝑥, giving totality. ◀ A crucial observation is that 𝔰 correctly orders 2-element bags, but it does not necessarily sort bags with 3 or more elements. ▶Proposition 69. ≼𝔰is not necessarily transitive. Proof. We give a counterexample of an 𝔰 that violates transitivity. Consider the section 𝑠:SList(N) → List(N) defined as follows. First, we define a sort function sort:SList(N) → List(N)which sorts SList(N)ascendingly. Then we use sort to construct 𝔰. 𝔰(xs)=(sort(xs)if length(xs)is odd reverse(sort(xs)) otherwise Now we have 𝔰([2,3,1]) =[1,2,3]but 𝔰([2,3,1,4]) =[4,3,2,1].◀ We will enforce additional constraints on the image of 𝔰 , to turn it into a correct sort function. ▶ Definition 70 ( Ó−∈im(𝔰) ).The fiber of 𝔰 at a point in the codomain xs:L(𝐴) is given by fib𝔰(xs)≔(𝑦𝑠 :M(𝐴)) × (𝔰(𝑦𝑠)=xs) . The image of 𝔰 is given by im(𝔰)≔(xs :L(𝐴)) × ∥fib𝔰(xs)∥−1 . Simplifying, we say that xs:L(𝐴) is “in the image of 𝔰 ”, or, xs ∈im(𝔰) , if there merely exists a ys :M(𝐴)such that 𝔰(ys)=xs. If 𝔰 were a sort function, the image of 𝔰 would be the set of 𝔰 -“sorted” lists, therefore xs ∈im(𝔰) would imply xs is a correctly 𝔰 -“sorted” list. First, we note that the 2-element case is correct. ▶Proposition 71 (Ó).𝑥≼𝔰𝑦iff [𝑥, 𝑦] ∈ im(𝔰). Then, we state the first axiom on 𝔰. ▶Definition 72 (ÓisHeadLeast).A section 𝔰satisfies isHeadLeast iff for all 𝑥, 𝑦, xs: 𝑦∈𝑥:: xs ∧𝑥:: xs ∈im(𝔰) → [𝑥, 𝑦] ∈ im(𝔰). We use the definition of list membership from Definition 55. The ∈ symbol is intentionally overloaded to make the axiom look like a logical “cut” rule. Informally, it says that the head of an 𝔰-“sorted” list is the least element of the list. 24 Symmetries in Sorting ▶ Proposition 73 ( Ó ).If 𝐴 has a total order ≤ , insertion sort defined using ≤ satisfies isHeadLeast. ▶Proposition 74 (Ó).If 𝔰satisfies isHeadLeast,≼𝔰is transitive. Proof. Given 𝑥≼𝔰𝑦 and 𝑦≼𝔰𝑧 , we want to show 𝑥≼𝔰𝑧 . Consider the 3-element bag *𝑥, 𝑦, 𝑧+:M(𝐴) . Let 𝑢 be least(*𝑥, 𝑦, 𝑧+) , by Definition 72 and Proposition 71, we have 𝑢≼𝔰 𝑥∧𝑢≼𝔰𝑦∧𝑢≼𝔰𝑧 . Since 𝑢∈*𝑥, 𝑦, 𝑧+ , 𝑢 must be one of the elements. If 𝑢=𝑥 we have 𝑥≼𝔰𝑧 . If 𝑢=𝑦 we have 𝑦≼𝔰𝑥 , and since 𝑥≼𝔰𝑦 and 𝑦≼𝔰𝑧 by assumption, we have 𝑥=𝑦 by antisymmetry, and then we have 𝑥≼𝔰𝑧 by substitution. Finally, if 𝑢=𝑧 , we have 𝑧≼𝔰𝑦 , and since 𝑦≼𝔰𝑧 and 𝑥≼𝔰𝑦 by assumption, we have 𝑧=𝑦 by antisymmetry, and then we have 𝑥≼𝔰𝑧by substitution. ◀ 5.3.3 Embedding orders into sections Following from Propositions 68 and 74, and Proposition 73, we have shown that a section 𝔰 that satisfies isHeadLeast produces a total order 𝑥≼𝔰𝑦≔least(*𝑥, 𝑦+)=inr(𝑥) , and a total order ≤ on the carrier set produces a section satisfying isHeadLeast , constructed by sorting with ≤ . This constitutes an embedding of decidable total orders into sections satisfying isHeadLeast. ▶ Proposition 75 ( Ó ).Assume 𝐴 has a decidable total order ≤ , we can construct a section 𝔰that satisfies isHeadLeast, such that ≼𝔰constructed from 𝔰is equivalent to ≤. Proof. By the insertion sort algorithm parameterized by ≤ , it holds that [𝑥, 𝑦] ∈ im(𝔰) iff 𝑥≤𝑦 . By Proposition 71, we have 𝑥≼𝔰𝑦 iff 𝑥≤𝑦 . We now have a total order 𝑥≼𝔰𝑦 equivalent to 𝑥≤𝑦.◀ 5.3.4 Equivalence of order and sections We want to upgrade the embedding to an isomorphism, and it remains to show that we can turn a section satisfying isHeadLeast to a total order ≼𝔰 , then construct the same section back from ≼𝔰. Unfortunately, isHeadLeast is not enough to guarantee this. ▶ Proposition 76. Assume 𝐴 is a set with different elements, i.e. ∃𝑥, 𝑦 :𝐴. 𝑥 ≠𝑦 , we cannot construct a full equivalence between sections that satisfy isHeadLeast and total orders on 𝐴. Proof. We give a counter-example of 𝔰 that satisfy isHeadLeast but is not a sort function. Consider the insertion sort function sort:M(N) → L(N)parameterized by ≤: reverseTail([]) =[] reverseTail(𝑥:: xs)=𝑥:: reverse(xs) 𝔰(xs)=reverseTail(sort(xs)) 𝔰(*2,3,1,4+)=[1,4,3,2] 𝔰(*2,3,1+)=[1,3,2] 𝔰(*2,3+)=[2,3] By Proposition 75 we can use sort to construct ≼𝔰 which would be equivalent to ≤ . However, the ≼𝔰 constructed by 𝔰 would also be equivalent to ≤ . This is because 𝔰 sorts 2-element list correctly, despite 𝑠≠sort . Since two different sections satisfying isHeadLeast maps to the same total order, there cannot be a full equivalence. ◀ V. Choudhury and W. Wong 25 Therefore, we need to introduce a second axiom of sorting. ▶Definition 77 (ÓisTailSorted).A section 𝔰satisfies isTailSorted iff for all 𝑥, xs, 𝑥:: xs ∈im(𝔰) → xs ∈im(𝔰) This says that 𝔰 -“sorted” lists are downwards-closed under cons-ing, that is, the tail of an 𝔰 -“sorted” list is also 𝔰 -“sorted”. To prove the correctness of our axioms, first we need to show that a section 𝔰 satisfying isHeadLeast and isTailSorted is equal to insertion sort parameterized by the ≼𝔰 constructed from 𝔰 . In fact, the axioms we have introduced are equivalent to the standard inductive characterization of sorted lists, found in textbooks, such as in [4]. ▶ Definition 78 ( ÓisSorted ).Given a total order ≤ on 𝐴 , the predicate isSorted≤ on L(𝐴) is generated by the following constructors: sorted-nil:isSorted≤([]) sorted −𝜂:∀𝑥. isSorted≤([𝑥]) sorted-cons:∀𝑥, 𝑦, zs. 𝑥 ≤𝑦→isSorted≤(𝑦:: zs) → isSorted≤(𝑥:: 𝑦:: zs) Note that isSorted≤(xs) is a proposition for every xs , and forces the list xs to be permuted in a unique way. ▶ Lemma 79 ( Ó ).Given a total order ≤ , for any xs,ys :L(𝐴) , 𝔮(xs)= 𝔮(ys)∧isSorted≤(xs)∧ isSorted≤(ys) → xs =ys. Insertion sort by ≤ always produces lists that satisfy isSorted≤ . Functions that also produce lists satisfying isSorted≤are equal to insertion sort by function extensionality. ▶ Proposition 80 ( Ó ).Given a total order ≤ , if a section 𝔰 always a produces sorted list, i.e. ∀xs.isSorted≤(𝔰(xs)),𝔰is equal to insertion sort by ≤. Finally, this gives us the correctness property of our axioms. ▶ Proposition 81 ( Ó ).Given a section 𝔰 that satisfies isHeadLeast and isTailSorted , and ≼𝔰 the order derived from 𝔰 , then for all xs:M(𝐴) , it holds that isSorted≼𝔰(𝔰(xs)) . Equivalently, for all lists xs :L(𝐴), it holds that xs ∈im(𝑠)iff isSorted≼𝔰(xs). Proof. We inspect the length of xs:M(𝐴) . For lengths 0 and 1, this holds trivially. Otherwise, we proceed by induction: given a xs:M(𝐴) of length ≥ 2, let 𝔰(xs)=𝑥:: 𝑦:: ys . We need to show 𝑥≼𝔰𝑦∧isSorted≼𝔰(𝑦:: ys) to construct isSorted≼𝔰(𝑥:: 𝑦:: ys) . By isHeadLeast , we have 𝑥≼𝔰𝑦, and by isTailSorted, we inductively prove isSorted≼𝔰(𝑦:: ys).◀ ▶ Lemma 82 ( Ó ).Given a decidable total order ≤ on 𝐴 , we can construct a section 𝑡≤ satisfying isHeadLeast and isTailSorted , such that, for the order ≼𝔰 derived from 𝔰 , we have 𝑡≼𝔰= 𝔰. Proof. From 𝔰 we can construct a decidable total order ≼𝔰 since 𝔰 satisfies isHeadLeast and 𝐴 has decidable equality by assumption. We construct 𝑡≼𝔰 as insertion sort parameterized by ≼𝔰constructed from 𝔰. By Proposition 80 and Proposition 81,𝑠=𝑡≼𝔰.◀ We can now state and prove our main theorem. ▶ Definition 83 ( Ó Sorting function).A sorting function is a section 𝔰:M(𝐴) → L(𝐴) to the canonical surjection 𝔮:L(𝐴)↠M(𝐴)satisfying two axioms: