cleaning up order theory (#591)

- `preorder-Prop` -> `Preorder-Prop` - `poset-Prop` -> `Poset-Prop`
UniMath · May 4, 2023 · 033ede4 · 033ede4
1 parent 8799a4a
commit 033ede4
Show file tree

Hide file tree

Showing 50 changed files with 1,049 additions and 961 deletions.
diff --git a/src/lists/quicksort-lists.lagda.md b/src/lists/quicksort-lists.lagda.md
@@ -47,55 +47,55 @@ applying the quicksort algorithm.
 
 ```agda
 module _
-  {l1 l2 : Level} (X : total-decidable-Poset l1 l2)
+  {l1 l2 : Level} (X : total-Decidable-Poset l1 l2)
   where
 
   helper-quicksort-list-divide-leq :
-    (x : element-total-decidable-Poset X) →
-    (y : element-total-decidable-Poset X) →
-    leq-or-strict-greater-decidable-Poset X x y →
-    list (element-total-decidable-Poset X) →
-    list (element-total-decidable-Poset X)
+    (x : element-total-Decidable-Poset X) →
+    (y : element-total-Decidable-Poset X) →
+    leq-or-strict-greater-Decidable-Poset X x y →
+    list (element-total-Decidable-Poset X) →
+    list (element-total-Decidable-Poset X)
   helper-quicksort-list-divide-leq x y (inl p) l = l
   helper-quicksort-list-divide-leq x y (inr p) l = cons y l
 
   quicksort-list-divide-leq :
-    element-total-decidable-Poset X → list (element-total-decidable-Poset X) →
-    list (element-total-decidable-Poset X)
+    element-total-Decidable-Poset X → list (element-total-Decidable-Poset X) →
+    list (element-total-Decidable-Poset X)
   quicksort-list-divide-leq x nil = nil
   quicksort-list-divide-leq x (cons y l) =
     helper-quicksort-list-divide-leq
       ( x)
       ( y)
-      ( is-leq-or-strict-greater-total-decidable-Poset X x y)
+      ( is-leq-or-strict-greater-total-Decidable-Poset X x y)
       ( quicksort-list-divide-leq x l)
 
   helper-quicksort-list-divide-strict-greater :
-    (x : element-total-decidable-Poset X) →
-    (y : element-total-decidable-Poset X) →
-    leq-or-strict-greater-decidable-Poset X x y →
-    list (element-total-decidable-Poset X) →
-    list (element-total-decidable-Poset X)
+    (x : element-total-Decidable-Poset X) →
+    (y : element-total-Decidable-Poset X) →
+    leq-or-strict-greater-Decidable-Poset X x y →
+    list (element-total-Decidable-Poset X) →
+    list (element-total-Decidable-Poset X)
   helper-quicksort-list-divide-strict-greater x y (inl p) l = cons y l
   helper-quicksort-list-divide-strict-greater x y (inr p) l = l
 
   quicksort-list-divide-strict-greater :
-    element-total-decidable-Poset X → list (element-total-decidable-Poset X) →
-    list (element-total-decidable-Poset X)
+    element-total-Decidable-Poset X → list (element-total-Decidable-Poset X) →
+    list (element-total-Decidable-Poset X)
   quicksort-list-divide-strict-greater x nil = nil
   quicksort-list-divide-strict-greater x (cons y l) =
     helper-quicksort-list-divide-strict-greater
       ( x)
       ( y)
-      ( is-leq-or-strict-greater-total-decidable-Poset X x y)
+      ( is-leq-or-strict-greater-total-Decidable-Poset X x y)
       ( quicksort-list-divide-strict-greater x l)
 
   private
     helper-inequality-length-quicksort-list-divide-leq :
-      (x : element-total-decidable-Poset X) →
-      (y : element-total-decidable-Poset X) →
-      (p : leq-or-strict-greater-decidable-Poset X x y) →
-      (l : list (element-total-decidable-Poset X)) →
+      (x : element-total-Decidable-Poset X) →
+      (y : element-total-Decidable-Poset X) →
+      (p : leq-or-strict-greater-Decidable-Poset X x y) →
+      (l : list (element-total-Decidable-Poset X)) →
       length-list (helper-quicksort-list-divide-leq x y p l) ≤-ℕ
       length-list (cons y l)
     helper-inequality-length-quicksort-list-divide-leq x y (inl _) l =
@@ -104,8 +104,8 @@ module _
       refl-leq-ℕ (length-list (cons y l))
 
     inequality-length-quicksort-list-divide-leq :
-      (x : element-total-decidable-Poset X) →
-      (l : list (element-total-decidable-Poset X)) →
+      (x : element-total-Decidable-Poset X) →
+      (l : list (element-total-Decidable-Poset X)) →
       length-list (quicksort-list-divide-leq x l) ≤-ℕ length-list l
     inequality-length-quicksort-list-divide-leq x nil = star
     inequality-length-quicksort-list-divide-leq x (cons y l) =
@@ -117,14 +117,14 @@ module _
         ( helper-inequality-length-quicksort-list-divide-leq
             ( x)
             ( y)
-            ( is-leq-or-strict-greater-total-decidable-Poset X x y)
+            ( is-leq-or-strict-greater-total-Decidable-Poset X x y)
             ( quicksort-list-divide-leq x l))
 
     helper-inequality-length-quicksort-list-divide-strict-greater :
-      (x : element-total-decidable-Poset X) →
-      (y : element-total-decidable-Poset X) →
-      (p : leq-or-strict-greater-decidable-Poset X x y) →
-      (l : list (element-total-decidable-Poset X)) →
+      (x : element-total-Decidable-Poset X) →
+      (y : element-total-Decidable-Poset X) →
+      (p : leq-or-strict-greater-Decidable-Poset X x y) →
+      (l : list (element-total-Decidable-Poset X)) →
       length-list (helper-quicksort-list-divide-strict-greater x y p l) ≤-ℕ
       length-list (cons y l)
     helper-inequality-length-quicksort-list-divide-strict-greater
@@ -141,8 +141,8 @@ module _
       succ-leq-ℕ (length-list l)
 
     inequality-length-quicksort-list-divide-strict-greater :
-      (x : element-total-decidable-Poset X) →
-      (l : list (element-total-decidable-Poset X)) →
+      (x : element-total-Decidable-Poset X) →
+      (l : list (element-total-Decidable-Poset X)) →
       length-list (quicksort-list-divide-strict-greater x l) ≤-ℕ length-list l
     inequality-length-quicksort-list-divide-strict-greater x nil = star
     inequality-length-quicksort-list-divide-strict-greater x (cons y l) =
@@ -154,23 +154,23 @@ module _
         ( helper-inequality-length-quicksort-list-divide-strict-greater
             ( x)
             ( y)
-            ( is-leq-or-strict-greater-total-decidable-Poset X x y)
+            ( is-leq-or-strict-greater-total-Decidable-Poset X x y)
             ( quicksort-list-divide-strict-greater x l))
 
   base-quicksort-list :
-    (l : list (element-total-decidable-Poset X)) → zero-ℕ ＝ length-list l →
-    list (element-total-decidable-Poset X)
+    (l : list (element-total-Decidable-Poset X)) → zero-ℕ ＝ length-list l →
+    list (element-total-Decidable-Poset X)
   base-quicksort-list nil x = nil
 
   inductive-step-quicksort-list :
     (k : ℕ) →
     □-≤-ℕ
     ( λ n →
-         (l : list (element-total-decidable-Poset X)) →
-         n ＝ length-list l → list (element-total-decidable-Poset X))
+         (l : list (element-total-Decidable-Poset X)) →
+         n ＝ length-list l → list (element-total-Decidable-Poset X))
     k →
-    (l : list (element-total-decidable-Poset X)) →
-    succ-ℕ k ＝ length-list l → list (element-total-decidable-Poset X)
+    (l : list (element-total-Decidable-Poset X)) →
+    succ-ℕ k ＝ length-list l → list (element-total-Decidable-Poset X)
   inductive-step-quicksort-list k sort (cons x l) p =
     concat-list
       ( sort
@@ -197,13 +197,13 @@ module _
               ( refl)))
 
   quicksort-list :
-    list (element-total-decidable-Poset X) →
-    list (element-total-decidable-Poset X)
+    list (element-total-Decidable-Poset X) →
+    list (element-total-Decidable-Poset X)
   quicksort-list l =
     strong-ind-ℕ
       ( λ n →
-        (l : list (element-total-decidable-Poset X)) → n ＝ length-list l →
-        list (element-total-decidable-Poset X))
+        (l : list (element-total-Decidable-Poset X)) → n ＝ length-list l →
+        list (element-total-Decidable-Poset X))
       ( base-quicksort-list)
       ( inductive-step-quicksort-list)
       ( length-list l)

diff --git a/src/lists/sort-by-insertion-vectors.lagda.md b/src/lists/sort-by-insertion-vectors.lagda.md
@@ -47,15 +47,15 @@ of the vector.
 
 ```agda
 module _
-  {l1 l2 : Level} (X : total-decidable-Poset l1 l2)
+  {l1 l2 : Level} (X : total-Decidable-Poset l1 l2)
   where
 
   helper-insertion-sort-vec :
     {n : ℕ}
-    (x y : element-total-decidable-Poset X)
-    (l : vec (element-total-decidable-Poset X) n) →
-    leq-or-strict-greater-decidable-Poset X x y →
-    vec (element-total-decidable-Poset X) (succ-ℕ (succ-ℕ (n)))
+    (x y : element-total-Decidable-Poset X)
+    (l : vec (element-total-Decidable-Poset X) n) →
+    leq-or-strict-greater-Decidable-Poset X x y →
+    vec (element-total-Decidable-Poset X) (succ-ℕ (succ-ℕ (n)))
   helper-insertion-sort-vec x y l (inl p) = x ∷ y ∷ l
   helper-insertion-sort-vec {0} x y empty-vec (inr p) = y ∷ x ∷ empty-vec
   helper-insertion-sort-vec {succ-ℕ n} x y (z ∷ l) (inr p) =
@@ -64,20 +64,20 @@ module _
       ( x)
       ( z)
       ( l)
-      ( is-leq-or-strict-greater-total-decidable-Poset X x z))
+      ( is-leq-or-strict-greater-total-Decidable-Poset X x z))
 
   insertion-sort-vec :
     {n : ℕ} →
-    vec (element-total-decidable-Poset X) n →
-    vec (element-total-decidable-Poset X) n
+    vec (element-total-Decidable-Poset X) n →
+    vec (element-total-Decidable-Poset X) n
   insertion-sort-vec {zero-ℕ} empty-vec = empty-vec
   insertion-sort-vec {1} l = l
   insertion-sort-vec {succ-ℕ (succ-ℕ n)} (x ∷ y ∷ l) =
     helper-insertion-sort-vec
       ( x)
       ( head-vec (insertion-sort-vec (y ∷ l)))
       ( tail-vec (insertion-sort-vec (y ∷ l)))
-      ( is-leq-or-strict-greater-total-decidable-Poset X _ _)
+      ( is-leq-or-strict-greater-total-Decidable-Poset X _ _)
 ```
 
 ## Properties
@@ -87,9 +87,9 @@ module _
 ```agda
   helper-permutation-insertion-sort-vec :
     {n : ℕ}
-    (x y : element-total-decidable-Poset X)
-    (l : vec (element-total-decidable-Poset X) n) →
-    leq-or-strict-greater-decidable-Poset X x y →
+    (x y : element-total-Decidable-Poset X)
+    (l : vec (element-total-Decidable-Poset X) n) →
+    leq-or-strict-greater-Decidable-Poset X x y →
     Permutation (succ-ℕ (succ-ℕ (n)))
   helper-permutation-insertion-sort-vec x y l (inl _) = id-equiv
   helper-permutation-insertion-sort-vec {0} x y empty-vec (inr _) =
@@ -101,12 +101,12 @@ module _
             ( x)
             ( z)
             ( l)
-            ( is-leq-or-strict-greater-total-decidable-Poset X x z))
+            ( is-leq-or-strict-greater-total-Decidable-Poset X x z))
           ( id-equiv))))
 
   permutation-insertion-sort-vec :
     {n : ℕ}
-    (v : vec (element-total-decidable-Poset X) n) →
+    (v : vec (element-total-Decidable-Poset X) n) →
     Permutation n
   permutation-insertion-sort-vec {zero-ℕ} empty-vec = id-equiv
   permutation-insertion-sort-vec {1} l = id-equiv
@@ -118,13 +118,13 @@ module _
       ( x)
       ( head-vec (insertion-sort-vec (y ∷ l)))
       ( tail-vec (insertion-sort-vec (y ∷ l)))
-      ( is-leq-or-strict-greater-total-decidable-Poset X _ _)
+      ( is-leq-or-strict-greater-total-Decidable-Poset X _ _)
 
   helper-is-permutation-insertion-sort-vec :
     {n : ℕ}
-    (x y : element-total-decidable-Poset X)
-    (v : vec (element-total-decidable-Poset X) n)
-    (p : leq-or-strict-greater-decidable-Poset X x y) →
+    (x y : element-total-Decidable-Poset X)
+    (v : vec (element-total-Decidable-Poset X) n)
+    (p : leq-or-strict-greater-Decidable-Poset X x y) →
     helper-insertion-sort-vec x y v p ＝
     permute-vec
       ( succ-ℕ (succ-ℕ n))
@@ -149,7 +149,7 @@ module _
             ( x)
             ( z)
             ( v)
-            ( is-leq-or-strict-greater-total-decidable-Poset X x z))
+            ( is-leq-or-strict-greater-total-Decidable-Poset X x z))
           ( tail-vec
             ( permute-vec
               ( succ-ℕ (succ-ℕ (succ-ℕ n)))
@@ -159,7 +159,7 @@ module _
               ( x)
               ( z)
               ( v)
-              ( is-leq-or-strict-greater-total-decidable-Poset X x z)) ∙
+              ( is-leq-or-strict-greater-total-Decidable-Poset X x z)) ∙
             ( ap
               ( tail-vec)
               ( ap-permute-vec
@@ -168,7 +168,7 @@ module _
                     ( x)
                     ( z)
                     ( v)
-                    ( is-leq-or-strict-greater-total-decidable-Poset
+                    ( is-leq-or-strict-greater-total-Decidable-Poset
                       ( X)
                       ( x)
                       ( z)))
@@ -189,15 +189,15 @@ module _
                         ( x)
                         ( z)
                         ( v)
-                        ( is-leq-or-strict-greater-total-decidable-Poset
+                        ( is-leq-or-strict-greater-total-Decidable-Poset
                           ( X)
                           ( x)
                           ( z)))
                         ( id-equiv))))))))
 
   is-permutation-insertion-sort-vec :
     {n : ℕ}
-    (v : vec (element-total-decidable-Poset X) n) →
+    (v : vec (element-total-Decidable-Poset X) n) →
     insertion-sort-vec v ＝ permute-vec n v (permutation-insertion-sort-vec v)
   is-permutation-insertion-sort-vec {0} empty-vec = refl
   is-permutation-insertion-sort-vec {1} (x ∷ empty-vec) = refl
@@ -206,13 +206,13 @@ module _
         ( x)
         ( head-vec (insertion-sort-vec (y ∷ v)))
         ( tail-vec (insertion-sort-vec (y ∷ v)))
-        ( is-leq-or-strict-greater-total-decidable-Poset X _ _)) ∙
+        ( is-leq-or-strict-greater-total-Decidable-Poset X _ _)) ∙
       ( ( ap-permute-vec
           ( helper-permutation-insertion-sort-vec
             ( x)
             ( head-vec (insertion-sort-vec (y ∷ v)))
             ( tail-vec (insertion-sort-vec (y ∷ v)))
-            ( is-leq-or-strict-greater-total-decidable-Poset X _ _))
+            ( is-leq-or-strict-greater-total-Decidable-Poset X _ _))
           ( ap
             ( λ l → x ∷ l)
             ( cons-head-tail-vec n (insertion-sort-vec (y ∷ v)) ∙
@@ -228,17 +228,17 @@ module _
                 ( x)
                 ( head-vec (insertion-sort-vec (y ∷ v)))
                 ( tail-vec (insertion-sort-vec (y ∷ v)))
-                ( is-leq-or-strict-greater-total-decidable-Poset X _ _)))))))
+                ( is-leq-or-strict-greater-total-Decidable-Poset X _ _)))))))
 ```
 
 ### Sort by insertion is sorting vectors
 
 ```agda
   helper-is-sorting-insertion-sort-vec :
     {n : ℕ}
-    (x y : element-total-decidable-Poset X)
-    (v : vec (element-total-decidable-Poset X) n) →
-    (p : leq-or-strict-greater-decidable-Poset X x y) →
+    (x y : element-total-Decidable-Poset X)
+    (v : vec (element-total-Decidable-Poset X) n) →
+    (p : leq-or-strict-greater-Decidable-Poset X x y) →
     is-sorted-vec X (y ∷ v) →
     is-sorted-vec X (helper-insertion-sort-vec x y v p)
   helper-is-sorting-insertion-sort-vec {0} x y empty-vec (inl p) _ =
@@ -258,7 +258,7 @@ module _
             ( x)
             ( z)
             ( v)
-            ( is-leq-or-strict-greater-total-decidable-Poset X x z)))
+            ( is-leq-or-strict-greater-total-Decidable-Poset X x z)))
         ( is-least-element-permute-vec
           ( X)
           ( y)
@@ -267,7 +267,7 @@ module _
             ( x)
             ( z)
             ( v)
-            ( is-leq-or-strict-greater-total-decidable-Poset X x z))
+            ( is-leq-or-strict-greater-total-Decidable-Poset X x z))
           ( pr2 p ,
             pr1
               ( is-sorted-least-element-vec-is-sorted-vec
@@ -280,17 +280,17 @@ module _
              ( x)
              ( z)
              ( v)
-             ( is-leq-or-strict-greater-total-decidable-Poset X x z))
+             ( is-leq-or-strict-greater-total-Decidable-Poset X x z))
            ( helper-is-sorting-insertion-sort-vec
              ( x)
              ( z)
              ( v)
-             ( is-leq-or-strict-greater-total-decidable-Poset X x z)
+             ( is-leq-or-strict-greater-total-Decidable-Poset X x z)
              ( is-sorted-tail-is-sorted-vec X (y ∷ z ∷ v) s)))
 
   is-sorting-insertion-sort-vec :
     {n : ℕ}
-    (v : vec (element-total-decidable-Poset X) n) →
+    (v : vec (element-total-Decidable-Poset X) n) →
     is-sorted-vec X (insertion-sort-vec v)
   is-sorting-insertion-sort-vec {0} v = raise-star
   is-sorting-insertion-sort-vec {1} v = raise-star
@@ -299,7 +299,7 @@ module _
       ( x)
       ( head-vec (insertion-sort-vec (y ∷ v)))
       ( tail-vec (insertion-sort-vec (y ∷ v)))
-      ( is-leq-or-strict-greater-total-decidable-Poset X _ _)
+      ( is-leq-or-strict-greater-total-Decidable-Poset X _ _)
       ( tr
         ( λ l → is-sorted-vec X l)
         ( inv (cons-head-tail-vec n (insertion-sort-vec (y ∷ v))))