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 axiomatisation 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 [10] 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 [ 13 , Ch.14]. Suppose there are balls of three colours, corresponding to the colours 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 colours 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 tricolour 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 𝐴 . A sorting function can be correctly axiomatised from this point of view, which is our main contribution. Outline and Contributions The paper is organised as follows: 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 equational systems over signatures. These are elementary constructions but necessary groundwork for us, and we give an informal exposition in type theory. In § 3, we give constructions of free monoids, and proofs of their universal property. Following this, in § 4, we add commutativity to each representation of free monoids, and extend the proofs of universal property from free monoids to free commutative monoids. These constructions are standard, and we formalise by using our general framework. In § 5, we build on the previous constructions and study sorting functions. The main result connects total orders, sorting, and commutativity, by proving an equivalence between decidable total orders on a carrier set 𝐴 , and correct sorting functions defined using free monoids and free commutative monoids over 𝐴. Finally, § 6discusses aspects of the formalisation, related and future work. The three main parts of the paper may be read independently. Readers interested in the formalisation of universal algebra and free algebras may start from § 2. Readers interested in concrete constructions of free monoids and free commutative monoids may skip ahead to §§ 3 and 4. If the reader is already familiar with these constructions, they may directly skip to the technical section on sorting functions, in § 5. The paper is accompanied by a formalisation of all the results in Cubical Agda, and the artefact is available online at [ 10 ]. However, we use informal mathematical language in the paper to keep the presentation accessible. 2 Universal Algebra We develop some basic notions from universal algebra and equational logic [ 6 ], 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 [ 29 ], that predates the Lawvere theory or abstract clone point of view [ 21 , 17 ]. 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}) . Informally, we denote this two-element list of operations as a tuple (𝑒, •). 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 [25]. 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. ▶ 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 produces a monad on Set. Proof. We have unit 𝜂 and extension (−)♯ from the free algebra construction. 𝐹 becomes an endofunctor on Set where the action on functions is given by 𝑓:𝑋→𝑌↦→ (𝜂𝑌◦𝑓)♯:𝐹(𝑋) → 𝐹(𝑌) . The monad unit is given by 𝜂 , and multiplication given by 𝜇𝑋≔id𝐹(𝑋)♯:𝐹(𝐹(𝑋)) → 𝐹(𝑋). The monad laws follow from the identities of universal extension. ◀ ▶Proposition 13 (Ó).The following properties of free algebras on 0,1, and +hold: if 𝜎has one constant symbol, then 𝔉(0)is contractible, the type of algebra structures on 1is contractible, V. Choudhury and W. Wong 5 𝔉(𝑋+𝑌)is the coproduct of 𝔉(𝑋)and 𝔉(𝑌)in 𝜎-Alg, that is: 𝜎-Alg(𝔉(𝑋+𝑌),ℨ) ≃ 𝜎-Alg(𝔉(𝑋),ℨ) × 𝜎-Alg(𝔉(𝑌),ℨ). Proof. 𝐹 being a left adjoint, preserves coproducts. This makes 𝔉( 0 ) initial in 𝜎-Alg . Note that 𝔉( 0 ) is inhabited by all the constant symbols in the signature, so if there is one constant symbol, it becomes contractible. 𝔉(1) → 1is contractible because 1is terminal in Set.◀ 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. Trees for 𝜎Mon look like: 𝑥 𝑦 𝑧 • • 𝑥• (𝑦•𝑧) 𝑒 ▶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, 0 ,+) should be identified as equal. 2 1 1 + + 2+ (1+1) 2 1 1 + + (2+1) + 1 To impose equations on the generated abstract syntax trees, we adopt the point of view of equational logic. 6 Symmetries in Sorting ▶ 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. ▶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. V. Choudhury and W. Wong 7 ▶ 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 [ 7 , § 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. 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 [11,23] and algebraically-free monoids [19] 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(𝐴) → 𝔛. 8 Symmetries in Sorting Proof. To show that 𝑓♯ is a monoid homomorphism, we need to show 𝑓♯(xs ++ ys)=𝑓♯(xs) • 𝑓♯(ys). We do so by induction on xs. Case nil: 𝑓♯(nil ++ys)=𝑓♯(ys)by definition of concatenation =𝑒•𝑓♯(ys)by unit law =𝑓♯(nil) • 𝑓♯(ys)by definition of (−)♯ 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 (−)♯ =𝑓(nil)by homomorphism properties of 𝑓 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. ◀ V. Choudhury and W. Wong 9 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 [ 14 ]. 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. ▶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 𝑛 < 0 for 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, 𝜆{}) =(𝑛, 𝑓 ). 16 Symmetries in Sorting ▶Theorem 46 (Commutativity).For all xs,ys :SList(𝐴),xs ++ ys =ys ++ xs. Proof. By induction on xs we can iteratively apply Lemma 45 to move all elements of xs to after ys . This moves ys to the head and xs to the end, thereby proving xs ++ ys =ys ++ xs . ◀ We refer the reader to [ 8 ] or the Cubical Agda library [ 27 ] for further details. Much like List , SList is inductively defined, therefore making it intuitive to reason with when defining inductive operations or proofs on SList , but difficult to reason with when defining operations that involve arbitrary partitioning, for reasons similar to those given in § 4.2. Unlike PList which is defined as a set quotient, SList is defined as a HIT, therefore handling equalities between SList is much simpler than PList . We would still need to prove a function 𝑓 respects the path constructor of SList when pattern matching, i.e. 𝑓(𝑥:: 𝑦:: xs)=𝑓(𝑦:: 𝑥:: xs) . Unlike PList we do not need to worry about as many auxiliary variables since swap only happens at the head of the list, whereas with PList we would need to prove 𝑓(xs ++ 𝑥:: 𝑦:: ys)= 𝑓(xs ++ 𝑦:: 𝑥:: ys) . One may be tempted to just remove xs from the perm-swap constructor such that it becomes perm-swap:Perm (𝑥:: 𝑦:: ys)zs →Perm (𝑦:: 𝑥:: ys)zs . However this would break Perm ’s congruence w.r.t. ++ , therefore violating the axioms of permutation relations. Also, since we are working with the identity type directly, properties we would expect from 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 [ 4 ] and [ 22 ], partially considered in [ 8 ], and in in [ 18 ], who gave a similar construction, where only the index function is quotiented, instead of the entire array. [ 12 ] also considered Bag as a setoid relation on List in an intensional MLTT setting. [ 18 ] 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 w.r.t. ++. V. Choudhury and W. Wong 17 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 [9]) to define 𝜙: 𝜙≔Finn+m ∼ −→ Finn+Finm swap+ −−−−−→ Finm+Finn ∼ −→ Finm+n 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 [24] and developed further in [9] 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 𝜏◦𝑆=𝑆◦𝜓. 18 Symmetries in Sorting 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 [9]. {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 (−)♯ ◀ 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 permutations in Proposition 49. This makes it so that when defining divide-and-conquer algorithms like merge sort, Bag and Array are more natural representations to work with than List,SList, or PList. V. Choudhury and W. Wong 19 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 then 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 [ 2 ]), 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. 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 levels 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 [ 28 ], and instead use Agda’s universe 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. 20 Symmetries in Sorting ▶Definition 56 (Any and All). Any(𝑃)≔𝑃♯:F (𝐴)→(hProp,⊥,∨) All(𝑃)≔𝑃♯:F (𝐴)→(hProp,⊤,∧) Note that Cubical Agda has problems with indexing over HITs [ 26 , 3 , § 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. 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 then 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 𝐴. V. Choudhury and W. Wong 21 ▶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, 𝑥≠𝑦. ◀ We can show that giving a decidable strict total order structure on 𝐴 is equivalent to giving a decidable total order structure on 𝐴. ▶ 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 checked to be 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: 𝑥⊓𝑦=𝑦⊓𝑥. Atotal meet semi-lattice further satisfies: total: ∀𝑥, 𝑦, either 𝑥⊓𝑦=𝑥or 𝑥⊓𝑦=𝑦. Adecidable total meet semi-lattice strengthens this to: decidable totality: ∀𝑥, 𝑦, (𝑥⊓𝑦=𝑥)+(𝑥⊓𝑦=𝑦). ▶ Proposition 64 ( Ó ).If 𝐴 has decidable equality, all total meet semi-lattice structures on 𝐴are decidable. Proof. We decide if 𝑥⊓𝑦=𝑥 and 𝑥⊓𝑦=𝑦 to compute whether 𝑥⊓𝑦=𝑥 or 𝑥⊓𝑦=𝑦 . By totality, one of them must hold. ◀ 22 Symmetries in Sorting L(𝐴) M(𝐴) 𝔰 𝔮 Figure 1 Relationship of L(𝐴)and M(𝐴) ▶ Proposition 65 ( Ó ).A total order structure on a set 𝐴 is equivalent to a total meet semi-lattice structure on 𝐴 . Further, a decidable total order on 𝐴 induces a decidable total 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, by Proposition 59 and Proposition 64, the mapped meet operation is decidable. The converse does not hold however, as a decidable total meet semi-lattice structure does not imply discreteness of 𝐴.◀ Finally, tying this back to Definition 57, we have the following for free commutative monoids. ▶ Definition 66 ( Ó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. 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), the canonical inclusion into the quotient. 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 V. Choudhury and W. Wong 23 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 67 ( Ó ).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 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 68 (Óleast).Given a section 𝔰, we define a relation ≼𝔰parametrised by 𝔰: 𝑥≼𝔰𝑦≔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 69 (Ó).≼𝔰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 70 (Ó).≼𝔰is not necessarily transitive. Proof. A sorting section 𝔰 would indeed give a ≼𝔰 that satisfies transitivity. However, we can turn a sorting section into a non-sorting misbehaving section that gives a non-transitive 24 Symmetries in Sorting ≼𝔰 . Take the sorting section sort:SList(N) → List(N) which sorts SList(N) ascendingly, we can use sort to construct a counterexample 𝔰as follows: 𝔰(xs)≔([3,1]if 𝑥𝑠 =*1,3+ sort(xs)otherwise Indeed, we have 1 ≼𝔰 2and 2 ≼𝔰 3as expected, but least(*1,3+)=inr( 3 ) , therefore 1 ≼𝔰 3, thus violating transitivity. ◀ To make sure that 𝔰 is a well-behaved section that recovers a total order on 𝐴 , we will enforce additional constraints on the image of 𝔰. ▶ Definition 71 ( Ó−∈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 72 (Ó).𝑥≼𝔰𝑦iff [𝑥, 𝑦] ∈ im(𝔰). Then, we state the first axiom on 𝔰. ▶Definition 73 (ÓisHeadLeast).A section 𝔰satisfies isHeadLeast iff for all 𝑥, 𝑦, xs: 𝑦∈𝑥:: xs ∧𝑥:: xs ∈im(𝔰) → [𝑥, 𝑦] ∈ im(𝔰). There are two different membership symbols in this axiom, where the first membership is list membership from Definition 55, and the second membership is image membership from Definition 71. The ∈symbol is intentionally overloaded to make the axiom look like a logical “cut” rule, that pushes the (least) 𝑥 element to the head of the list. Informally, the head of an 𝔰-“sorted” list is always the least element of the list. ▶ Proposition 74 ( Ó ).If 𝐴 has a total order ≤ , the insertion sort function defined using ≤ satisfies isHeadLeast. ▶Proposition 75 (Ó).If 𝔰satisfies isHeadLeast,≼𝔰is transitive. Proof. Given 𝑥≼𝔰𝑦 and 𝑦≼𝔰𝑧 , we want to show 𝑥≼𝔰𝑧 . Consider the 3-element bag *𝑥, 𝑦, 𝑧+:M(𝐴) . Let 𝑢 be least(*𝑥, 𝑦, 𝑧+) , by Definition 73 and Proposition 72, 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 69 and 75, and Proposition 74, 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. V. Choudhury and W. Wong 25 ▶ Proposition 76 ( Ó ).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 72, we have 𝑥≼𝔰𝑦 iff 𝑥≤𝑦 . We now have a total order 𝑥≼𝔰𝑦 equivalent to 𝑥≤𝑦.◀ 5.3.4 Equivalence of order and sections We want to improve the embedding to an isomorphism, and it remains to show that we can turn a section satisfying isHeadLeast to a total order ≼𝔰 , then reconstruct the same section from ≼𝔰. Unfortunately, isHeadLeast is not enough to guarantee this. ▶ Proposition 77 ( Ó ).There is no equivalence between sections satisfying the isHeadLeast axiom and total orders on 𝐴. Proof. We consider the set N of natural numbers, and construct a 𝔰 that satisfies isHeadLeast but is not a sort function. Let the correct insertion sort function be sort:M(N) → L(N) . We define reverseTail which reverses only the tail of a list, and a section 𝔰 that sorts correctly using sort then reverses the tail: reverseTail([]) ≔[] reverseTail(𝑥:: xs)≔𝑥:: reverse(xs) 𝔰(xs)≔reverseTail(sort(xs)) For example: 𝔰(*2,3,1,4+)=[1,4,3,2] 𝔰(*2,3,1+)=[1,3,2] 𝔰(*2,3+)=[2,3] Note that both sort and 𝔰 satisfy isHeadLeast , but 𝔰 only sorts 2-element lists correctly, and 𝔰 ≠ sort . By Proposition 76 we can use both sort and 𝔰 to reconstruct the same ≤ on N . Hence, two different sections satisfying isHeadLeast map to the same total order. ◀ Therefore, we need to introduce a second axiom of sorting. ▶Definition 78 (Ó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 characterisation of sorted lists, found in textbooks, such as in [5]. ▶ Definition 79 ( Ó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)