Fix name type sequences posets (#1407)

This PR fixes some naming issues raised in
#1401 (comment)
and https://github.com/UniMath/agda-unimath/pull/1388/files#r2054971412.

It introduces the following changes:

- `type-sequence-Preorder` and `type-sequence-Poset` are now
`sequence-type-Preorder` and `sequence-type-Poset`, since they're
actually `sequence (type-XX ..)`;
- on the other hand, `type-increasing-sequence-Poset` is now called
`increasing-sequence-Poset` since it actively uses the poset structure
(like `isometry-Metric-Space` uses the metric structure). The
corresponding poset is now called `poset-increasing-sequence-Poset`.

Author: malarbol

src/order-theory/increasing-sequences-posets.lagda.md

@@ -40,7 +40,7 @@ or, equivalently, if `uₙ ≤ uₙ₊₁` for all `n : ℕ`.
 
 ```agda
 module _
-  {l1 l2 : Level} (P : Poset l1 l2) (u : type-sequence-Poset P)
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-type-Poset P)
   where
 
   is-increasing-prop-sequence-Poset : Prop l2
@@ -59,23 +59,23 @@ module _
   {l1 l2 : Level} (P : Poset l1 l2)
   where
 
-  increasing-sequence-Poset : Poset (l1 ⊔ l2) l2
-  increasing-sequence-Poset =
+  poset-increasing-sequence-Poset : Poset (l1 ⊔ l2) l2
+  poset-increasing-sequence-Poset =
     poset-Subposet
       ( sequence-Poset P)
       ( is-increasing-prop-sequence-Poset P)
 
-  type-increasing-sequence-Poset : UU (l1 ⊔ l2)
-  type-increasing-sequence-Poset =
-    type-Poset increasing-sequence-Poset
+  increasing-sequence-Poset : UU (l1 ⊔ l2)
+  increasing-sequence-Poset =
+    type-Poset poset-increasing-sequence-Poset
 
   seq-increasing-sequence-Poset :
-    type-increasing-sequence-Poset →
-    type-sequence-Poset P
+    increasing-sequence-Poset →
+    sequence-type-Poset P
   seq-increasing-sequence-Poset = pr1
 
   is-increasing-seq-increasing-sequence-Poset :
-    (u : type-increasing-sequence-Poset) →
+    (u : increasing-sequence-Poset) →
     is-increasing-sequence-Poset
       ( P)
       ( seq-increasing-sequence-Poset u)
@@ -88,7 +88,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (P : Poset l1 l2) (u : type-sequence-Poset P)
+  {l1 l2 : Level} (P : Poset l1 l2) (u : sequence-type-Poset P)
   where
 
   is-increasing-leq-succ-sequence-Poset :

src/order-theory/sequences-posets.lagda.md

@@ -25,7 +25,7 @@ open import order-theory.sequences-preorders
 
 ## Idea
 
-A {{#concept "sequence" Disambiguation="in a poset" Agda=type-sequence-Poset}}
+A {{#concept "sequence" Disambiguation="in a poset" Agda=sequence-type-Poset}}
 in a [poset](order-theory.posets.md) is a [sequence](foundation.sequences.md) in
 its underlying type.
 
@@ -38,8 +38,8 @@ module _
   {l1 l2 : Level} (P : Poset l1 l2)
   where
 
-  type-sequence-Poset : UU l1
-  type-sequence-Poset = type-sequence-Preorder (preorder-Poset P)
+  sequence-type-Poset : UU l1
+  sequence-type-Poset = sequence-type-Preorder (preorder-Poset P)
 ```
 
 ### Pointwise comparison on sequences in partially ordered sets
@@ -50,25 +50,25 @@ module _
   where
 
   leq-value-prop-sequence-Poset :
-    (u v : type-sequence-Poset P) → ℕ → Prop l2
+    (u v : sequence-type-Poset P) → ℕ → Prop l2
   leq-value-prop-sequence-Poset =
     leq-value-prop-sequence-Preorder (preorder-Poset P)
 
   leq-value-sequence-Poset :
-    (u v : type-sequence-Poset P) → ℕ → UU l2
+    (u v : sequence-type-Poset P) → ℕ → UU l2
   leq-value-sequence-Poset =
     leq-value-sequence-Preorder (preorder-Poset P)
 
-  leq-prop-sequence-Poset : (u v : type-sequence-Poset P) → Prop l2
+  leq-prop-sequence-Poset : (u v : sequence-type-Poset P) → Prop l2
   leq-prop-sequence-Poset =
     leq-prop-sequence-Preorder (preorder-Poset P)
 
-  leq-sequence-Poset : (u v : type-sequence-Poset P) → UU l2
+  leq-sequence-Poset : (u v : sequence-type-Poset P) → UU l2
   leq-sequence-Poset =
     leq-sequence-Preorder (preorder-Poset P)
 
   is-prop-leq-sequence-Poset :
-    (u v : type-sequence-Poset P) →
+    (u v : sequence-type-Poset P) →
     is-prop (leq-sequence-Poset u v)
   is-prop-leq-sequence-Poset =
     is-prop-leq-sequence-Preorder (preorder-Poset P)

src/order-theory/sequences-preorders.lagda.md

@@ -25,7 +25,7 @@ open import order-theory.preorders
 ## Idea
 
 A
-{{#concept "sequence" Disambiguation="in a preorder" Agda=type-sequence-Preorder}}
+{{#concept "sequence" Disambiguation="in a preorder" Agda=sequence-type-Preorder}}
 in a [preorder](order-theory.preorders.md) is a
 [sequence](foundation.sequences.md) in its underlying type.
 
@@ -38,15 +38,15 @@ module _
   {l1 l2 : Level} (P : Preorder l1 l2)
   where
 
-  type-sequence-Preorder : UU l1
-  type-sequence-Preorder = sequence (type-Preorder P)
+  sequence-type-Preorder : UU l1
+  sequence-type-Preorder = sequence (type-Preorder P)
 ```
 
 ### Pointwise comparison on sequences in preorders
 
 ```agda
 module _
-  {l1 l2 : Level} (P : Preorder l1 l2) (u v : type-sequence-Preorder P)
+  {l1 l2 : Level} (P : Preorder l1 l2) (u v : sequence-type-Preorder P)
   where
 
   leq-value-prop-sequence-Preorder : ℕ → Prop l2
@@ -82,7 +82,7 @@ module _
     transitive-leq-Preorder P (u n) (v n) (w n) (J n) (I n)
 
   sequence-Preorder : Preorder l1 l2
-  pr1 sequence-Preorder = type-sequence-Preorder P
+  pr1 sequence-Preorder = sequence-type-Preorder P
   pr1 (pr2 sequence-Preorder) = leq-prop-sequence-Preorder P
   pr1 (pr2 (pr2 sequence-Preorder)) = refl-leq-sequence-Preorder
   pr2 (pr2 (pr2 sequence-Preorder)) = transitive-leq-sequence-Preorder