From b959f9ffb2e36d120da002755d4e6f310bbe6963 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 13:50:28 -0500
Subject: [PATCH 01/17] extract order theory from PR 1211

---
 src/order-theory/chains-posets.lagda.md       |   4 +-
 .../decidable-total-orders.lagda.md           | 169 ------------------
 .../deflationary-maps-posets.lagda.md         | 145 +++++++++++++++
 .../deflationary-maps-preorders.lagda.md      | 146 +++++++++++++++
 src/order-theory/galois-connections.lagda.md  |   4 +-
 .../homomorphisms-large-suplattices.lagda.md  |   4 +-
 .../inflationary-maps-posets.lagda.md         | 145 +++++++++++++++
 .../inflationary-maps-preorders.lagda.md      | 146 +++++++++++++++
 ...onary-maps-strictly-ordered-types.lagda.md | 162 +++++++++++++++++
 src/order-theory/opposite-preorders.lagda.md  |   2 +-
 .../order-preserving-maps-posets.lagda.md     |   6 +-
 .../order-preserving-maps-preorders.lagda.md  |  58 +++---
 .../strict-order-preserving-maps.lagda.md     | 153 ++++++++++++++++
 .../strictly-ordered-sets.lagda.md            | 115 ++++++++++++
 .../strictly-ordered-types.lagda.md           |  92 ++++++++++
 15 files changed, 1150 insertions(+), 201 deletions(-)
 create mode 100644 src/order-theory/deflationary-maps-posets.lagda.md
 create mode 100644 src/order-theory/deflationary-maps-preorders.lagda.md
 create mode 100644 src/order-theory/inflationary-maps-posets.lagda.md
 create mode 100644 src/order-theory/inflationary-maps-preorders.lagda.md
 create mode 100644 src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
 create mode 100644 src/order-theory/strict-order-preserving-maps.lagda.md
 create mode 100644 src/order-theory/strictly-ordered-sets.lagda.md
 create mode 100644 src/order-theory/strictly-ordered-types.lagda.md

diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md
index 0136242af1..404b506ee9 100644
--- a/src/order-theory/chains-posets.lagda.md
+++ b/src/order-theory/chains-posets.lagda.md
@@ -130,7 +130,7 @@ module _
                   inl-disjunction
                     ( concatenate-eq-leq-eq-Poset' X
                       ( pr2 p)
-                      ( preserves-order-map-hom-Poset (poset-Total-Order T) X f
+                      ( preserves-order-hom-Poset (poset-Total-Order T) X f
                         ( pr1 p)
                         ( pr1 q)
                         ( H))
@@ -139,7 +139,7 @@ module _
                   inr-disjunction
                     ( concatenate-eq-leq-eq-Poset' X
                       ( pr2 q)
-                      ( preserves-order-map-hom-Poset (poset-Total-Order T) X f
+                      ( preserves-order-hom-Poset (poset-Total-Order T) X f
                         ( pr1 q)
                         ( pr1 p)
                         ( H))
diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md
index 1bd894c446..2aeb739708 100644
--- a/src/order-theory/decidable-total-orders.lagda.md
+++ b/src/order-theory/decidable-total-orders.lagda.md
@@ -11,7 +11,6 @@ open import foundation.binary-relations
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
-open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
@@ -19,8 +18,6 @@ open import foundation.universe-levels
 
 open import order-theory.decidable-posets
 open import order-theory.decidable-total-preorders
-open import order-theory.greatest-lower-bounds-posets
-open import order-theory.least-upper-bounds-posets
 open import order-theory.posets
 open import order-theory.preorders
 open import order-theory.total-orders
@@ -184,169 +181,3 @@ module _
   set-Decidable-Total-Order : Set l1
   set-Decidable-Total-Order = set-Poset poset-Decidable-Total-Order
 ```
-
-## Properties
-
-### Any two elements in a decidable total order have a minimum and maximum
-
-```agda
-module _
-  {l1 l2 : Level}
-  (T : Decidable-Total-Order l1 l2)
-  (x y : type-Decidable-Total-Order T)
-  where
-
-  min-Decidable-Total-Order : type-Decidable-Total-Order T
-  min-Decidable-Total-Order =
-    rec-coproduct
-      ( λ x≤y → x)
-      ( λ y<x → y)
-      ( is-leq-or-strict-greater-Decidable-Total-Order T x y)
-
-  max-Decidable-Total-Order : type-Decidable-Total-Order T
-  max-Decidable-Total-Order =
-    rec-coproduct
-      ( λ x≤y → y)
-      ( λ y<x → x)
-      ( is-leq-or-strict-greater-Decidable-Total-Order T x y)
-```
-
-### The minimum is a lower bound
-
-```agda
-  leq-left-min-Decidable-Total-Order :
-    leq-Decidable-Total-Order T min-Decidable-Total-Order x
-  leq-left-min-Decidable-Total-Order
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = refl-leq-Decidable-Total-Order T x
-  ... | inr y<x = pr2 y<x
-
-  leq-right-min-Decidable-Total-Order :
-    leq-Decidable-Total-Order T min-Decidable-Total-Order y
-  leq-right-min-Decidable-Total-Order
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = x≤y
-  ... | inr y<x = refl-leq-Decidable-Total-Order T y
-```
-
-### The maximum of two values is an upper bound
-
-```agda
-  leq-left-max-Decidable-Total-Order :
-    leq-Decidable-Total-Order T x max-Decidable-Total-Order
-  leq-left-max-Decidable-Total-Order
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = x≤y
-  ... | inr y<x = refl-leq-Decidable-Total-Order T x
-
-  leq-right-max-Decidable-Total-Order :
-    leq-Decidable-Total-Order T y max-Decidable-Total-Order
-  leq-right-max-Decidable-Total-Order
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = refl-leq-Decidable-Total-Order T y
-  ... | inr y<x = pr2 y<x
-```
-
-### The minimum operation is commutative
-
-```agda
-module _
-  {l1 l2 : Level}
-  (T : Decidable-Total-Order l1 l2)
-  (x y : type-Decidable-Total-Order T)
-  where
-
-  commutative-min-Decidable-Total-Order :
-    min-Decidable-Total-Order T x y ＝ min-Decidable-Total-Order T y x
-  commutative-min-Decidable-Total-Order
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-          | is-leq-or-strict-greater-Decidable-Total-Order T y x
-  ... | inl x≤y | inl y≤x =
-    antisymmetric-leq-Decidable-Total-Order T x y x≤y y≤x
-  ... | inl x≤y | inr x<y = refl
-  ... | inr y<x | inl y≤x = refl
-  ... | inr y<x | inr x<y =
-    ex-falso
-      (pr1
-        ( x<y)
-        ( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
-```
-
-### The maximum operation is commutative
-
-```agda
-  commutative-max-Decidable-Total-Order :
-    max-Decidable-Total-Order T x y ＝ max-Decidable-Total-Order T y x
-  commutative-max-Decidable-Total-Order
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-          | is-leq-or-strict-greater-Decidable-Total-Order T y x
-  ... | inl x≤y | inl y≤x =
-    antisymmetric-leq-Decidable-Total-Order T y x y≤x x≤y
-  ... | inl x≤y | inr x<y = refl
-  ... | inr y<x | inl y≤x = refl
-  ... | inr y<x | inr x<y =
-    ex-falso
-      (pr1
-        ( x<y)
-        ( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
-```
-
-### The minimum of two values is their greatest lower bound
-
-```agda
-  min-is-greatest-binary-lower-bound-Decidable-Total-Order :
-    is-greatest-binary-lower-bound-Poset
-      ( poset-Decidable-Total-Order T)
-      ( x)
-      ( y)
-      ( min-Decidable-Total-Order T x y)
-  pr1 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) (z≤x , z≤y)
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = z≤x
-  ... | inr y<x = z≤y
-  pr1 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = z≤min
-  ... | inr y<x = transitive-leq-Decidable-Total-Order T z y x (pr2 y<x) z≤min
-  pr2 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = transitive-leq-Decidable-Total-Order T z x y x≤y z≤min
-  ... | inr y<x = z≤min
-
-  has-greatest-binary-lower-bound-Decidable-Total-Order :
-    has-greatest-binary-lower-bound-Poset (poset-Decidable-Total-Order T) x y
-  pr1 has-greatest-binary-lower-bound-Decidable-Total-Order =
-    min-Decidable-Total-Order T x y
-  pr2 has-greatest-binary-lower-bound-Decidable-Total-Order =
-    min-is-greatest-binary-lower-bound-Decidable-Total-Order
-```
-
-### The maximum of two values is their least upper bound
-
-```agda
-  max-is-least-binary-upper-bound-Decidable-Total-Order :
-    is-least-binary-upper-bound-Poset
-      ( poset-Decidable-Total-Order T)
-      ( x)
-      ( y)
-      ( max-Decidable-Total-Order T x y)
-  pr1 (max-is-least-binary-upper-bound-Decidable-Total-Order z) (x≤z , y≤z)
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = y≤z
-  ... | inr y<x = x≤z
-  pr1 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = transitive-leq-Decidable-Total-Order T x y z min≤z x≤y
-  ... | inr y<x = min≤z
-  pr2 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
-    with is-leq-or-strict-greater-Decidable-Total-Order T x y
-  ... | inl x≤y = min≤z
-  ... | inr y<x = transitive-leq-Decidable-Total-Order T y x z min≤z (pr2 y<x)
-
-  has-least-binary-upper-bound-Decidable-Total-Order :
-    has-least-binary-upper-bound-Poset (poset-Decidable-Total-Order T) x y
-  pr1 has-least-binary-upper-bound-Decidable-Total-Order =
-    max-Decidable-Total-Order T x y
-  pr2 has-least-binary-upper-bound-Decidable-Total-Order =
-    max-is-least-binary-upper-bound-Decidable-Total-Order
-```
diff --git a/src/order-theory/deflationary-maps-posets.lagda.md b/src/order-theory/deflationary-maps-posets.lagda.md
new file mode 100644
index 0000000000..e765e77437
--- /dev/null
+++ b/src/order-theory/deflationary-maps-posets.lagda.md
@@ -0,0 +1,145 @@
+# Deflationary maps on a poset
+
+```agda
+module order-theory.deflationary-maps-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.deflationary-maps-preorders
+open import order-theory.order-preserving-maps-posets
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be an
+{{#concept "deflationary map" Disambiguation="poset" Agda=deflationary-map-Poset}} if the inequality
+
+$$
+  f(x) \leq x
+$$
+
+holds for any element $x : P$. In other words, a map on a poset is deflationary precisely when the map on its underlying [preorder](order-theory.preorders.md) is [deflationary](order-theory.deflationary-maps-preorders.md). If $f$ is also [order preserving](order-theory.order-preserving-maps-posets.md) we say that $f$ is an {{#concept "deflationary morphism" Disambiguation="poset" Agda=deflationary-hom-Poset}}.
+
+## Definitions
+
+### The predicate of being an deflationary map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : type-Poset P → type-Poset P)
+  where
+
+  is-deflationary-prop-map-Poset :
+    Prop (l1 ⊔ l2)
+  is-deflationary-prop-map-Poset =
+    is-deflationary-prop-map-Preorder (preorder-Poset P) f
+
+  is-deflationary-map-Poset :
+    UU (l1 ⊔ l2)
+  is-deflationary-map-Poset =
+    is-deflationary-map-Preorder (preorder-Poset P) f
+
+  is-prop-is-deflationary-map-Poset :
+    is-prop is-deflationary-map-Poset
+  is-prop-is-deflationary-map-Poset =
+    is-prop-is-deflationary-map-Preorder (preorder-Poset P) f
+```
+
+### The type of deflationary maps on a poset
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  deflationary-map-Poset :
+    UU (l1 ⊔ l2)
+  deflationary-map-Poset =
+    deflationary-map-Preorder (preorder-Poset P)
+
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : deflationary-map-Poset P)
+  where
+
+  map-deflationary-map-Poset :
+    type-Poset P → type-Poset P
+  map-deflationary-map-Poset =
+    map-deflationary-map-Preorder (preorder-Poset P) f
+
+  is-deflationary-deflationary-map-Poset :
+    is-deflationary-map-Poset P map-deflationary-map-Poset
+  is-deflationary-deflationary-map-Poset =
+    is-deflationary-deflationary-map-Preorder (preorder-Poset P) f
+```
+
+### The predicate on order preserving maps of being deflationary
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : hom-Poset P P)
+  where
+
+  is-deflationary-prop-hom-Poset : Prop (l1 ⊔ l2)
+  is-deflationary-prop-hom-Poset =
+    is-deflationary-prop-hom-Preorder (preorder-Poset P) f
+
+  is-deflationary-hom-Poset : UU (l1 ⊔ l2)
+  is-deflationary-hom-Poset =
+    is-deflationary-hom-Preorder (preorder-Poset P) f
+
+  is-prop-is-deflationary-hom-Poset :
+    is-prop is-deflationary-hom-Poset
+  is-prop-is-deflationary-hom-Poset =
+    is-prop-is-deflationary-hom-Preorder (preorder-Poset P) f
+```
+
+### The type of deflationary morphisms on a poset
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  deflationary-hom-Poset : UU (l1 ⊔ l2)
+  deflationary-hom-Poset =
+    deflationary-hom-Preorder (preorder-Poset P)
+
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : deflationary-hom-Poset P)
+  where
+
+  hom-deflationary-hom-Poset :
+    hom-Poset P P
+  hom-deflationary-hom-Poset =
+    hom-deflationary-hom-Preorder (preorder-Poset P) f
+
+  map-deflationary-hom-Poset :
+    type-Poset P → type-Poset P
+  map-deflationary-hom-Poset =
+    map-deflationary-hom-Preorder (preorder-Poset P) f
+
+  preserves-order-deflationary-hom-Poset :
+    preserves-order-Poset P P map-deflationary-hom-Poset
+  preserves-order-deflationary-hom-Poset =
+    preserves-order-deflationary-hom-Preorder (preorder-Poset P) f
+
+  is-deflationary-deflationary-hom-Poset :
+    is-deflationary-map-Poset P map-deflationary-hom-Poset
+  is-deflationary-deflationary-hom-Poset =
+    is-deflationary-deflationary-hom-Preorder (preorder-Poset P) f
+
+  deflationary-map-deflationary-hom-Poset :
+    deflationary-map-Poset P
+  deflationary-map-deflationary-hom-Poset =
+    deflationary-map-deflationary-hom-Preorder (preorder-Poset P) f
+```
diff --git a/src/order-theory/deflationary-maps-preorders.lagda.md b/src/order-theory/deflationary-maps-preorders.lagda.md
new file mode 100644
index 0000000000..0368370cb8
--- /dev/null
+++ b/src/order-theory/deflationary-maps-preorders.lagda.md
@@ -0,0 +1,146 @@
+# Deflationary maps on a preorder
+
+```agda
+module order-theory.deflationary-maps-preorders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-preorders
+open import order-theory.preorders
+```
+
+</details>
+
+## Idea
+
+A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be an
+{{#concept "deflationary map" Disambiguation="preorder" Agda=deflationary-map-Preorder}} if the inequality
+
+$$
+  f(x) \leq x
+$$
+
+holds for any element $x : P$. If $f$ is also [order preserving](order-theory.order-preserving-maps-preorders.md) we say that $f$ is an {{#concept "deflationary morphism" Disambiguation="preorder" Agda=deflationary-hom-Preorder}}.
+
+## Definitions
+
+### The predicate of being an deflationary map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : type-Preorder P → type-Preorder P)
+  where
+
+  is-deflationary-prop-map-Preorder :
+    Prop (l1 ⊔ l2)
+  is-deflationary-prop-map-Preorder =
+    Π-Prop (type-Preorder P) (λ x → leq-prop-Preorder P (f x) x)
+
+  is-deflationary-map-Preorder :
+    UU (l1 ⊔ l2)
+  is-deflationary-map-Preorder =
+    type-Prop is-deflationary-prop-map-Preorder
+
+  is-prop-is-deflationary-map-Preorder :
+    is-prop is-deflationary-map-Preorder
+  is-prop-is-deflationary-map-Preorder =
+    is-prop-type-Prop is-deflationary-prop-map-Preorder
+```
+
+### The type of deflationary maps on a preorder
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2)
+  where
+
+  deflationary-map-Preorder :
+    UU (l1 ⊔ l2)
+  deflationary-map-Preorder =
+    type-subtype (is-deflationary-prop-map-Preorder P)
+
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : deflationary-map-Preorder P)
+  where
+
+  map-deflationary-map-Preorder :
+    type-Preorder P → type-Preorder P
+  map-deflationary-map-Preorder =
+    pr1 f
+
+  is-deflationary-deflationary-map-Preorder :
+    is-deflationary-map-Preorder P map-deflationary-map-Preorder
+  is-deflationary-deflationary-map-Preorder =
+    pr2 f
+```
+
+### The predicate on order preserving maps of being deflationary
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : hom-Preorder P P)
+  where
+
+  is-deflationary-prop-hom-Preorder : Prop (l1 ⊔ l2)
+  is-deflationary-prop-hom-Preorder =
+    is-deflationary-prop-map-Preorder P (map-hom-Preorder P P f)
+
+  is-deflationary-hom-Preorder : UU (l1 ⊔ l2)
+  is-deflationary-hom-Preorder =
+    is-deflationary-map-Preorder P (map-hom-Preorder P P f)
+
+  is-prop-is-deflationary-hom-Preorder :
+    is-prop is-deflationary-hom-Preorder
+  is-prop-is-deflationary-hom-Preorder =
+    is-prop-is-deflationary-map-Preorder P (map-hom-Preorder P P f)
+```
+
+### The type of deflationary morphisms on a preorder
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2)
+  where
+
+  deflationary-hom-Preorder : UU (l1 ⊔ l2)
+  deflationary-hom-Preorder =
+    type-subtype (is-deflationary-prop-hom-Preorder P)
+
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : deflationary-hom-Preorder P)
+  where
+
+  hom-deflationary-hom-Preorder :
+    hom-Preorder P P
+  hom-deflationary-hom-Preorder =
+    pr1 f
+
+  map-deflationary-hom-Preorder :
+    type-Preorder P → type-Preorder P
+  map-deflationary-hom-Preorder =
+    map-hom-Preorder P P hom-deflationary-hom-Preorder
+
+  preserves-order-deflationary-hom-Preorder :
+    preserves-order-Preorder P P map-deflationary-hom-Preorder
+  preserves-order-deflationary-hom-Preorder =
+    preserves-order-hom-Preorder P P hom-deflationary-hom-Preorder
+
+  is-deflationary-deflationary-hom-Preorder :
+    is-deflationary-map-Preorder P map-deflationary-hom-Preorder
+  is-deflationary-deflationary-hom-Preorder =
+    pr2 f
+
+  deflationary-map-deflationary-hom-Preorder :
+    deflationary-map-Preorder P
+  pr1 deflationary-map-deflationary-hom-Preorder =
+    map-deflationary-hom-Preorder
+  pr2 deflationary-map-deflationary-hom-Preorder =
+    is-deflationary-deflationary-hom-Preorder
+```
diff --git a/src/order-theory/galois-connections.lagda.md b/src/order-theory/galois-connections.lagda.md
index 5ae6e96259..e0ac6170c7 100644
--- a/src/order-theory/galois-connections.lagda.md
+++ b/src/order-theory/galois-connections.lagda.md
@@ -84,7 +84,7 @@ module _
     preserves-order-upper-adjoint-Galois-Connection :
       preserves-order-Poset Q P map-upper-adjoint-Galois-Connection
     preserves-order-upper-adjoint-Galois-Connection =
-      preserves-order-map-hom-Poset Q P upper-adjoint-Galois-Connection
+      preserves-order-hom-Poset Q P upper-adjoint-Galois-Connection
 
     is-upper-adjoint-upper-adjoint-Galois-Connection :
       is-upper-adjoint-Galois-Connection upper-adjoint-Galois-Connection
@@ -102,7 +102,7 @@ module _
     preserves-order-lower-adjoint-Galois-Connection :
       preserves-order-Poset P Q map-lower-adjoint-Galois-Connection
     preserves-order-lower-adjoint-Galois-Connection =
-      preserves-order-map-hom-Poset P Q lower-adjoint-Galois-Connection
+      preserves-order-hom-Poset P Q lower-adjoint-Galois-Connection
 
     adjoint-relation-Galois-Connection :
       (x : type-Poset P) (y : type-Poset Q) →
diff --git a/src/order-theory/homomorphisms-large-suplattices.lagda.md b/src/order-theory/homomorphisms-large-suplattices.lagda.md
index ac054229b8..181c422651 100644
--- a/src/order-theory/homomorphisms-large-suplattices.lagda.md
+++ b/src/order-theory/homomorphisms-large-suplattices.lagda.md
@@ -81,14 +81,14 @@ module _
         ( large-poset-Large-Suplattice L)
         ( hom-large-poset-hom-Large-Suplattice f)
 
-    preserves-order-map-hom-Large-Suplattice :
+    preserves-order-hom-Large-Suplattice :
       {l1 l2 : Level}
       (x : type-Large-Suplattice K l1) (y : type-Large-Suplattice K l2) →
       leq-Large-Suplattice K x y →
       leq-Large-Suplattice L
         ( map-hom-Large-Suplattice x)
         ( map-hom-Large-Suplattice y)
-    preserves-order-map-hom-Large-Suplattice =
+    preserves-order-hom-Large-Suplattice =
       preserves-order-hom-Large-Poset
         ( large-poset-Large-Suplattice K)
         ( large-poset-Large-Suplattice L)
diff --git a/src/order-theory/inflationary-maps-posets.lagda.md b/src/order-theory/inflationary-maps-posets.lagda.md
new file mode 100644
index 0000000000..d6e25e7dbf
--- /dev/null
+++ b/src/order-theory/inflationary-maps-posets.lagda.md
@@ -0,0 +1,145 @@
+# Inflationary maps on a poset
+
+```agda
+module order-theory.inflationary-maps-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.inflationary-maps-preorders
+open import order-theory.order-preserving-maps-posets
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be an
+{{#concept "inflationary map" Disambiguation="poset" Agda=inflationary-map-Poset}} if the inequality
+
+$$
+  x \leq f(x)
+$$
+
+holds for any element $x : P$. In other words, a map on a poset is inflationary precisely when the map on its underlying [preorder](order-theory.preorders.md) is [inflationary](order-theory.inflationary-maps-preorders.md). If $f$ is also [order preserving](order-theory.order-preserving-maps-posets.md) we say that $f$ is an {{#concept "inflationary morphism" Disambiguation="poset" Agda=inflationary-hom-Poset}}.
+
+## Definitions
+
+### The predicate of being an inflationary map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : type-Poset P → type-Poset P)
+  where
+
+  is-inflationary-prop-map-Poset :
+    Prop (l1 ⊔ l2)
+  is-inflationary-prop-map-Poset =
+    is-inflationary-prop-map-Preorder (preorder-Poset P) f
+
+  is-inflationary-map-Poset :
+    UU (l1 ⊔ l2)
+  is-inflationary-map-Poset =
+    is-inflationary-map-Preorder (preorder-Poset P) f
+
+  is-prop-is-inflationary-map-Poset :
+    is-prop is-inflationary-map-Poset
+  is-prop-is-inflationary-map-Poset =
+    is-prop-is-inflationary-map-Preorder (preorder-Poset P) f
+```
+
+### The type of inflationary maps on a poset
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  inflationary-map-Poset :
+    UU (l1 ⊔ l2)
+  inflationary-map-Poset =
+    inflationary-map-Preorder (preorder-Poset P)
+
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : inflationary-map-Poset P)
+  where
+
+  map-inflationary-map-Poset :
+    type-Poset P → type-Poset P
+  map-inflationary-map-Poset =
+    map-inflationary-map-Preorder (preorder-Poset P) f
+
+  is-inflationary-inflationary-map-Poset :
+    is-inflationary-map-Poset P map-inflationary-map-Poset
+  is-inflationary-inflationary-map-Poset =
+    is-inflationary-inflationary-map-Preorder (preorder-Poset P) f
+```
+
+### The predicate on order preserving maps of being inflationary
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : hom-Poset P P)
+  where
+
+  is-inflationary-prop-hom-Poset : Prop (l1 ⊔ l2)
+  is-inflationary-prop-hom-Poset =
+    is-inflationary-prop-hom-Preorder (preorder-Poset P) f
+
+  is-inflationary-hom-Poset : UU (l1 ⊔ l2)
+  is-inflationary-hom-Poset =
+    is-inflationary-hom-Preorder (preorder-Poset P) f
+
+  is-prop-is-inflationary-hom-Poset :
+    is-prop is-inflationary-hom-Poset
+  is-prop-is-inflationary-hom-Poset =
+    is-prop-is-inflationary-hom-Preorder (preorder-Poset P) f
+```
+
+### The type of inflationary morphisms on a poset
+
+```agda
+module _
+  {l1 l2 : Level} (P : Poset l1 l2)
+  where
+
+  inflationary-hom-Poset : UU (l1 ⊔ l2)
+  inflationary-hom-Poset =
+    inflationary-hom-Preorder (preorder-Poset P)
+
+module _
+  {l1 l2 : Level} (P : Poset l1 l2) (f : inflationary-hom-Poset P)
+  where
+
+  hom-inflationary-hom-Poset :
+    hom-Poset P P
+  hom-inflationary-hom-Poset =
+    hom-inflationary-hom-Preorder (preorder-Poset P) f
+
+  map-inflationary-hom-Poset :
+    type-Poset P → type-Poset P
+  map-inflationary-hom-Poset =
+    map-inflationary-hom-Preorder (preorder-Poset P) f
+
+  preserves-order-inflationary-hom-Poset :
+    preserves-order-Poset P P map-inflationary-hom-Poset
+  preserves-order-inflationary-hom-Poset =
+    preserves-order-inflationary-hom-Preorder (preorder-Poset P) f
+
+  is-inflationary-inflationary-hom-Poset :
+    is-inflationary-map-Poset P map-inflationary-hom-Poset
+  is-inflationary-inflationary-hom-Poset =
+    is-inflationary-inflationary-hom-Preorder (preorder-Poset P) f
+
+  inflationary-map-inflationary-hom-Poset :
+    inflationary-map-Poset P
+  inflationary-map-inflationary-hom-Poset =
+    inflationary-map-inflationary-hom-Preorder (preorder-Poset P) f
+```
diff --git a/src/order-theory/inflationary-maps-preorders.lagda.md b/src/order-theory/inflationary-maps-preorders.lagda.md
new file mode 100644
index 0000000000..a057e74a03
--- /dev/null
+++ b/src/order-theory/inflationary-maps-preorders.lagda.md
@@ -0,0 +1,146 @@
+# Inflationary maps on a preorder
+
+```agda
+module order-theory.inflationary-maps-preorders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-preorders
+open import order-theory.preorders
+```
+
+</details>
+
+## Idea
+
+A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be an
+{{#concept "inflationary map" Disambiguation="preorder" Agda=inflationary-map-Preorder}} if the inequality
+
+$$
+  x \leq f(x)
+$$
+
+holds for any element $x : P$. If $f$ is also [order preserving](order-theory.order-preserving-maps-preorders.md) we say that $f$ is an {{#concept "inflationary morphism" Disambiguation="preorder" Agda=inflationary-hom-Preorder}}.
+
+## Definitions
+
+### The predicate of being an inflationary map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : type-Preorder P → type-Preorder P)
+  where
+
+  is-inflationary-prop-map-Preorder :
+    Prop (l1 ⊔ l2)
+  is-inflationary-prop-map-Preorder =
+    Π-Prop (type-Preorder P) (λ x → leq-prop-Preorder P x (f x))
+
+  is-inflationary-map-Preorder :
+    UU (l1 ⊔ l2)
+  is-inflationary-map-Preorder =
+    type-Prop is-inflationary-prop-map-Preorder
+
+  is-prop-is-inflationary-map-Preorder :
+    is-prop is-inflationary-map-Preorder
+  is-prop-is-inflationary-map-Preorder =
+    is-prop-type-Prop is-inflationary-prop-map-Preorder
+```
+
+### The type of inflationary maps on a preorder
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2)
+  where
+
+  inflationary-map-Preorder :
+    UU (l1 ⊔ l2)
+  inflationary-map-Preorder =
+    type-subtype (is-inflationary-prop-map-Preorder P)
+
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : inflationary-map-Preorder P)
+  where
+
+  map-inflationary-map-Preorder :
+    type-Preorder P → type-Preorder P
+  map-inflationary-map-Preorder =
+    pr1 f
+
+  is-inflationary-inflationary-map-Preorder :
+    is-inflationary-map-Preorder P map-inflationary-map-Preorder
+  is-inflationary-inflationary-map-Preorder =
+    pr2 f
+```
+
+### The predicate on order preserving maps of being inflationary
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : hom-Preorder P P)
+  where
+
+  is-inflationary-prop-hom-Preorder : Prop (l1 ⊔ l2)
+  is-inflationary-prop-hom-Preorder =
+    is-inflationary-prop-map-Preorder P (map-hom-Preorder P P f)
+
+  is-inflationary-hom-Preorder : UU (l1 ⊔ l2)
+  is-inflationary-hom-Preorder =
+    is-inflationary-map-Preorder P (map-hom-Preorder P P f)
+
+  is-prop-is-inflationary-hom-Preorder :
+    is-prop is-inflationary-hom-Preorder
+  is-prop-is-inflationary-hom-Preorder =
+    is-prop-is-inflationary-map-Preorder P (map-hom-Preorder P P f)
+```
+
+### The type of inflationary morphisms on a preorder
+
+```agda
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2)
+  where
+
+  inflationary-hom-Preorder : UU (l1 ⊔ l2)
+  inflationary-hom-Preorder =
+    type-subtype (is-inflationary-prop-hom-Preorder P)
+
+module _
+  {l1 l2 : Level} (P : Preorder l1 l2) (f : inflationary-hom-Preorder P)
+  where
+
+  hom-inflationary-hom-Preorder :
+    hom-Preorder P P
+  hom-inflationary-hom-Preorder =
+    pr1 f
+
+  map-inflationary-hom-Preorder :
+    type-Preorder P → type-Preorder P
+  map-inflationary-hom-Preorder =
+    map-hom-Preorder P P hom-inflationary-hom-Preorder
+
+  preserves-order-inflationary-hom-Preorder :
+    preserves-order-Preorder P P map-inflationary-hom-Preorder
+  preserves-order-inflationary-hom-Preorder =
+    preserves-order-hom-Preorder P P hom-inflationary-hom-Preorder
+
+  is-inflationary-inflationary-hom-Preorder :
+    is-inflationary-map-Preorder P map-inflationary-hom-Preorder
+  is-inflationary-inflationary-hom-Preorder =
+    pr2 f
+
+  inflationary-map-inflationary-hom-Preorder :
+    inflationary-map-Preorder P
+  pr1 inflationary-map-inflationary-hom-Preorder =
+    map-inflationary-hom-Preorder
+  pr2 inflationary-map-inflationary-hom-Preorder =
+    is-inflationary-inflationary-hom-Preorder
+```
diff --git a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
new file mode 100644
index 0000000000..069d80d2c3
--- /dev/null
+++ b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
@@ -0,0 +1,162 @@
+# Inflationary maps on a strictly ordered type
+
+```agda
+module order-theory.inflationary-maps-strictly-ordered-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.strict-order-preserving-maps
+open import order-theory.strictly-ordered-types
+```
+
+</details>
+
+## Idea
+
+A map $f : P → P$ on a [strictly ordered type](order-theory.strictly-ordered-types.md) $P$ is said to be an
+{{#concept "inflationary map" Disambiguation="strictly ordered type" Agda=inflationary-map-Strictly-Ordered-Type}} if the inequality
+
+$$
+  x < f(x)
+$$
+
+holds for any element $x : P$. If $f$ is also [order preserving](order-theory.order-preserving-maps-strictly-ordered-types.md) we say that $f$ is an {{#concept "inflationary morphism" Disambiguation="strictly ordered type" Agda=inflationary-hom-Strictly-Ordered-Type}}.
+
+## Definitions
+
+### The predicate of being an inflationary map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
+  (f : type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type P)
+  where
+
+  is-inflationary-prop-map-Strictly-Ordered-Type :
+    Prop (l1 ⊔ l2)
+  is-inflationary-prop-map-Strictly-Ordered-Type =
+    Π-Prop
+      ( type-Strictly-Ordered-Type P)
+      ( λ x → le-prop-Strictly-Ordered-Type P x (f x))
+
+  is-inflationary-map-Strictly-Ordered-Type :
+    UU (l1 ⊔ l2)
+  is-inflationary-map-Strictly-Ordered-Type =
+    type-Prop is-inflationary-prop-map-Strictly-Ordered-Type
+
+  is-prop-is-inflationary-map-Strictly-Ordered-Type :
+    is-prop is-inflationary-map-Strictly-Ordered-Type
+  is-prop-is-inflationary-map-Strictly-Ordered-Type =
+    is-prop-type-Prop is-inflationary-prop-map-Strictly-Ordered-Type
+```
+
+### The type of inflationary maps on a strictly ordered type
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
+  where
+
+  inflationary-map-Strictly-Ordered-Type :
+    UU (l1 ⊔ l2)
+  inflationary-map-Strictly-Ordered-Type =
+    type-subtype (is-inflationary-prop-map-Strictly-Ordered-Type P)
+
+module _
+  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
+  (f : inflationary-map-Strictly-Ordered-Type P)
+  where
+
+  map-inflationary-map-Strictly-Ordered-Type :
+    type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type P
+  map-inflationary-map-Strictly-Ordered-Type =
+    pr1 f
+
+  is-inflationary-inflationary-map-Strictly-Ordered-Type :
+    is-inflationary-map-Strictly-Ordered-Type P
+      ( map-inflationary-map-Strictly-Ordered-Type)
+  is-inflationary-inflationary-map-Strictly-Ordered-Type =
+    pr2 f
+```
+
+### The predicate on order preserving maps of being inflationary
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
+  (f : hom-Strictly-Ordered-Type P P)
+  where
+
+  is-inflationary-prop-hom-Strictly-Ordered-Type :
+    Prop (l1 ⊔ l2)
+  is-inflationary-prop-hom-Strictly-Ordered-Type =
+    is-inflationary-prop-map-Strictly-Ordered-Type P
+      ( map-hom-Strictly-Ordered-Type P P f)
+
+  is-inflationary-hom-Strictly-Ordered-Type :
+    UU (l1 ⊔ l2)
+  is-inflationary-hom-Strictly-Ordered-Type =
+    is-inflationary-map-Strictly-Ordered-Type P
+      ( map-hom-Strictly-Ordered-Type P P f)
+
+  is-prop-is-inflationary-hom-Strictly-Ordered-Type :
+    is-prop is-inflationary-hom-Strictly-Ordered-Type
+  is-prop-is-inflationary-hom-Strictly-Ordered-Type =
+    is-prop-is-inflationary-map-Strictly-Ordered-Type P
+      ( map-hom-Strictly-Ordered-Type P P f)
+```
+
+### The type of inflationary morphisms on a strictly ordered type
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
+  where
+
+  inflationary-hom-Strictly-Ordered-Type :
+    UU (l1 ⊔ l2)
+  inflationary-hom-Strictly-Ordered-Type =
+    type-subtype (is-inflationary-prop-hom-Strictly-Ordered-Type P)
+
+module _
+  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
+  (f : inflationary-hom-Strictly-Ordered-Type P)
+  where
+
+  hom-inflationary-hom-Strictly-Ordered-Type :
+    hom-Strictly-Ordered-Type P P
+  hom-inflationary-hom-Strictly-Ordered-Type =
+    pr1 f
+
+  map-inflationary-hom-Strictly-Ordered-Type :
+    type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type P
+  map-inflationary-hom-Strictly-Ordered-Type =
+    map-hom-Strictly-Ordered-Type P P hom-inflationary-hom-Strictly-Ordered-Type
+
+  preserves-order-inflationary-hom-Strictly-Ordered-Type :
+    preserves-strict-order-map-Strictly-Ordered-Type P P
+      ( map-inflationary-hom-Strictly-Ordered-Type)
+  preserves-order-inflationary-hom-Strictly-Ordered-Type =
+    preserves-strict-order-hom-Strictly-Ordered-Type P P
+      ( hom-inflationary-hom-Strictly-Ordered-Type)
+
+  is-inflationary-inflationary-hom-Strictly-Ordered-Type :
+    is-inflationary-map-Strictly-Ordered-Type P
+      ( map-inflationary-hom-Strictly-Ordered-Type)
+  is-inflationary-inflationary-hom-Strictly-Ordered-Type =
+    pr2 f
+
+  inflationary-map-inflationary-hom-Strictly-Ordered-Type :
+    inflationary-map-Strictly-Ordered-Type P
+  pr1 inflationary-map-inflationary-hom-Strictly-Ordered-Type =
+    map-inflationary-hom-Strictly-Ordered-Type
+  pr2 inflationary-map-inflationary-hom-Strictly-Ordered-Type =
+    is-inflationary-inflationary-hom-Strictly-Ordered-Type
+```
diff --git a/src/order-theory/opposite-preorders.lagda.md b/src/order-theory/opposite-preorders.lagda.md
index 39c2c42ec0..2e6db98be2 100644
--- a/src/order-theory/opposite-preorders.lagda.md
+++ b/src/order-theory/opposite-preorders.lagda.md
@@ -80,7 +80,7 @@ module _
     hom-Preorder (opposite-Preorder P) (opposite-Preorder Q)
   opposite-hom-Preorder f =
     ( map-hom-Preorder P Q f) ,
-    ( λ x y p → preserves-order-map-hom-Preorder P Q f y x p)
+    ( λ x y p → preserves-order-hom-Preorder P Q f y x p)
 ```
 
 ## Properties
diff --git a/src/order-theory/order-preserving-maps-posets.lagda.md b/src/order-theory/order-preserving-maps-posets.lagda.md
index 077313f75b..163aee3f3f 100644
--- a/src/order-theory/order-preserving-maps-posets.lagda.md
+++ b/src/order-theory/order-preserving-maps-posets.lagda.md
@@ -64,10 +64,10 @@ module _
   map-hom-Poset : hom-Poset → type-Poset P → type-Poset Q
   map-hom-Poset = map-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
 
-  preserves-order-map-hom-Poset :
+  preserves-order-hom-Poset :
     (f : hom-Poset) → preserves-order-Poset (map-hom-Poset f)
-  preserves-order-map-hom-Poset =
-    preserves-order-map-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
+  preserves-order-hom-Poset =
+    preserves-order-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
 ```
 
 ### Homotopies of order preserving maps
diff --git a/src/order-theory/order-preserving-maps-preorders.lagda.md b/src/order-theory/order-preserving-maps-preorders.lagda.md
index d3bf16d8ee..a45df09656 100644
--- a/src/order-theory/order-preserving-maps-preorders.lagda.md
+++ b/src/order-theory/order-preserving-maps-preorders.lagda.md
@@ -28,21 +28,24 @@ open import order-theory.preorders
 
 ## Idea
 
-A map `f : P → Q` between the underlying types of two preorders is said to be
-**order preserving** if `x ≤ y` in `P` implies `f x ≤ f y` in `Q`.
+A map `f : P → Q` between the underlying types of two
+[preorders](order-theory.preorders.md) is said to be an
+{{#concept "order preserving map" Disambiguation="preorder" Agda=hom-Preorder}}
+if for any two elements `x ≤ y` in `P` we have `f x ≤ f y` in `Q`.
 
 ## Definition
 
-### Order preserving maps
+### The predicate of being an order preserving map
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4)
+  (f : type-Preorder P → type-Preorder Q)
   where
 
   preserves-order-prop-Preorder :
-    (type-Preorder P → type-Preorder Q) → Prop (l1 ⊔ l2 ⊔ l4)
-  preserves-order-prop-Preorder f =
+    Prop (l1 ⊔ l2 ⊔ l4)
+  preserves-order-prop-Preorder =
     Π-Prop
       ( type-Preorder P)
       ( λ x →
@@ -54,26 +57,37 @@ module _
               ( leq-prop-Preorder Q (f x) (f y))))
 
   preserves-order-Preorder :
-    (type-Preorder P → type-Preorder Q) → UU (l1 ⊔ l2 ⊔ l4)
-  preserves-order-Preorder f =
-    type-Prop (preserves-order-prop-Preorder f)
+    UU (l1 ⊔ l2 ⊔ l4)
+  preserves-order-Preorder =
+    type-Prop preserves-order-prop-Preorder
 
   is-prop-preserves-order-Preorder :
-    (f : type-Preorder P → type-Preorder Q) →
-    is-prop (preserves-order-Preorder f)
-  is-prop-preserves-order-Preorder f =
-    is-prop-type-Prop (preserves-order-prop-Preorder f)
+    is-prop preserves-order-Preorder
+  is-prop-preserves-order-Preorder =
+    is-prop-type-Prop preserves-order-prop-Preorder
+```
+
+### The type of order preserving maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4)
+  where
 
-  hom-Preorder : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-Preorder :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   hom-Preorder =
-    Σ (type-Preorder P → type-Preorder Q) preserves-order-Preorder
+    Σ (type-Preorder P → type-Preorder Q) (preserves-order-Preorder P Q)
 
-  map-hom-Preorder : hom-Preorder → type-Preorder P → type-Preorder Q
-  map-hom-Preorder = pr1
+  map-hom-Preorder :
+    hom-Preorder → type-Preorder P → type-Preorder Q
+  map-hom-Preorder =
+    pr1
 
-  preserves-order-map-hom-Preorder :
-    (f : hom-Preorder) → preserves-order-Preorder (map-hom-Preorder f)
-  preserves-order-map-hom-Preorder = pr2
+  preserves-order-hom-Preorder :
+    (f : hom-Preorder) → preserves-order-Preorder P Q (map-hom-Preorder f)
+  preserves-order-hom-Preorder =
+    pr2
 ```
 
 ### Homotopies of order preserving maps
@@ -101,7 +115,7 @@ module _
       ( is-prop-preserves-order-Preorder P Q)
       ( map-hom-Preorder P Q f)
       ( refl-htpy)
-      ( preserves-order-map-hom-Preorder P Q f)
+      ( preserves-order-hom-Preorder P Q f)
 
   is-equiv-htpy-eq-hom-Preorder :
     (f g : hom-Preorder P Q) → is-equiv (htpy-eq-hom-Preorder f g)
@@ -150,10 +164,10 @@ module _
     preserves-order-Preorder P R
       ( map-hom-Preorder Q R g ∘ map-hom-Preorder P Q f)
   preserves-order-comp-Preorder g f x y H =
-    preserves-order-map-hom-Preorder Q R g
+    preserves-order-hom-Preorder Q R g
       ( map-hom-Preorder P Q f x)
       ( map-hom-Preorder P Q f y)
-      ( preserves-order-map-hom-Preorder P Q f x y H)
+      ( preserves-order-hom-Preorder P Q f x y H)
 
   comp-hom-Preorder :
     (g : hom-Preorder Q R) (f : hom-Preorder P Q) →
diff --git a/src/order-theory/strict-order-preserving-maps.lagda.md b/src/order-theory/strict-order-preserving-maps.lagda.md
new file mode 100644
index 0000000000..0b8e200905
--- /dev/null
+++ b/src/order-theory/strict-order-preserving-maps.lagda.md
@@ -0,0 +1,153 @@
+# Strict order preserving maps
+
+```agda
+module order-theory.strict-order-preserving-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.strictly-ordered-sets
+open import order-theory.strictly-ordered-types
+```
+
+</details>
+
+## Idea
+
+Consider two [strictly ordered types](order-theory.strictly-ordered-types.md) $P$ and $Q$, with orderings $<_P$ and $<_Q$ respectively. A {{#concept "strict order preserving map" Agda=hom-Strictly-Ordered-Type}} consists of map $f : P → Q$ between their underlying types such that for any two elements $x<_P y$ in $P$ we have $f(x)<_Q f(y)$ in $Q$.
+
+## Definitions
+
+### The predicate on maps between strictly ordered types of preserving the strict ordering
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strictly-Ordered-Type l1 l2) (Q : Strictly-Ordered-Type l3 l4)
+  (f : type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type Q)
+  where
+
+  preserves-strict-order-prop-map-Strictly-Ordered-Type :
+    Prop (l1 ⊔ l2 ⊔ l4)
+  preserves-strict-order-prop-map-Strictly-Ordered-Type =
+    Π-Prop
+      ( type-Strictly-Ordered-Type P)
+      ( λ x →
+        Π-Prop
+          ( type-Strictly-Ordered-Type P)
+          ( λ y →
+            hom-Prop
+              ( le-prop-Strictly-Ordered-Type P x y)
+              ( le-prop-Strictly-Ordered-Type Q (f x) (f y))))
+
+  preserves-strict-order-map-Strictly-Ordered-Type :
+    UU (l1 ⊔ l2 ⊔ l4)
+  preserves-strict-order-map-Strictly-Ordered-Type =
+    type-Prop preserves-strict-order-prop-map-Strictly-Ordered-Type
+
+  is-prop-preserves-strict-order-map-Strictly-Ordered-Type :
+    is-prop preserves-strict-order-map-Strictly-Ordered-Type
+  is-prop-preserves-strict-order-map-Strictly-Ordered-Type =
+    is-prop-type-Prop preserves-strict-order-prop-map-Strictly-Ordered-Type
+```
+
+### The type of strict order preserving maps between strictly ordered types
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strictly-Ordered-Type l1 l2) (Q : Strictly-Ordered-Type l3 l4)
+  where
+
+  hom-Strictly-Ordered-Type : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-Strictly-Ordered-Type =
+    type-subtype (preserves-strict-order-prop-map-Strictly-Ordered-Type P Q)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strictly-Ordered-Type l1 l2) (Q : Strictly-Ordered-Type l3 l4)
+  (f : hom-Strictly-Ordered-Type P Q)
+  where
+
+  map-hom-Strictly-Ordered-Type :
+    type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type Q
+  map-hom-Strictly-Ordered-Type =
+    pr1 f
+
+  preserves-strict-order-hom-Strictly-Ordered-Type :
+    preserves-strict-order-map-Strictly-Ordered-Type P Q
+      ( map-hom-Strictly-Ordered-Type)
+  preserves-strict-order-hom-Strictly-Ordered-Type =
+    pr2 f
+```
+
+### The predicate on maps between strictly ordered sets of preserving the strict ordering
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strictly-Ordered-Set l1 l2) (Q : Strictly-Ordered-Set l3 l4)
+  (f : type-Strictly-Ordered-Set P → type-Strictly-Ordered-Set Q)
+  where
+
+  preserves-strict-order-prop-map-Strictly-Ordered-Set :
+    Prop (l1 ⊔ l2 ⊔ l4)
+  preserves-strict-order-prop-map-Strictly-Ordered-Set =
+    preserves-strict-order-prop-map-Strictly-Ordered-Type
+      ( strictly-ordered-type-Strictly-Ordered-Set P)
+      ( strictly-ordered-type-Strictly-Ordered-Set Q)
+      ( f)
+
+  preserves-strict-order-map-Strictly-Ordered-Set :
+    UU (l1 ⊔ l2 ⊔ l4)
+  preserves-strict-order-map-Strictly-Ordered-Set =
+    preserves-strict-order-map-Strictly-Ordered-Type
+      ( strictly-ordered-type-Strictly-Ordered-Set P)
+      ( strictly-ordered-type-Strictly-Ordered-Set Q)
+      ( f)
+
+  is-prop-preserves-strict-order-map-Strictly-Ordered-Set :
+    is-prop preserves-strict-order-map-Strictly-Ordered-Set
+  is-prop-preserves-strict-order-map-Strictly-Ordered-Set =
+    is-prop-preserves-strict-order-map-Strictly-Ordered-Type
+      ( strictly-ordered-type-Strictly-Ordered-Set P)
+      ( strictly-ordered-type-Strictly-Ordered-Set Q)
+      ( f)
+```
+
+### The type of strict order preserving maps between strictly ordered sets
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strictly-Ordered-Set l1 l2) (Q : Strictly-Ordered-Set l3 l4)
+  where
+
+  hom-Strictly-Ordered-Set : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-Strictly-Ordered-Set =
+    type-subtype (preserves-strict-order-prop-map-Strictly-Ordered-Set P Q)
+
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strictly-Ordered-Set l1 l2) (Q : Strictly-Ordered-Set l3 l4)
+  (f : hom-Strictly-Ordered-Set P Q)
+  where
+
+  map-hom-Strictly-Ordered-Set :
+    type-Strictly-Ordered-Set P → type-Strictly-Ordered-Set Q
+  map-hom-Strictly-Ordered-Set =
+    pr1 f
+
+  preserves-strict-order-hom-Strictly-Ordered-Set :
+    preserves-strict-order-map-Strictly-Ordered-Set P Q
+      ( map-hom-Strictly-Ordered-Set)
+  preserves-strict-order-hom-Strictly-Ordered-Set =
+    pr2 f
+```
diff --git a/src/order-theory/strictly-ordered-sets.lagda.md b/src/order-theory/strictly-ordered-sets.lagda.md
new file mode 100644
index 0000000000..f53b3caf1d
--- /dev/null
+++ b/src/order-theory/strictly-ordered-sets.lagda.md
@@ -0,0 +1,115 @@
+# Strictly ordered sets
+
+```agda
+module order-theory.strictly-ordered-sets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import order-theory.strictly-ordered-types
+```
+
+</details>
+
+## Idea
+
+A {{#concept "strictly ordered set" Agda=Strictly-Ordered-Set}} is a [strictly ordered type](order-theory.strictly-ordered-types.md) whose underlying type is a [set](foundation-core.sets.md). More specifically, a strictly ordered set consists of a set $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the [propositions](foundation-core.propositions.md), such that the relation $<$ is {{#concept "irreflexive"}} and transitive:
+
+- For any $x:A$ we have $x \nle x$.
+- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
+
+Strictly ordered sets satisfy antisymmetry by irreflexivity and transitivity.
+
+## Definitions
+
+### The type of strictly ordered sets
+
+```agda
+Strictly-Ordered-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Strictly-Ordered-Set l1 l2 =
+  Σ ( Set l1)
+    ( λ A →
+      Σ ( Relation-Prop l2 (type-Set A))
+        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
+
+module _
+  {l1 l2 : Level} (A : Strictly-Ordered-Set l1 l2)
+  where
+
+  set-Strictly-Ordered-Set :
+    Set l1
+  set-Strictly-Ordered-Set =
+    pr1 A
+
+  type-Strictly-Ordered-Set :
+    UU l1
+  type-Strictly-Ordered-Set =
+    type-Set set-Strictly-Ordered-Set
+
+  is-set-type-Strictly-Ordered-Set :
+    is-set type-Strictly-Ordered-Set
+  is-set-type-Strictly-Ordered-Set =
+    is-set-type-Set set-Strictly-Ordered-Set
+
+  le-prop-Strictly-Ordered-Set :
+    Relation-Prop l2 type-Strictly-Ordered-Set
+  le-prop-Strictly-Ordered-Set =
+    pr1 (pr2 A)
+
+  le-Strictly-Ordered-Set :
+    Relation l2 type-Strictly-Ordered-Set
+  le-Strictly-Ordered-Set =
+    type-Relation-Prop le-prop-Strictly-Ordered-Set
+
+  is-prop-le-Strictly-Ordered-Set :
+    (x y : type-Strictly-Ordered-Set) → is-prop (le-Strictly-Ordered-Set x y)
+  is-prop-le-Strictly-Ordered-Set =
+    is-prop-type-Relation-Prop le-prop-Strictly-Ordered-Set
+
+  is-irreflexive-le-Strictly-Ordered-Set :
+    is-irreflexive le-Strictly-Ordered-Set
+  is-irreflexive-le-Strictly-Ordered-Set =
+    pr1 (pr2 (pr2 A))
+
+  is-transitive-le-Strictly-Ordered-Set :
+    is-transitive le-Strictly-Ordered-Set
+  is-transitive-le-Strictly-Ordered-Set =
+    pr2 (pr2 (pr2 A))
+
+  strictly-ordered-type-Strictly-Ordered-Set :
+    Strictly-Ordered-Type l1 l2
+  pr1 strictly-ordered-type-Strictly-Ordered-Set =
+    type-Strictly-Ordered-Set
+  pr1 (pr2 strictly-ordered-type-Strictly-Ordered-Set) =
+    le-prop-Strictly-Ordered-Set
+  pr1 (pr2 (pr2 strictly-ordered-type-Strictly-Ordered-Set)) =
+    is-irreflexive-le-Strictly-Ordered-Set
+  pr2 (pr2 (pr2 strictly-ordered-type-Strictly-Ordered-Set)) =
+    is-transitive-le-Strictly-Ordered-Set
+```
+
+## Properties
+
+### The ordering of a strictly ordered set is antisymmetric
+
+```agda
+module _
+  {l1 l2 : Level} (A : Strictly-Ordered-Set l1 l2)
+  where
+
+  is-antisymmetric-le-Strictly-Ordered-Set :
+    is-antisymmetric (le-Strictly-Ordered-Set A)
+  is-antisymmetric-le-Strictly-Ordered-Set =
+    is-antisymmetric-le-Strictly-Ordered-Type
+      ( strictly-ordered-type-Strictly-Ordered-Set A)
+```
diff --git a/src/order-theory/strictly-ordered-types.lagda.md b/src/order-theory/strictly-ordered-types.lagda.md
new file mode 100644
index 0000000000..84388b0843
--- /dev/null
+++ b/src/order-theory/strictly-ordered-types.lagda.md
@@ -0,0 +1,92 @@
+# Strictly ordered types
+
+```agda
+module order-theory.strictly-ordered-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "strictly ordered type" Agda=Strictly-Ordered-Type}} consists of a type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the [propositions](foundation-core.propositions.md), such that the relation $<$ is {{#concept "irreflexive"}} and transitive:
+
+- For any $x:A$ we have $x \nle x$.
+- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
+
+Strictly ordered types satisfy antisymmetry by irreflexivity and transitivity.
+
+## Definitions
+
+### The type of strictly ordered types
+
+```agda
+Strictly-Ordered-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Strictly-Ordered-Type l1 l2 =
+  Σ ( UU l1)
+    ( λ A →
+      Σ ( Relation-Prop l2 A)
+        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
+
+module _
+  {l1 l2 : Level} (A : Strictly-Ordered-Type l1 l2)
+  where
+
+  type-Strictly-Ordered-Type :
+    UU l1
+  type-Strictly-Ordered-Type =
+    pr1 A
+
+  le-prop-Strictly-Ordered-Type :
+    Relation-Prop l2 type-Strictly-Ordered-Type
+  le-prop-Strictly-Ordered-Type =
+    pr1 (pr2 A)
+
+  le-Strictly-Ordered-Type :
+    Relation l2 type-Strictly-Ordered-Type
+  le-Strictly-Ordered-Type =
+    type-Relation-Prop le-prop-Strictly-Ordered-Type
+
+  is-prop-le-Strictly-Ordered-Type :
+    (x y : type-Strictly-Ordered-Type) → is-prop (le-Strictly-Ordered-Type x y)
+  is-prop-le-Strictly-Ordered-Type =
+    is-prop-type-Relation-Prop le-prop-Strictly-Ordered-Type
+
+  is-irreflexive-le-Strictly-Ordered-Type :
+    is-irreflexive le-Strictly-Ordered-Type
+  is-irreflexive-le-Strictly-Ordered-Type =
+    pr1 (pr2 (pr2 A))
+
+  is-transitive-le-Strictly-Ordered-Type :
+    is-transitive le-Strictly-Ordered-Type
+  is-transitive-le-Strictly-Ordered-Type =
+    pr2 (pr2 (pr2 A))
+```
+
+## Properties
+
+### The ordering of a strictly ordered type is antisymmetric
+
+```agda
+module _
+  {l1 l2 : Level} (A : Strictly-Ordered-Type l1 l2)
+  where
+
+  is-antisymmetric-le-Strictly-Ordered-Type :
+    is-antisymmetric (le-Strictly-Ordered-Type A)
+  is-antisymmetric-le-Strictly-Ordered-Type x y H K =
+    ex-falso
+      ( is-irreflexive-le-Strictly-Ordered-Type A x
+        ( is-transitive-le-Strictly-Ordered-Type A x y x K H))
+```

From 67de13605f6cf14284b595f90b505df7ebab0911 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 13:55:47 -0500
Subject: [PATCH 02/17] make pre-commit

---
 src/order-theory.lagda.md                            |  8 ++++++++
 src/order-theory/deflationary-maps-posets.lagda.md   | 10 ++++++++--
 .../deflationary-maps-preorders.lagda.md             | 11 ++++++++---
 src/order-theory/inflationary-maps-posets.lagda.md   | 10 ++++++++--
 .../inflationary-maps-preorders.lagda.md             | 11 ++++++++---
 ...inflationary-maps-strictly-ordered-types.lagda.md | 12 +++++++++---
 .../strict-order-preserving-maps.lagda.md            |  6 +++++-
 src/order-theory/strictly-ordered-sets.lagda.md      |  7 ++++++-
 src/order-theory/strictly-ordered-types.lagda.md     |  5 ++++-
 9 files changed, 64 insertions(+), 16 deletions(-)

diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index a5f5985c0f..c4df760010 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -22,6 +22,8 @@ open import order-theory.decidable-subposets public
 open import order-theory.decidable-subpreorders public
 open import order-theory.decidable-total-orders public
 open import order-theory.decidable-total-preorders public
+open import order-theory.deflationary-maps-posets public
+open import order-theory.deflationary-maps-preorders public
 open import order-theory.dependent-products-large-frames public
 open import order-theory.dependent-products-large-locales public
 open import order-theory.dependent-products-large-meet-semilattices public
@@ -49,6 +51,9 @@ open import order-theory.homomorphisms-meet-suplattices public
 open import order-theory.homomorphisms-suplattices public
 open import order-theory.ideals-preorders public
 open import order-theory.incidence-algebras public
+open import order-theory.inflationary-maps-posets public
+open import order-theory.inflationary-maps-preorders public
+open import order-theory.inflationary-maps-strictly-ordered-types public
 open import order-theory.inflattices public
 open import order-theory.inhabited-chains-posets public
 open import order-theory.inhabited-chains-preorders public
@@ -111,6 +116,9 @@ open import order-theory.similarity-of-elements-large-posets public
 open import order-theory.similarity-of-elements-large-preorders public
 open import order-theory.similarity-of-order-preserving-maps-large-posets public
 open import order-theory.similarity-of-order-preserving-maps-large-preorders public
+open import order-theory.strict-order-preserving-maps public
+open import order-theory.strictly-ordered-sets public
+open import order-theory.strictly-ordered-types public
 open import order-theory.subposets public
 open import order-theory.subpreorders public
 open import order-theory.suplattices public
diff --git a/src/order-theory/deflationary-maps-posets.lagda.md b/src/order-theory/deflationary-maps-posets.lagda.md
index e765e77437..ab536c12ab 100644
--- a/src/order-theory/deflationary-maps-posets.lagda.md
+++ b/src/order-theory/deflationary-maps-posets.lagda.md
@@ -22,13 +22,19 @@ open import order-theory.posets
 ## Idea
 
 A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be an
-{{#concept "deflationary map" Disambiguation="poset" Agda=deflationary-map-Poset}} if the inequality
+{{#concept "deflationary map" Disambiguation="poset" Agda=deflationary-map-Poset}}
+if the inequality
 
 $$
   f(x) \leq x
 $$
 
-holds for any element $x : P$. In other words, a map on a poset is deflationary precisely when the map on its underlying [preorder](order-theory.preorders.md) is [deflationary](order-theory.deflationary-maps-preorders.md). If $f$ is also [order preserving](order-theory.order-preserving-maps-posets.md) we say that $f$ is an {{#concept "deflationary morphism" Disambiguation="poset" Agda=deflationary-hom-Poset}}.
+holds for any element $x : P$. In other words, a map on a poset is deflationary
+precisely when the map on its underlying [preorder](order-theory.preorders.md)
+is [deflationary](order-theory.deflationary-maps-preorders.md). If $f$ is also
+[order preserving](order-theory.order-preserving-maps-posets.md) we say that $f$
+is an
+{{#concept "deflationary morphism" Disambiguation="poset" Agda=deflationary-hom-Poset}}.
 
 ## Definitions
 
diff --git a/src/order-theory/deflationary-maps-preorders.lagda.md b/src/order-theory/deflationary-maps-preorders.lagda.md
index 0368370cb8..977aabcc51 100644
--- a/src/order-theory/deflationary-maps-preorders.lagda.md
+++ b/src/order-theory/deflationary-maps-preorders.lagda.md
@@ -20,14 +20,19 @@ open import order-theory.preorders
 
 ## Idea
 
-A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be an
-{{#concept "deflationary map" Disambiguation="preorder" Agda=deflationary-map-Preorder}} if the inequality
+A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be
+an
+{{#concept "deflationary map" Disambiguation="preorder" Agda=deflationary-map-Preorder}}
+if the inequality
 
 $$
   f(x) \leq x
 $$
 
-holds for any element $x : P$. If $f$ is also [order preserving](order-theory.order-preserving-maps-preorders.md) we say that $f$ is an {{#concept "deflationary morphism" Disambiguation="preorder" Agda=deflationary-hom-Preorder}}.
+holds for any element $x : P$. If $f$ is also
+[order preserving](order-theory.order-preserving-maps-preorders.md) we say that
+$f$ is an
+{{#concept "deflationary morphism" Disambiguation="preorder" Agda=deflationary-hom-Preorder}}.
 
 ## Definitions
 
diff --git a/src/order-theory/inflationary-maps-posets.lagda.md b/src/order-theory/inflationary-maps-posets.lagda.md
index d6e25e7dbf..2a8ee69fcf 100644
--- a/src/order-theory/inflationary-maps-posets.lagda.md
+++ b/src/order-theory/inflationary-maps-posets.lagda.md
@@ -22,13 +22,19 @@ open import order-theory.posets
 ## Idea
 
 A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be an
-{{#concept "inflationary map" Disambiguation="poset" Agda=inflationary-map-Poset}} if the inequality
+{{#concept "inflationary map" Disambiguation="poset" Agda=inflationary-map-Poset}}
+if the inequality
 
 $$
   x \leq f(x)
 $$
 
-holds for any element $x : P$. In other words, a map on a poset is inflationary precisely when the map on its underlying [preorder](order-theory.preorders.md) is [inflationary](order-theory.inflationary-maps-preorders.md). If $f$ is also [order preserving](order-theory.order-preserving-maps-posets.md) we say that $f$ is an {{#concept "inflationary morphism" Disambiguation="poset" Agda=inflationary-hom-Poset}}.
+holds for any element $x : P$. In other words, a map on a poset is inflationary
+precisely when the map on its underlying [preorder](order-theory.preorders.md)
+is [inflationary](order-theory.inflationary-maps-preorders.md). If $f$ is also
+[order preserving](order-theory.order-preserving-maps-posets.md) we say that $f$
+is an
+{{#concept "inflationary morphism" Disambiguation="poset" Agda=inflationary-hom-Poset}}.
 
 ## Definitions
 
diff --git a/src/order-theory/inflationary-maps-preorders.lagda.md b/src/order-theory/inflationary-maps-preorders.lagda.md
index a057e74a03..87d1fdd8c2 100644
--- a/src/order-theory/inflationary-maps-preorders.lagda.md
+++ b/src/order-theory/inflationary-maps-preorders.lagda.md
@@ -20,14 +20,19 @@ open import order-theory.preorders
 
 ## Idea
 
-A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be an
-{{#concept "inflationary map" Disambiguation="preorder" Agda=inflationary-map-Preorder}} if the inequality
+A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be
+an
+{{#concept "inflationary map" Disambiguation="preorder" Agda=inflationary-map-Preorder}}
+if the inequality
 
 $$
   x \leq f(x)
 $$
 
-holds for any element $x : P$. If $f$ is also [order preserving](order-theory.order-preserving-maps-preorders.md) we say that $f$ is an {{#concept "inflationary morphism" Disambiguation="preorder" Agda=inflationary-hom-Preorder}}.
+holds for any element $x : P$. If $f$ is also
+[order preserving](order-theory.order-preserving-maps-preorders.md) we say that
+$f$ is an
+{{#concept "inflationary morphism" Disambiguation="preorder" Agda=inflationary-hom-Preorder}}.
 
 ## Definitions
 
diff --git a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
index 069d80d2c3..b47ed3f7a4 100644
--- a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
+++ b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
@@ -20,14 +20,20 @@ open import order-theory.strictly-ordered-types
 
 ## Idea
 
-A map $f : P → P$ on a [strictly ordered type](order-theory.strictly-ordered-types.md) $P$ is said to be an
-{{#concept "inflationary map" Disambiguation="strictly ordered type" Agda=inflationary-map-Strictly-Ordered-Type}} if the inequality
+A map $f : P → P$ on a
+[strictly ordered type](order-theory.strictly-ordered-types.md) $P$ is said to
+be an
+{{#concept "inflationary map" Disambiguation="strictly ordered type" Agda=inflationary-map-Strictly-Ordered-Type}}
+if the inequality
 
 $$
   x < f(x)
 $$
 
-holds for any element $x : P$. If $f$ is also [order preserving](order-theory.order-preserving-maps-strictly-ordered-types.md) we say that $f$ is an {{#concept "inflationary morphism" Disambiguation="strictly ordered type" Agda=inflationary-hom-Strictly-Ordered-Type}}.
+holds for any element $x : P$. If $f$ is also
+[order preserving](order-theory.order-preserving-maps-strictly-ordered-types.md)
+we say that $f$ is an
+{{#concept "inflationary morphism" Disambiguation="strictly ordered type" Agda=inflationary-hom-Strictly-Ordered-Type}}.
 
 ## Definitions
 
diff --git a/src/order-theory/strict-order-preserving-maps.lagda.md b/src/order-theory/strict-order-preserving-maps.lagda.md
index 0b8e200905..913acce6c2 100644
--- a/src/order-theory/strict-order-preserving-maps.lagda.md
+++ b/src/order-theory/strict-order-preserving-maps.lagda.md
@@ -21,7 +21,11 @@ open import order-theory.strictly-ordered-types
 
 ## Idea
 
-Consider two [strictly ordered types](order-theory.strictly-ordered-types.md) $P$ and $Q$, with orderings $<_P$ and $<_Q$ respectively. A {{#concept "strict order preserving map" Agda=hom-Strictly-Ordered-Type}} consists of map $f : P → Q$ between their underlying types such that for any two elements $x<_P y$ in $P$ we have $f(x)<_Q f(y)$ in $Q$.
+Consider two [strictly ordered types](order-theory.strictly-ordered-types.md)
+$P$ and $Q$, with orderings $<_P$ and $<_Q$ respectively. A
+{{#concept "strict order preserving map" Agda=hom-Strictly-Ordered-Type}}
+consists of map $f : P → Q$ between their underlying types such that for any two
+elements $x<_P y$ in $P$ we have $f(x)<_Q f(y)$ in $Q$.
 
 ## Definitions
 
diff --git a/src/order-theory/strictly-ordered-sets.lagda.md b/src/order-theory/strictly-ordered-sets.lagda.md
index f53b3caf1d..3710758984 100644
--- a/src/order-theory/strictly-ordered-sets.lagda.md
+++ b/src/order-theory/strictly-ordered-sets.lagda.md
@@ -23,7 +23,12 @@ open import order-theory.strictly-ordered-types
 
 ## Idea
 
-A {{#concept "strictly ordered set" Agda=Strictly-Ordered-Set}} is a [strictly ordered type](order-theory.strictly-ordered-types.md) whose underlying type is a [set](foundation-core.sets.md). More specifically, a strictly ordered set consists of a set $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the [propositions](foundation-core.propositions.md), such that the relation $<$ is {{#concept "irreflexive"}} and transitive:
+A {{#concept "strictly ordered set" Agda=Strictly-Ordered-Set}} is a
+[strictly ordered type](order-theory.strictly-ordered-types.md) whose underlying
+type is a [set](foundation-core.sets.md). More specifically, a strictly ordered
+set consists of a set $A$, a [binary relation](foundation.binary-relations.md)
+$<$ on $A$ valued in the [propositions](foundation-core.propositions.md), such
+that the relation $<$ is {{#concept "irreflexive"}} and transitive:
 
 - For any $x:A$ we have $x \nle x$.
 - For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
diff --git a/src/order-theory/strictly-ordered-types.lagda.md b/src/order-theory/strictly-ordered-types.lagda.md
index 84388b0843..d0ddaef694 100644
--- a/src/order-theory/strictly-ordered-types.lagda.md
+++ b/src/order-theory/strictly-ordered-types.lagda.md
@@ -20,7 +20,10 @@ open import foundation.universe-levels
 
 ## Idea
 
-A {{#concept "strictly ordered type" Agda=Strictly-Ordered-Type}} consists of a type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the [propositions](foundation-core.propositions.md), such that the relation $<$ is {{#concept "irreflexive"}} and transitive:
+A {{#concept "strictly ordered type" Agda=Strictly-Ordered-Type}} consists of a
+type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued
+in the [propositions](foundation-core.propositions.md), such that the relation
+$<$ is {{#concept "irreflexive"}} and transitive:
 
 - For any $x:A$ we have $x \nle x$.
 - For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.

From c902276464e0e12a830fa75abe6ed6cc01d0d1f5 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 13:59:56 -0500
Subject: [PATCH 03/17] typo

---
 src/domain-theory/directed-families-posets.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/domain-theory/directed-families-posets.lagda.md b/src/domain-theory/directed-families-posets.lagda.md
index 2684d639aa..0b192c1b84 100644
--- a/src/domain-theory/directed-families-posets.lagda.md
+++ b/src/domain-theory/directed-families-posets.lagda.md
@@ -138,11 +138,11 @@ module _
         ( exists-structure-Prop type-directed-family-hom-Poset _)
         ( λ z y →
           intro-exists z
-            ( preserves-order-map-hom-Poset P Q f
+            ( preserves-order-hom-Poset P Q f
                 ( family-directed-family-Poset P x u)
                 ( family-directed-family-Poset P x z)
                 ( pr1 y) ,
-              preserves-order-map-hom-Poset P Q f
+              preserves-order-hom-Poset P Q f
                 ( family-directed-family-Poset P x v)
                 ( family-directed-family-Poset P x z)
                 ( pr2 y)))

From ded18986de3949fe49e07d8b05f52c85e691ef6e Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 14:15:15 -0500
Subject: [PATCH 04/17] strict orders

---
 src/foundation/binary-relations.lagda.md | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md
index e4fe8d4600..b9ad577958 100644
--- a/src/foundation/binary-relations.lagda.md
+++ b/src/foundation/binary-relations.lagda.md
@@ -21,6 +21,7 @@ open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.negation
 open import foundation-core.propositions
+open import foundation-core.sets
 open import foundation-core.torsorial-type-families
 ```
 
@@ -191,7 +192,14 @@ module _
   where
 
   is-irreflexive : UU (l1 ⊔ l2)
-  is-irreflexive = (x : A) → ¬ (R x x)
+  is-irreflexive = (x : A) → ¬ R x x
+
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-irreflexive-Relation-Prop : UU (l1 ⊔ l2)
+  is-irreflexive-Relation-Prop = is-irreflexive (type-Relation-Prop R)
 ```
 
 ### The predicate of being an asymmetric relation

From 78f3838ce5e7641c6e0a4fa12d6b8f0e5fe714c9 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 14:20:24 -0500
Subject: [PATCH 05/17] put min/max back

---
 .../decidable-total-orders.lagda.md           | 169 ++++++++++++++++++
 1 file changed, 169 insertions(+)

diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md
index 2aeb739708..1bd894c446 100644
--- a/src/order-theory/decidable-total-orders.lagda.md
+++ b/src/order-theory/decidable-total-orders.lagda.md
@@ -11,6 +11,7 @@ open import foundation.binary-relations
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
+open import foundation.empty-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
@@ -18,6 +19,8 @@ open import foundation.universe-levels
 
 open import order-theory.decidable-posets
 open import order-theory.decidable-total-preorders
+open import order-theory.greatest-lower-bounds-posets
+open import order-theory.least-upper-bounds-posets
 open import order-theory.posets
 open import order-theory.preorders
 open import order-theory.total-orders
@@ -181,3 +184,169 @@ module _
   set-Decidable-Total-Order : Set l1
   set-Decidable-Total-Order = set-Poset poset-Decidable-Total-Order
 ```
+
+## Properties
+
+### Any two elements in a decidable total order have a minimum and maximum
+
+```agda
+module _
+  {l1 l2 : Level}
+  (T : Decidable-Total-Order l1 l2)
+  (x y : type-Decidable-Total-Order T)
+  where
+
+  min-Decidable-Total-Order : type-Decidable-Total-Order T
+  min-Decidable-Total-Order =
+    rec-coproduct
+      ( λ x≤y → x)
+      ( λ y<x → y)
+      ( is-leq-or-strict-greater-Decidable-Total-Order T x y)
+
+  max-Decidable-Total-Order : type-Decidable-Total-Order T
+  max-Decidable-Total-Order =
+    rec-coproduct
+      ( λ x≤y → y)
+      ( λ y<x → x)
+      ( is-leq-or-strict-greater-Decidable-Total-Order T x y)
+```
+
+### The minimum is a lower bound
+
+```agda
+  leq-left-min-Decidable-Total-Order :
+    leq-Decidable-Total-Order T min-Decidable-Total-Order x
+  leq-left-min-Decidable-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = refl-leq-Decidable-Total-Order T x
+  ... | inr y<x = pr2 y<x
+
+  leq-right-min-Decidable-Total-Order :
+    leq-Decidable-Total-Order T min-Decidable-Total-Order y
+  leq-right-min-Decidable-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = x≤y
+  ... | inr y<x = refl-leq-Decidable-Total-Order T y
+```
+
+### The maximum of two values is an upper bound
+
+```agda
+  leq-left-max-Decidable-Total-Order :
+    leq-Decidable-Total-Order T x max-Decidable-Total-Order
+  leq-left-max-Decidable-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = x≤y
+  ... | inr y<x = refl-leq-Decidable-Total-Order T x
+
+  leq-right-max-Decidable-Total-Order :
+    leq-Decidable-Total-Order T y max-Decidable-Total-Order
+  leq-right-max-Decidable-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = refl-leq-Decidable-Total-Order T y
+  ... | inr y<x = pr2 y<x
+```
+
+### The minimum operation is commutative
+
+```agda
+module _
+  {l1 l2 : Level}
+  (T : Decidable-Total-Order l1 l2)
+  (x y : type-Decidable-Total-Order T)
+  where
+
+  commutative-min-Decidable-Total-Order :
+    min-Decidable-Total-Order T x y ＝ min-Decidable-Total-Order T y x
+  commutative-min-Decidable-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+          | is-leq-or-strict-greater-Decidable-Total-Order T y x
+  ... | inl x≤y | inl y≤x =
+    antisymmetric-leq-Decidable-Total-Order T x y x≤y y≤x
+  ... | inl x≤y | inr x<y = refl
+  ... | inr y<x | inl y≤x = refl
+  ... | inr y<x | inr x<y =
+    ex-falso
+      (pr1
+        ( x<y)
+        ( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
+```
+
+### The maximum operation is commutative
+
+```agda
+  commutative-max-Decidable-Total-Order :
+    max-Decidable-Total-Order T x y ＝ max-Decidable-Total-Order T y x
+  commutative-max-Decidable-Total-Order
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+          | is-leq-or-strict-greater-Decidable-Total-Order T y x
+  ... | inl x≤y | inl y≤x =
+    antisymmetric-leq-Decidable-Total-Order T y x y≤x x≤y
+  ... | inl x≤y | inr x<y = refl
+  ... | inr y<x | inl y≤x = refl
+  ... | inr y<x | inr x<y =
+    ex-falso
+      (pr1
+        ( x<y)
+        ( antisymmetric-leq-Decidable-Total-Order T x y (pr2 x<y) (pr2 y<x)))
+```
+
+### The minimum of two values is their greatest lower bound
+
+```agda
+  min-is-greatest-binary-lower-bound-Decidable-Total-Order :
+    is-greatest-binary-lower-bound-Poset
+      ( poset-Decidable-Total-Order T)
+      ( x)
+      ( y)
+      ( min-Decidable-Total-Order T x y)
+  pr1 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) (z≤x , z≤y)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = z≤x
+  ... | inr y<x = z≤y
+  pr1 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = z≤min
+  ... | inr y<x = transitive-leq-Decidable-Total-Order T z y x (pr2 y<x) z≤min
+  pr2 (pr2 (min-is-greatest-binary-lower-bound-Decidable-Total-Order z) z≤min)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = transitive-leq-Decidable-Total-Order T z x y x≤y z≤min
+  ... | inr y<x = z≤min
+
+  has-greatest-binary-lower-bound-Decidable-Total-Order :
+    has-greatest-binary-lower-bound-Poset (poset-Decidable-Total-Order T) x y
+  pr1 has-greatest-binary-lower-bound-Decidable-Total-Order =
+    min-Decidable-Total-Order T x y
+  pr2 has-greatest-binary-lower-bound-Decidable-Total-Order =
+    min-is-greatest-binary-lower-bound-Decidable-Total-Order
+```
+
+### The maximum of two values is their least upper bound
+
+```agda
+  max-is-least-binary-upper-bound-Decidable-Total-Order :
+    is-least-binary-upper-bound-Poset
+      ( poset-Decidable-Total-Order T)
+      ( x)
+      ( y)
+      ( max-Decidable-Total-Order T x y)
+  pr1 (max-is-least-binary-upper-bound-Decidable-Total-Order z) (x≤z , y≤z)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = y≤z
+  ... | inr y<x = x≤z
+  pr1 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = transitive-leq-Decidable-Total-Order T x y z min≤z x≤y
+  ... | inr y<x = min≤z
+  pr2 (pr2 (max-is-least-binary-upper-bound-Decidable-Total-Order z) min≤z)
+    with is-leq-or-strict-greater-Decidable-Total-Order T x y
+  ... | inl x≤y = min≤z
+  ... | inr y<x = transitive-leq-Decidable-Total-Order T y x z min≤z (pr2 y<x)
+
+  has-least-binary-upper-bound-Decidable-Total-Order :
+    has-least-binary-upper-bound-Poset (poset-Decidable-Total-Order T) x y
+  pr1 has-least-binary-upper-bound-Decidable-Total-Order =
+    max-Decidable-Total-Order T x y
+  pr2 has-least-binary-upper-bound-Decidable-Total-Order =
+    max-is-least-binary-upper-bound-Decidable-Total-Order
+```

From a2b6844fbbed8d57c41cf2bbb7054d67fe1e62f3 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 14:40:33 -0500
Subject: [PATCH 06/17] fix broken link

---
 .../inflationary-maps-strictly-ordered-types.lagda.md           | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
index b47ed3f7a4..7c05eeee54 100644
--- a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
+++ b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
@@ -31,7 +31,7 @@ $$
 $$
 
 holds for any element $x : P$. If $f$ is also
-[order preserving](order-theory.order-preserving-maps-strictly-ordered-types.md)
+[order preserving](order-theory.strict-order-preserving-maps.md)
 we say that $f$ is an
 {{#concept "inflationary morphism" Disambiguation="strictly ordered type" Agda=inflationary-hom-Strictly-Ordered-Type}}.
 

From 3f5a8d1cf6af34086db6641e15d6d2cee12534d4 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 15:08:48 -0500
Subject: [PATCH 07/17] make pre-commit

---
 .../inflationary-maps-strictly-ordered-types.lagda.md         | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
index 7c05eeee54..aaeb02fb60 100644
--- a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
+++ b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
@@ -31,8 +31,8 @@ $$
 $$
 
 holds for any element $x : P$. If $f$ is also
-[order preserving](order-theory.strict-order-preserving-maps.md)
-we say that $f$ is an
+[order preserving](order-theory.strict-order-preserving-maps.md) we say that $f$
+is an
 {{#concept "inflationary morphism" Disambiguation="strictly ordered type" Agda=inflationary-hom-Strictly-Ordered-Type}}.
 
 ## Definitions

From 812a6c6d3ece44f4faaac9a64b4249a6d0008005 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 15:34:09 -0500
Subject: [PATCH 08/17] indefinite articles

---
 src/order-theory/deflationary-maps-posets.lagda.md    | 6 +++---
 src/order-theory/deflationary-maps-preorders.lagda.md | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/order-theory/deflationary-maps-posets.lagda.md b/src/order-theory/deflationary-maps-posets.lagda.md
index ab536c12ab..a78f2bf619 100644
--- a/src/order-theory/deflationary-maps-posets.lagda.md
+++ b/src/order-theory/deflationary-maps-posets.lagda.md
@@ -21,7 +21,7 @@ open import order-theory.posets
 
 ## Idea
 
-A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be an
+A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be a
 {{#concept "deflationary map" Disambiguation="poset" Agda=deflationary-map-Poset}}
 if the inequality
 
@@ -33,12 +33,12 @@ holds for any element $x : P$. In other words, a map on a poset is deflationary
 precisely when the map on its underlying [preorder](order-theory.preorders.md)
 is [deflationary](order-theory.deflationary-maps-preorders.md). If $f$ is also
 [order preserving](order-theory.order-preserving-maps-posets.md) we say that $f$
-is an
+is a
 {{#concept "deflationary morphism" Disambiguation="poset" Agda=deflationary-hom-Poset}}.
 
 ## Definitions
 
-### The predicate of being an deflationary map
+### The predicate of being a deflationary map
 
 ```agda
 module _
diff --git a/src/order-theory/deflationary-maps-preorders.lagda.md b/src/order-theory/deflationary-maps-preorders.lagda.md
index 977aabcc51..7376940889 100644
--- a/src/order-theory/deflationary-maps-preorders.lagda.md
+++ b/src/order-theory/deflationary-maps-preorders.lagda.md
@@ -21,7 +21,7 @@ open import order-theory.preorders
 ## Idea
 
 A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be
-an
+a
 {{#concept "deflationary map" Disambiguation="preorder" Agda=deflationary-map-Preorder}}
 if the inequality
 
@@ -31,12 +31,12 @@ $$
 
 holds for any element $x : P$. If $f$ is also
 [order preserving](order-theory.order-preserving-maps-preorders.md) we say that
-$f$ is an
+$f$ is a
 {{#concept "deflationary morphism" Disambiguation="preorder" Agda=deflationary-hom-Preorder}}.
 
 ## Definitions
 
-### The predicate of being an deflationary map
+### The predicate of being a deflationary map
 
 ```agda
 module _

From 219e07b021a87ae165298898c96fe1c8bc6875ca Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 15:35:38 -0500
Subject: [PATCH 09/17] make pre-commit

---
 src/order-theory/deflationary-maps-preorders.lagda.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/order-theory/deflationary-maps-preorders.lagda.md b/src/order-theory/deflationary-maps-preorders.lagda.md
index 7376940889..e0da17ee5d 100644
--- a/src/order-theory/deflationary-maps-preorders.lagda.md
+++ b/src/order-theory/deflationary-maps-preorders.lagda.md
@@ -20,8 +20,7 @@ open import order-theory.preorders
 
 ## Idea
 
-A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be
-a
+A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be a
 {{#concept "deflationary map" Disambiguation="preorder" Agda=deflationary-map-Preorder}}
 if the inequality
 

From f10692a34fe7577571c4943a365b2aee0b0ea07f Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 15:57:41 -0500
Subject: [PATCH 10/17] \leq

---
 src/order-theory/deflationary-maps-posets.lagda.md    | 2 +-
 src/order-theory/deflationary-maps-preorders.lagda.md | 2 +-
 src/order-theory/inflationary-maps-posets.lagda.md    | 2 +-
 src/order-theory/inflationary-maps-preorders.lagda.md | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/order-theory/deflationary-maps-posets.lagda.md b/src/order-theory/deflationary-maps-posets.lagda.md
index a78f2bf619..ffeb8f4da5 100644
--- a/src/order-theory/deflationary-maps-posets.lagda.md
+++ b/src/order-theory/deflationary-maps-posets.lagda.md
@@ -26,7 +26,7 @@ A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be a
 if the inequality
 
 $$
-  f(x) \leq x
+  f(x) ≤ x
 $$
 
 holds for any element $x : P$. In other words, a map on a poset is deflationary
diff --git a/src/order-theory/deflationary-maps-preorders.lagda.md b/src/order-theory/deflationary-maps-preorders.lagda.md
index e0da17ee5d..508b702878 100644
--- a/src/order-theory/deflationary-maps-preorders.lagda.md
+++ b/src/order-theory/deflationary-maps-preorders.lagda.md
@@ -25,7 +25,7 @@ A map $f : P → P$ on a [preorder](order-theory.preorders.md) $P$ is said to be
 if the inequality
 
 $$
-  f(x) \leq x
+  f(x) ≤ x
 $$
 
 holds for any element $x : P$. If $f$ is also
diff --git a/src/order-theory/inflationary-maps-posets.lagda.md b/src/order-theory/inflationary-maps-posets.lagda.md
index 2a8ee69fcf..00c3374a3b 100644
--- a/src/order-theory/inflationary-maps-posets.lagda.md
+++ b/src/order-theory/inflationary-maps-posets.lagda.md
@@ -26,7 +26,7 @@ A map $f : P → P$ on a [poset](order-theory.posets.md) $P$ is said to be an
 if the inequality
 
 $$
-  x \leq f(x)
+  x ≤ f(x)
 $$
 
 holds for any element $x : P$. In other words, a map on a poset is inflationary
diff --git a/src/order-theory/inflationary-maps-preorders.lagda.md b/src/order-theory/inflationary-maps-preorders.lagda.md
index 87d1fdd8c2..aa2d482b97 100644
--- a/src/order-theory/inflationary-maps-preorders.lagda.md
+++ b/src/order-theory/inflationary-maps-preorders.lagda.md
@@ -26,7 +26,7 @@ an
 if the inequality
 
 $$
-  x \leq f(x)
+  x ≤ f(x)
 $$
 
 holds for any element $x : P$. If $f$ is also

From c17b41cb21b2578367ccd0478772484cad1916e7 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 16:04:27 -0500
Subject: [PATCH 11/17] name changes

---
 src/elementary-number-theory.lagda.md         |   2 +-
 ...-ordered-pairs-of-natural-numbers.lagda.md |  50 +++---
 src/foundation/repetitions-sequences.lagda.md |   8 +-
 src/order-theory.lagda.md                     |   6 +-
 ...onary-maps-strictly-ordered-types.lagda.md | 168 ------------------
 ...ry-maps-strictly-preordered-types.lagda.md | 168 ++++++++++++++++++
 .../strict-order-preserving-maps.lagda.md     | 137 +++++++-------
 .../strictly-ordered-sets.lagda.md            | 120 -------------
 .../strictly-ordered-types.lagda.md           |  95 ----------
 .../strictly-preordered-sets.lagda.md         | 121 +++++++++++++
 .../strictly-preordered-types.lagda.md        |  96 ++++++++++
 11 files changed, 487 insertions(+), 484 deletions(-)
 delete mode 100644 src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
 create mode 100644 src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
 delete mode 100644 src/order-theory/strictly-ordered-sets.lagda.md
 delete mode 100644 src/order-theory/strictly-ordered-types.lagda.md
 create mode 100644 src/order-theory/strictly-preordered-sets.lagda.md
 create mode 100644 src/order-theory/strictly-preordered-types.lagda.md

diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index befe9c31fc..2c044fc6b3 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -161,7 +161,7 @@ open import elementary-number-theory.strict-inequality-integers public
 open import elementary-number-theory.strict-inequality-natural-numbers public
 open import elementary-number-theory.strict-inequality-rational-numbers public
 open import elementary-number-theory.strict-inequality-standard-finite-types public
-open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
+open import elementary-number-theory.strictly-preordered-pairs-of-natural-numbers public
 open import elementary-number-theory.strong-induction-natural-numbers public
 open import elementary-number-theory.sums-of-natural-numbers public
 open import elementary-number-theory.sylvesters-sequence public
diff --git a/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md b/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
index faab496e28..4c9cec59c8 100644
--- a/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
@@ -1,7 +1,7 @@
 # Strictly ordered pairs of natural numbers
 
 ```agda
-module elementary-number-theory.strictly-ordered-pairs-of-natural-numbers where
+module elementary-number-theory.strictly-preordered-pairs-of-natural-numbers where
 ```
 
 <details><summary>Imports</summary>
@@ -32,22 +32,22 @@ A strictly ordered pair of natural numbers consists of `x y : ℕ` such that
 ## Definition
 
 ```agda
-strictly-ordered-pair-ℕ : UU lzero
-strictly-ordered-pair-ℕ = Σ ℕ (λ x → Σ ℕ (λ y → le-ℕ x y))
+strictly-preordered-pair-ℕ : UU lzero
+strictly-preordered-pair-ℕ = Σ ℕ (λ x → Σ ℕ (λ y → le-ℕ x y))
 
 module _
-  (p : strictly-ordered-pair-ℕ)
+  (p : strictly-preordered-pair-ℕ)
   where
 
-  first-strictly-ordered-pair-ℕ : ℕ
-  first-strictly-ordered-pair-ℕ = pr1 p
+  first-strictly-preordered-pair-ℕ : ℕ
+  first-strictly-preordered-pair-ℕ = pr1 p
 
-  second-strictly-ordered-pair-ℕ : ℕ
-  second-strictly-ordered-pair-ℕ = pr1 (pr2 p)
+  second-strictly-preordered-pair-ℕ : ℕ
+  second-strictly-preordered-pair-ℕ = pr1 (pr2 p)
 
-  strict-inequality-strictly-ordered-pair-ℕ :
-    le-ℕ first-strictly-ordered-pair-ℕ second-strictly-ordered-pair-ℕ
-  strict-inequality-strictly-ordered-pair-ℕ = pr2 (pr2 p)
+  strict-inequality-strictly-preordered-pair-ℕ :
+    le-ℕ first-strictly-preordered-pair-ℕ second-strictly-preordered-pair-ℕ
+  strict-inequality-strictly-preordered-pair-ℕ = pr2 (pr2 p)
 ```
 
 ## Properties
@@ -55,34 +55,34 @@ module _
 ### Strictly ordered pairs of natural numbers are pairs of distinct elements
 
 ```agda
-pair-of-distinct-elements-strictly-ordered-pair-ℕ :
-  strictly-ordered-pair-ℕ → pair-of-distinct-elements ℕ
-pair-of-distinct-elements-strictly-ordered-pair-ℕ (a , b , H) =
+pair-of-distinct-elements-strictly-preordered-pair-ℕ :
+  strictly-preordered-pair-ℕ → pair-of-distinct-elements ℕ
+pair-of-distinct-elements-strictly-preordered-pair-ℕ (a , b , H) =
   (a , b , neq-le-ℕ H)
 ```
 
 ### Any pair of distinct elements of natural numbers can be strictly ordered
 
 ```agda
-strictly-ordered-pair-pair-of-distinct-elements-ℕ' :
-  (a b : ℕ) → a ≠ b → strictly-ordered-pair-ℕ
-strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ zero-ℕ H =
+strictly-preordered-pair-pair-of-distinct-elements-ℕ' :
+  (a b : ℕ) → a ≠ b → strictly-preordered-pair-ℕ
+strictly-preordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ zero-ℕ H =
   ex-falso (H refl)
-strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ (succ-ℕ b) H =
+strictly-preordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ (succ-ℕ b) H =
   (0 , succ-ℕ b , star)
-strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) zero-ℕ H =
+strictly-preordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) zero-ℕ H =
   (0 , succ-ℕ a , star)
-strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) (succ-ℕ b) H =
+strictly-preordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) (succ-ℕ b) H =
   map-Σ
     ( λ x → Σ ℕ (λ y → le-ℕ x y))
     ( succ-ℕ)
     ( λ x →
       map-Σ (le-ℕ (succ-ℕ x)) succ-ℕ (λ y → id))
-    ( strictly-ordered-pair-pair-of-distinct-elements-ℕ' a b
+    ( strictly-preordered-pair-pair-of-distinct-elements-ℕ' a b
       ( λ p → H (ap succ-ℕ p)))
 
-strictly-ordered-pair-pair-of-distinct-elements-ℕ :
-  pair-of-distinct-elements ℕ → strictly-ordered-pair-ℕ
-strictly-ordered-pair-pair-of-distinct-elements-ℕ (a , b , H) =
-  strictly-ordered-pair-pair-of-distinct-elements-ℕ' a b H
+strictly-preordered-pair-pair-of-distinct-elements-ℕ :
+  pair-of-distinct-elements ℕ → strictly-preordered-pair-ℕ
+strictly-preordered-pair-pair-of-distinct-elements-ℕ (a , b , H) =
+  strictly-preordered-pair-pair-of-distinct-elements-ℕ' a b H
 ```
diff --git a/src/foundation/repetitions-sequences.lagda.md b/src/foundation/repetitions-sequences.lagda.md
index c52b33a71d..1d7a764730 100644
--- a/src/foundation/repetitions-sequences.lagda.md
+++ b/src/foundation/repetitions-sequences.lagda.md
@@ -8,7 +8,7 @@ module foundation.repetitions-sequences where
 
 ```agda
 open import elementary-number-theory.natural-numbers
-open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers
+open import elementary-number-theory.strictly-preordered-pairs-of-natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
@@ -84,14 +84,14 @@ module _
 
 ```agda
 is-ordered-repetition-of-values-ℕ :
-  {l1 : Level} {A : UU l1} (f : ℕ → A) (x : strictly-ordered-pair-ℕ) → UU l1
+  {l1 : Level} {A : UU l1} (f : ℕ → A) (x : strictly-preordered-pair-ℕ) → UU l1
 is-ordered-repetition-of-values-ℕ f x =
-  f (first-strictly-ordered-pair-ℕ x) ＝ f (second-strictly-ordered-pair-ℕ x)
+  f (first-strictly-preordered-pair-ℕ x) ＝ f (second-strictly-preordered-pair-ℕ x)
 
 ordered-repetition-of-values-ℕ :
   {l1 : Level} {A : UU l1} (f : ℕ → A) → UU l1
 ordered-repetition-of-values-ℕ f =
-  Σ strictly-ordered-pair-ℕ (is-ordered-repetition-of-values-ℕ f)
+  Σ strictly-preordered-pair-ℕ (is-ordered-repetition-of-values-ℕ f)
 
 ordered-repetition-of-values-comp-ℕ :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : A → B) {f : ℕ → A} →
diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index c4df760010..a1e9bc7fd1 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -53,7 +53,7 @@ open import order-theory.ideals-preorders public
 open import order-theory.incidence-algebras public
 open import order-theory.inflationary-maps-posets public
 open import order-theory.inflationary-maps-preorders public
-open import order-theory.inflationary-maps-strictly-ordered-types public
+open import order-theory.inflationary-maps-strictly-preordered-types public
 open import order-theory.inflattices public
 open import order-theory.inhabited-chains-posets public
 open import order-theory.inhabited-chains-preorders public
@@ -117,8 +117,8 @@ open import order-theory.similarity-of-elements-large-preorders public
 open import order-theory.similarity-of-order-preserving-maps-large-posets public
 open import order-theory.similarity-of-order-preserving-maps-large-preorders public
 open import order-theory.strict-order-preserving-maps public
-open import order-theory.strictly-ordered-sets public
-open import order-theory.strictly-ordered-types public
+open import order-theory.strictly-preordered-sets public
+open import order-theory.strictly-preordered-types public
 open import order-theory.subposets public
 open import order-theory.subpreorders public
 open import order-theory.suplattices public
diff --git a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md b/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
deleted file mode 100644
index aaeb02fb60..0000000000
--- a/src/order-theory/inflationary-maps-strictly-ordered-types.lagda.md
+++ /dev/null
@@ -1,168 +0,0 @@
-# Inflationary maps on a strictly ordered type
-
-```agda
-module order-theory.inflationary-maps-strictly-ordered-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.dependent-pair-types
-open import foundation.propositions
-open import foundation.subtypes
-open import foundation.universe-levels
-
-open import order-theory.strict-order-preserving-maps
-open import order-theory.strictly-ordered-types
-```
-
-</details>
-
-## Idea
-
-A map $f : P → P$ on a
-[strictly ordered type](order-theory.strictly-ordered-types.md) $P$ is said to
-be an
-{{#concept "inflationary map" Disambiguation="strictly ordered type" Agda=inflationary-map-Strictly-Ordered-Type}}
-if the inequality
-
-$$
-  x < f(x)
-$$
-
-holds for any element $x : P$. If $f$ is also
-[order preserving](order-theory.strict-order-preserving-maps.md) we say that $f$
-is an
-{{#concept "inflationary morphism" Disambiguation="strictly ordered type" Agda=inflationary-hom-Strictly-Ordered-Type}}.
-
-## Definitions
-
-### The predicate of being an inflationary map
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
-  (f : type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type P)
-  where
-
-  is-inflationary-prop-map-Strictly-Ordered-Type :
-    Prop (l1 ⊔ l2)
-  is-inflationary-prop-map-Strictly-Ordered-Type =
-    Π-Prop
-      ( type-Strictly-Ordered-Type P)
-      ( λ x → le-prop-Strictly-Ordered-Type P x (f x))
-
-  is-inflationary-map-Strictly-Ordered-Type :
-    UU (l1 ⊔ l2)
-  is-inflationary-map-Strictly-Ordered-Type =
-    type-Prop is-inflationary-prop-map-Strictly-Ordered-Type
-
-  is-prop-is-inflationary-map-Strictly-Ordered-Type :
-    is-prop is-inflationary-map-Strictly-Ordered-Type
-  is-prop-is-inflationary-map-Strictly-Ordered-Type =
-    is-prop-type-Prop is-inflationary-prop-map-Strictly-Ordered-Type
-```
-
-### The type of inflationary maps on a strictly ordered type
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
-  where
-
-  inflationary-map-Strictly-Ordered-Type :
-    UU (l1 ⊔ l2)
-  inflationary-map-Strictly-Ordered-Type =
-    type-subtype (is-inflationary-prop-map-Strictly-Ordered-Type P)
-
-module _
-  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
-  (f : inflationary-map-Strictly-Ordered-Type P)
-  where
-
-  map-inflationary-map-Strictly-Ordered-Type :
-    type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type P
-  map-inflationary-map-Strictly-Ordered-Type =
-    pr1 f
-
-  is-inflationary-inflationary-map-Strictly-Ordered-Type :
-    is-inflationary-map-Strictly-Ordered-Type P
-      ( map-inflationary-map-Strictly-Ordered-Type)
-  is-inflationary-inflationary-map-Strictly-Ordered-Type =
-    pr2 f
-```
-
-### The predicate on order preserving maps of being inflationary
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
-  (f : hom-Strictly-Ordered-Type P P)
-  where
-
-  is-inflationary-prop-hom-Strictly-Ordered-Type :
-    Prop (l1 ⊔ l2)
-  is-inflationary-prop-hom-Strictly-Ordered-Type =
-    is-inflationary-prop-map-Strictly-Ordered-Type P
-      ( map-hom-Strictly-Ordered-Type P P f)
-
-  is-inflationary-hom-Strictly-Ordered-Type :
-    UU (l1 ⊔ l2)
-  is-inflationary-hom-Strictly-Ordered-Type =
-    is-inflationary-map-Strictly-Ordered-Type P
-      ( map-hom-Strictly-Ordered-Type P P f)
-
-  is-prop-is-inflationary-hom-Strictly-Ordered-Type :
-    is-prop is-inflationary-hom-Strictly-Ordered-Type
-  is-prop-is-inflationary-hom-Strictly-Ordered-Type =
-    is-prop-is-inflationary-map-Strictly-Ordered-Type P
-      ( map-hom-Strictly-Ordered-Type P P f)
-```
-
-### The type of inflationary morphisms on a strictly ordered type
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
-  where
-
-  inflationary-hom-Strictly-Ordered-Type :
-    UU (l1 ⊔ l2)
-  inflationary-hom-Strictly-Ordered-Type =
-    type-subtype (is-inflationary-prop-hom-Strictly-Ordered-Type P)
-
-module _
-  {l1 l2 : Level} (P : Strictly-Ordered-Type l1 l2)
-  (f : inflationary-hom-Strictly-Ordered-Type P)
-  where
-
-  hom-inflationary-hom-Strictly-Ordered-Type :
-    hom-Strictly-Ordered-Type P P
-  hom-inflationary-hom-Strictly-Ordered-Type =
-    pr1 f
-
-  map-inflationary-hom-Strictly-Ordered-Type :
-    type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type P
-  map-inflationary-hom-Strictly-Ordered-Type =
-    map-hom-Strictly-Ordered-Type P P hom-inflationary-hom-Strictly-Ordered-Type
-
-  preserves-order-inflationary-hom-Strictly-Ordered-Type :
-    preserves-strict-order-map-Strictly-Ordered-Type P P
-      ( map-inflationary-hom-Strictly-Ordered-Type)
-  preserves-order-inflationary-hom-Strictly-Ordered-Type =
-    preserves-strict-order-hom-Strictly-Ordered-Type P P
-      ( hom-inflationary-hom-Strictly-Ordered-Type)
-
-  is-inflationary-inflationary-hom-Strictly-Ordered-Type :
-    is-inflationary-map-Strictly-Ordered-Type P
-      ( map-inflationary-hom-Strictly-Ordered-Type)
-  is-inflationary-inflationary-hom-Strictly-Ordered-Type =
-    pr2 f
-
-  inflationary-map-inflationary-hom-Strictly-Ordered-Type :
-    inflationary-map-Strictly-Ordered-Type P
-  pr1 inflationary-map-inflationary-hom-Strictly-Ordered-Type =
-    map-inflationary-hom-Strictly-Ordered-Type
-  pr2 inflationary-map-inflationary-hom-Strictly-Ordered-Type =
-    is-inflationary-inflationary-hom-Strictly-Ordered-Type
-```
diff --git a/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md b/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
new file mode 100644
index 0000000000..2bbcbfe244
--- /dev/null
+++ b/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
@@ -0,0 +1,168 @@
+# Inflationary maps on a strictly preordered type
+
+```agda
+module order-theory.inflationary-maps-strictly-preordered-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.strict-order-preserving-maps
+open import order-theory.strictly-preordered-types
+```
+
+</details>
+
+## Idea
+
+A map $f : P → P$ on a
+[strictly preordered type](order-theory.strictly-preordered-types.md) $P$ is
+said to be an
+{{#concept "inflationary map" Disambiguation="strictly preordered type" Agda=inflationary-map-Strictly-Preordered-Type}}
+if the inequality
+
+$$
+  x < f(x)
+$$
+
+holds for any element $x : P$. If $f$ is also
+[order preserving](order-theory.strict-order-preserving-maps.md) we say that $f$
+is an
+{{#concept "inflationary morphism" Disambiguation="strictly preordered type" Agda=inflationary-hom-Strictly-Preordered-Type}}.
+
+## Definitions
+
+### The predicate of being an inflationary map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
+  (f : type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P)
+  where
+
+  is-inflationary-prop-map-Strictly-Preordered-Type :
+    Prop (l1 ⊔ l2)
+  is-inflationary-prop-map-Strictly-Preordered-Type =
+    Π-Prop
+      ( type-Strictly-Preordered-Type P)
+      ( λ x → le-prop-Strictly-Preordered-Type P x (f x))
+
+  is-inflationary-map-Strictly-Preordered-Type :
+    UU (l1 ⊔ l2)
+  is-inflationary-map-Strictly-Preordered-Type =
+    type-Prop is-inflationary-prop-map-Strictly-Preordered-Type
+
+  is-prop-is-inflationary-map-Strictly-Preordered-Type :
+    is-prop is-inflationary-map-Strictly-Preordered-Type
+  is-prop-is-inflationary-map-Strictly-Preordered-Type =
+    is-prop-type-Prop is-inflationary-prop-map-Strictly-Preordered-Type
+```
+
+### The type of inflationary maps on a strictly preordered type
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
+  where
+
+  inflationary-map-Strictly-Preordered-Type :
+    UU (l1 ⊔ l2)
+  inflationary-map-Strictly-Preordered-Type =
+    type-subtype (is-inflationary-prop-map-Strictly-Preordered-Type P)
+
+module _
+  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
+  (f : inflationary-map-Strictly-Preordered-Type P)
+  where
+
+  map-inflationary-map-Strictly-Preordered-Type :
+    type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P
+  map-inflationary-map-Strictly-Preordered-Type =
+    pr1 f
+
+  is-inflationary-inflationary-map-Strictly-Preordered-Type :
+    is-inflationary-map-Strictly-Preordered-Type P
+      ( map-inflationary-map-Strictly-Preordered-Type)
+  is-inflationary-inflationary-map-Strictly-Preordered-Type =
+    pr2 f
+```
+
+### The predicate on order preserving maps of being inflationary
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
+  (f : hom-Strictly-Preordered-Type P P)
+  where
+
+  is-inflationary-prop-hom-Strictly-Preordered-Type :
+    Prop (l1 ⊔ l2)
+  is-inflationary-prop-hom-Strictly-Preordered-Type =
+    is-inflationary-prop-map-Strictly-Preordered-Type P
+      ( map-hom-Strictly-Preordered-Type P P f)
+
+  is-inflationary-hom-Strictly-Preordered-Type :
+    UU (l1 ⊔ l2)
+  is-inflationary-hom-Strictly-Preordered-Type =
+    is-inflationary-map-Strictly-Preordered-Type P
+      ( map-hom-Strictly-Preordered-Type P P f)
+
+  is-prop-is-inflationary-hom-Strictly-Preordered-Type :
+    is-prop is-inflationary-hom-Strictly-Preordered-Type
+  is-prop-is-inflationary-hom-Strictly-Preordered-Type =
+    is-prop-is-inflationary-map-Strictly-Preordered-Type P
+      ( map-hom-Strictly-Preordered-Type P P f)
+```
+
+### The type of inflationary morphisms on a strictly preordered type
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
+  where
+
+  inflationary-hom-Strictly-Preordered-Type :
+    UU (l1 ⊔ l2)
+  inflationary-hom-Strictly-Preordered-Type =
+    type-subtype (is-inflationary-prop-hom-Strictly-Preordered-Type P)
+
+module _
+  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
+  (f : inflationary-hom-Strictly-Preordered-Type P)
+  where
+
+  hom-inflationary-hom-Strictly-Preordered-Type :
+    hom-Strictly-Preordered-Type P P
+  hom-inflationary-hom-Strictly-Preordered-Type =
+    pr1 f
+
+  map-inflationary-hom-Strictly-Preordered-Type :
+    type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P
+  map-inflationary-hom-Strictly-Preordered-Type =
+    map-hom-Strictly-Preordered-Type P P hom-inflationary-hom-Strictly-Preordered-Type
+
+  preserves-order-inflationary-hom-Strictly-Preordered-Type :
+    preserves-strict-order-map-Strictly-Preordered-Type P P
+      ( map-inflationary-hom-Strictly-Preordered-Type)
+  preserves-order-inflationary-hom-Strictly-Preordered-Type =
+    preserves-strict-order-hom-Strictly-Preordered-Type P P
+      ( hom-inflationary-hom-Strictly-Preordered-Type)
+
+  is-inflationary-inflationary-hom-Strictly-Preordered-Type :
+    is-inflationary-map-Strictly-Preordered-Type P
+      ( map-inflationary-hom-Strictly-Preordered-Type)
+  is-inflationary-inflationary-hom-Strictly-Preordered-Type =
+    pr2 f
+
+  inflationary-map-inflationary-hom-Strictly-Preordered-Type :
+    inflationary-map-Strictly-Preordered-Type P
+  pr1 inflationary-map-inflationary-hom-Strictly-Preordered-Type =
+    map-inflationary-hom-Strictly-Preordered-Type
+  pr2 inflationary-map-inflationary-hom-Strictly-Preordered-Type =
+    is-inflationary-inflationary-hom-Strictly-Preordered-Type
+```
diff --git a/src/order-theory/strict-order-preserving-maps.lagda.md b/src/order-theory/strict-order-preserving-maps.lagda.md
index 913acce6c2..2fe8b9d85b 100644
--- a/src/order-theory/strict-order-preserving-maps.lagda.md
+++ b/src/order-theory/strict-order-preserving-maps.lagda.md
@@ -13,145 +13,146 @@ open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
 
-open import order-theory.strictly-ordered-sets
-open import order-theory.strictly-ordered-types
+open import order-theory.strictly-preordered-sets
+open import order-theory.strictly-preordered-types
 ```
 
 </details>
 
 ## Idea
 
-Consider two [strictly ordered types](order-theory.strictly-ordered-types.md)
-$P$ and $Q$, with orderings $<_P$ and $<_Q$ respectively. A
-{{#concept "strict order preserving map" Agda=hom-Strictly-Ordered-Type}}
+Consider two
+[strictly preordered types](order-theory.strictly-preordered-types.md) $P$ and
+$Q$, with orderings $<_P$ and $<_Q$ respectively. A
+{{#concept "strict order preserving map" Agda=hom-Strictly-Preordered-Type}}
 consists of map $f : P → Q$ between their underlying types such that for any two
 elements $x<_P y$ in $P$ we have $f(x)<_Q f(y)$ in $Q$.
 
 ## Definitions
 
-### The predicate on maps between strictly ordered types of preserving the strict ordering
+### The predicate on maps between strictly preordered types of preserving the strict ordering
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Ordered-Type l1 l2) (Q : Strictly-Ordered-Type l3 l4)
-  (f : type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type Q)
+  (P : Strictly-Preordered-Type l1 l2) (Q : Strictly-Preordered-Type l3 l4)
+  (f : type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type Q)
   where
 
-  preserves-strict-order-prop-map-Strictly-Ordered-Type :
+  preserves-strict-order-prop-map-Strictly-Preordered-Type :
     Prop (l1 ⊔ l2 ⊔ l4)
-  preserves-strict-order-prop-map-Strictly-Ordered-Type =
+  preserves-strict-order-prop-map-Strictly-Preordered-Type =
     Π-Prop
-      ( type-Strictly-Ordered-Type P)
+      ( type-Strictly-Preordered-Type P)
       ( λ x →
         Π-Prop
-          ( type-Strictly-Ordered-Type P)
+          ( type-Strictly-Preordered-Type P)
           ( λ y →
             hom-Prop
-              ( le-prop-Strictly-Ordered-Type P x y)
-              ( le-prop-Strictly-Ordered-Type Q (f x) (f y))))
+              ( le-prop-Strictly-Preordered-Type P x y)
+              ( le-prop-Strictly-Preordered-Type Q (f x) (f y))))
 
-  preserves-strict-order-map-Strictly-Ordered-Type :
+  preserves-strict-order-map-Strictly-Preordered-Type :
     UU (l1 ⊔ l2 ⊔ l4)
-  preserves-strict-order-map-Strictly-Ordered-Type =
-    type-Prop preserves-strict-order-prop-map-Strictly-Ordered-Type
+  preserves-strict-order-map-Strictly-Preordered-Type =
+    type-Prop preserves-strict-order-prop-map-Strictly-Preordered-Type
 
-  is-prop-preserves-strict-order-map-Strictly-Ordered-Type :
-    is-prop preserves-strict-order-map-Strictly-Ordered-Type
-  is-prop-preserves-strict-order-map-Strictly-Ordered-Type =
-    is-prop-type-Prop preserves-strict-order-prop-map-Strictly-Ordered-Type
+  is-prop-preserves-strict-order-map-Strictly-Preordered-Type :
+    is-prop preserves-strict-order-map-Strictly-Preordered-Type
+  is-prop-preserves-strict-order-map-Strictly-Preordered-Type =
+    is-prop-type-Prop preserves-strict-order-prop-map-Strictly-Preordered-Type
 ```
 
-### The type of strict order preserving maps between strictly ordered types
+### The type of strict order preserving maps between strictly preordered types
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Ordered-Type l1 l2) (Q : Strictly-Ordered-Type l3 l4)
+  (P : Strictly-Preordered-Type l1 l2) (Q : Strictly-Preordered-Type l3 l4)
   where
 
-  hom-Strictly-Ordered-Type : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  hom-Strictly-Ordered-Type =
-    type-subtype (preserves-strict-order-prop-map-Strictly-Ordered-Type P Q)
+  hom-Strictly-Preordered-Type : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-Strictly-Preordered-Type =
+    type-subtype (preserves-strict-order-prop-map-Strictly-Preordered-Type P Q)
 
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Ordered-Type l1 l2) (Q : Strictly-Ordered-Type l3 l4)
-  (f : hom-Strictly-Ordered-Type P Q)
+  (P : Strictly-Preordered-Type l1 l2) (Q : Strictly-Preordered-Type l3 l4)
+  (f : hom-Strictly-Preordered-Type P Q)
   where
 
-  map-hom-Strictly-Ordered-Type :
-    type-Strictly-Ordered-Type P → type-Strictly-Ordered-Type Q
-  map-hom-Strictly-Ordered-Type =
+  map-hom-Strictly-Preordered-Type :
+    type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type Q
+  map-hom-Strictly-Preordered-Type =
     pr1 f
 
-  preserves-strict-order-hom-Strictly-Ordered-Type :
-    preserves-strict-order-map-Strictly-Ordered-Type P Q
-      ( map-hom-Strictly-Ordered-Type)
-  preserves-strict-order-hom-Strictly-Ordered-Type =
+  preserves-strict-order-hom-Strictly-Preordered-Type :
+    preserves-strict-order-map-Strictly-Preordered-Type P Q
+      ( map-hom-Strictly-Preordered-Type)
+  preserves-strict-order-hom-Strictly-Preordered-Type =
     pr2 f
 ```
 
-### The predicate on maps between strictly ordered sets of preserving the strict ordering
+### The predicate on maps between strictly preordered sets of preserving the strict ordering
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Ordered-Set l1 l2) (Q : Strictly-Ordered-Set l3 l4)
-  (f : type-Strictly-Ordered-Set P → type-Strictly-Ordered-Set Q)
+  (P : Strictly-Preordered-Set l1 l2) (Q : Strictly-Preordered-Set l3 l4)
+  (f : type-Strictly-Preordered-Set P → type-Strictly-Preordered-Set Q)
   where
 
-  preserves-strict-order-prop-map-Strictly-Ordered-Set :
+  preserves-strict-order-prop-map-Strictly-Preordered-Set :
     Prop (l1 ⊔ l2 ⊔ l4)
-  preserves-strict-order-prop-map-Strictly-Ordered-Set =
-    preserves-strict-order-prop-map-Strictly-Ordered-Type
-      ( strictly-ordered-type-Strictly-Ordered-Set P)
-      ( strictly-ordered-type-Strictly-Ordered-Set Q)
+  preserves-strict-order-prop-map-Strictly-Preordered-Set =
+    preserves-strict-order-prop-map-Strictly-Preordered-Type
+      ( strictly-preordered-type-Strictly-Preordered-Set P)
+      ( strictly-preordered-type-Strictly-Preordered-Set Q)
       ( f)
 
-  preserves-strict-order-map-Strictly-Ordered-Set :
+  preserves-strict-order-map-Strictly-Preordered-Set :
     UU (l1 ⊔ l2 ⊔ l4)
-  preserves-strict-order-map-Strictly-Ordered-Set =
-    preserves-strict-order-map-Strictly-Ordered-Type
-      ( strictly-ordered-type-Strictly-Ordered-Set P)
-      ( strictly-ordered-type-Strictly-Ordered-Set Q)
+  preserves-strict-order-map-Strictly-Preordered-Set =
+    preserves-strict-order-map-Strictly-Preordered-Type
+      ( strictly-preordered-type-Strictly-Preordered-Set P)
+      ( strictly-preordered-type-Strictly-Preordered-Set Q)
       ( f)
 
-  is-prop-preserves-strict-order-map-Strictly-Ordered-Set :
-    is-prop preserves-strict-order-map-Strictly-Ordered-Set
-  is-prop-preserves-strict-order-map-Strictly-Ordered-Set =
-    is-prop-preserves-strict-order-map-Strictly-Ordered-Type
-      ( strictly-ordered-type-Strictly-Ordered-Set P)
-      ( strictly-ordered-type-Strictly-Ordered-Set Q)
+  is-prop-preserves-strict-order-map-Strictly-Preordered-Set :
+    is-prop preserves-strict-order-map-Strictly-Preordered-Set
+  is-prop-preserves-strict-order-map-Strictly-Preordered-Set =
+    is-prop-preserves-strict-order-map-Strictly-Preordered-Type
+      ( strictly-preordered-type-Strictly-Preordered-Set P)
+      ( strictly-preordered-type-Strictly-Preordered-Set Q)
       ( f)
 ```
 
-### The type of strict order preserving maps between strictly ordered sets
+### The type of strict order preserving maps between strictly preordered sets
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Ordered-Set l1 l2) (Q : Strictly-Ordered-Set l3 l4)
+  (P : Strictly-Preordered-Set l1 l2) (Q : Strictly-Preordered-Set l3 l4)
   where
 
-  hom-Strictly-Ordered-Set : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  hom-Strictly-Ordered-Set =
-    type-subtype (preserves-strict-order-prop-map-Strictly-Ordered-Set P Q)
+  hom-Strictly-Preordered-Set : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-Strictly-Preordered-Set =
+    type-subtype (preserves-strict-order-prop-map-Strictly-Preordered-Set P Q)
 
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Ordered-Set l1 l2) (Q : Strictly-Ordered-Set l3 l4)
-  (f : hom-Strictly-Ordered-Set P Q)
+  (P : Strictly-Preordered-Set l1 l2) (Q : Strictly-Preordered-Set l3 l4)
+  (f : hom-Strictly-Preordered-Set P Q)
   where
 
-  map-hom-Strictly-Ordered-Set :
-    type-Strictly-Ordered-Set P → type-Strictly-Ordered-Set Q
-  map-hom-Strictly-Ordered-Set =
+  map-hom-Strictly-Preordered-Set :
+    type-Strictly-Preordered-Set P → type-Strictly-Preordered-Set Q
+  map-hom-Strictly-Preordered-Set =
     pr1 f
 
-  preserves-strict-order-hom-Strictly-Ordered-Set :
-    preserves-strict-order-map-Strictly-Ordered-Set P Q
-      ( map-hom-Strictly-Ordered-Set)
-  preserves-strict-order-hom-Strictly-Ordered-Set =
+  preserves-strict-order-hom-Strictly-Preordered-Set :
+    preserves-strict-order-map-Strictly-Preordered-Set P Q
+      ( map-hom-Strictly-Preordered-Set)
+  preserves-strict-order-hom-Strictly-Preordered-Set =
     pr2 f
 ```
diff --git a/src/order-theory/strictly-ordered-sets.lagda.md b/src/order-theory/strictly-ordered-sets.lagda.md
deleted file mode 100644
index 3710758984..0000000000
--- a/src/order-theory/strictly-ordered-sets.lagda.md
+++ /dev/null
@@ -1,120 +0,0 @@
-# Strictly ordered sets
-
-```agda
-module order-theory.strictly-ordered-sets where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.binary-relations
-open import foundation.cartesian-product-types
-open import foundation.dependent-pair-types
-open import foundation.empty-types
-open import foundation.negation
-open import foundation.propositions
-open import foundation.sets
-open import foundation.universe-levels
-
-open import order-theory.strictly-ordered-types
-```
-
-</details>
-
-## Idea
-
-A {{#concept "strictly ordered set" Agda=Strictly-Ordered-Set}} is a
-[strictly ordered type](order-theory.strictly-ordered-types.md) whose underlying
-type is a [set](foundation-core.sets.md). More specifically, a strictly ordered
-set consists of a set $A$, a [binary relation](foundation.binary-relations.md)
-$<$ on $A$ valued in the [propositions](foundation-core.propositions.md), such
-that the relation $<$ is {{#concept "irreflexive"}} and transitive:
-
-- For any $x:A$ we have $x \nle x$.
-- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
-
-Strictly ordered sets satisfy antisymmetry by irreflexivity and transitivity.
-
-## Definitions
-
-### The type of strictly ordered sets
-
-```agda
-Strictly-Ordered-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Strictly-Ordered-Set l1 l2 =
-  Σ ( Set l1)
-    ( λ A →
-      Σ ( Relation-Prop l2 (type-Set A))
-        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
-
-module _
-  {l1 l2 : Level} (A : Strictly-Ordered-Set l1 l2)
-  where
-
-  set-Strictly-Ordered-Set :
-    Set l1
-  set-Strictly-Ordered-Set =
-    pr1 A
-
-  type-Strictly-Ordered-Set :
-    UU l1
-  type-Strictly-Ordered-Set =
-    type-Set set-Strictly-Ordered-Set
-
-  is-set-type-Strictly-Ordered-Set :
-    is-set type-Strictly-Ordered-Set
-  is-set-type-Strictly-Ordered-Set =
-    is-set-type-Set set-Strictly-Ordered-Set
-
-  le-prop-Strictly-Ordered-Set :
-    Relation-Prop l2 type-Strictly-Ordered-Set
-  le-prop-Strictly-Ordered-Set =
-    pr1 (pr2 A)
-
-  le-Strictly-Ordered-Set :
-    Relation l2 type-Strictly-Ordered-Set
-  le-Strictly-Ordered-Set =
-    type-Relation-Prop le-prop-Strictly-Ordered-Set
-
-  is-prop-le-Strictly-Ordered-Set :
-    (x y : type-Strictly-Ordered-Set) → is-prop (le-Strictly-Ordered-Set x y)
-  is-prop-le-Strictly-Ordered-Set =
-    is-prop-type-Relation-Prop le-prop-Strictly-Ordered-Set
-
-  is-irreflexive-le-Strictly-Ordered-Set :
-    is-irreflexive le-Strictly-Ordered-Set
-  is-irreflexive-le-Strictly-Ordered-Set =
-    pr1 (pr2 (pr2 A))
-
-  is-transitive-le-Strictly-Ordered-Set :
-    is-transitive le-Strictly-Ordered-Set
-  is-transitive-le-Strictly-Ordered-Set =
-    pr2 (pr2 (pr2 A))
-
-  strictly-ordered-type-Strictly-Ordered-Set :
-    Strictly-Ordered-Type l1 l2
-  pr1 strictly-ordered-type-Strictly-Ordered-Set =
-    type-Strictly-Ordered-Set
-  pr1 (pr2 strictly-ordered-type-Strictly-Ordered-Set) =
-    le-prop-Strictly-Ordered-Set
-  pr1 (pr2 (pr2 strictly-ordered-type-Strictly-Ordered-Set)) =
-    is-irreflexive-le-Strictly-Ordered-Set
-  pr2 (pr2 (pr2 strictly-ordered-type-Strictly-Ordered-Set)) =
-    is-transitive-le-Strictly-Ordered-Set
-```
-
-## Properties
-
-### The ordering of a strictly ordered set is antisymmetric
-
-```agda
-module _
-  {l1 l2 : Level} (A : Strictly-Ordered-Set l1 l2)
-  where
-
-  is-antisymmetric-le-Strictly-Ordered-Set :
-    is-antisymmetric (le-Strictly-Ordered-Set A)
-  is-antisymmetric-le-Strictly-Ordered-Set =
-    is-antisymmetric-le-Strictly-Ordered-Type
-      ( strictly-ordered-type-Strictly-Ordered-Set A)
-```
diff --git a/src/order-theory/strictly-ordered-types.lagda.md b/src/order-theory/strictly-ordered-types.lagda.md
deleted file mode 100644
index d0ddaef694..0000000000
--- a/src/order-theory/strictly-ordered-types.lagda.md
+++ /dev/null
@@ -1,95 +0,0 @@
-# Strictly ordered types
-
-```agda
-module order-theory.strictly-ordered-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.binary-relations
-open import foundation.cartesian-product-types
-open import foundation.dependent-pair-types
-open import foundation.empty-types
-open import foundation.negation
-open import foundation.propositions
-open import foundation.universe-levels
-```
-
-</details>
-
-## Idea
-
-A {{#concept "strictly ordered type" Agda=Strictly-Ordered-Type}} consists of a
-type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued
-in the [propositions](foundation-core.propositions.md), such that the relation
-$<$ is {{#concept "irreflexive"}} and transitive:
-
-- For any $x:A$ we have $x \nle x$.
-- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
-
-Strictly ordered types satisfy antisymmetry by irreflexivity and transitivity.
-
-## Definitions
-
-### The type of strictly ordered types
-
-```agda
-Strictly-Ordered-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Strictly-Ordered-Type l1 l2 =
-  Σ ( UU l1)
-    ( λ A →
-      Σ ( Relation-Prop l2 A)
-        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
-
-module _
-  {l1 l2 : Level} (A : Strictly-Ordered-Type l1 l2)
-  where
-
-  type-Strictly-Ordered-Type :
-    UU l1
-  type-Strictly-Ordered-Type =
-    pr1 A
-
-  le-prop-Strictly-Ordered-Type :
-    Relation-Prop l2 type-Strictly-Ordered-Type
-  le-prop-Strictly-Ordered-Type =
-    pr1 (pr2 A)
-
-  le-Strictly-Ordered-Type :
-    Relation l2 type-Strictly-Ordered-Type
-  le-Strictly-Ordered-Type =
-    type-Relation-Prop le-prop-Strictly-Ordered-Type
-
-  is-prop-le-Strictly-Ordered-Type :
-    (x y : type-Strictly-Ordered-Type) → is-prop (le-Strictly-Ordered-Type x y)
-  is-prop-le-Strictly-Ordered-Type =
-    is-prop-type-Relation-Prop le-prop-Strictly-Ordered-Type
-
-  is-irreflexive-le-Strictly-Ordered-Type :
-    is-irreflexive le-Strictly-Ordered-Type
-  is-irreflexive-le-Strictly-Ordered-Type =
-    pr1 (pr2 (pr2 A))
-
-  is-transitive-le-Strictly-Ordered-Type :
-    is-transitive le-Strictly-Ordered-Type
-  is-transitive-le-Strictly-Ordered-Type =
-    pr2 (pr2 (pr2 A))
-```
-
-## Properties
-
-### The ordering of a strictly ordered type is antisymmetric
-
-```agda
-module _
-  {l1 l2 : Level} (A : Strictly-Ordered-Type l1 l2)
-  where
-
-  is-antisymmetric-le-Strictly-Ordered-Type :
-    is-antisymmetric (le-Strictly-Ordered-Type A)
-  is-antisymmetric-le-Strictly-Ordered-Type x y H K =
-    ex-falso
-      ( is-irreflexive-le-Strictly-Ordered-Type A x
-        ( is-transitive-le-Strictly-Ordered-Type A x y x K H))
-```
diff --git a/src/order-theory/strictly-preordered-sets.lagda.md b/src/order-theory/strictly-preordered-sets.lagda.md
new file mode 100644
index 0000000000..60f8b7d338
--- /dev/null
+++ b/src/order-theory/strictly-preordered-sets.lagda.md
@@ -0,0 +1,121 @@
+# Strictly preordered sets
+
+```agda
+module order-theory.strictly-preordered-sets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import order-theory.strictly-preordered-types
+```
+
+</details>
+
+## Idea
+
+A {{#concept "strictly preordered set" Agda=Strictly-Preordered-Set}} is a
+[strictly preordered type](order-theory.strictly-preordered-types.md) whose
+underlying type is a [set](foundation-core.sets.md). More specifically, a
+strictly preordered set consists of a set $A$, a
+[binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the
+[propositions](foundation-core.propositions.md), such that the relation $<$ is
+{{#concept "irreflexive"}} and transitive:
+
+- For any $x:A$ we have $x \nle x$.
+- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
+
+Strictly preordered sets satisfy antisymmetry by irreflexivity and transitivity.
+
+## Definitions
+
+### The type of strictly preordered sets
+
+```agda
+Strictly-Preordered-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Strictly-Preordered-Set l1 l2 =
+  Σ ( Set l1)
+    ( λ A →
+      Σ ( Relation-Prop l2 (type-Set A))
+        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
+
+module _
+  {l1 l2 : Level} (A : Strictly-Preordered-Set l1 l2)
+  where
+
+  set-Strictly-Preordered-Set :
+    Set l1
+  set-Strictly-Preordered-Set =
+    pr1 A
+
+  type-Strictly-Preordered-Set :
+    UU l1
+  type-Strictly-Preordered-Set =
+    type-Set set-Strictly-Preordered-Set
+
+  is-set-type-Strictly-Preordered-Set :
+    is-set type-Strictly-Preordered-Set
+  is-set-type-Strictly-Preordered-Set =
+    is-set-type-Set set-Strictly-Preordered-Set
+
+  le-prop-Strictly-Preordered-Set :
+    Relation-Prop l2 type-Strictly-Preordered-Set
+  le-prop-Strictly-Preordered-Set =
+    pr1 (pr2 A)
+
+  le-Strictly-Preordered-Set :
+    Relation l2 type-Strictly-Preordered-Set
+  le-Strictly-Preordered-Set =
+    type-Relation-Prop le-prop-Strictly-Preordered-Set
+
+  is-prop-le-Strictly-Preordered-Set :
+    (x y : type-Strictly-Preordered-Set) → is-prop (le-Strictly-Preordered-Set x y)
+  is-prop-le-Strictly-Preordered-Set =
+    is-prop-type-Relation-Prop le-prop-Strictly-Preordered-Set
+
+  is-irreflexive-le-Strictly-Preordered-Set :
+    is-irreflexive le-Strictly-Preordered-Set
+  is-irreflexive-le-Strictly-Preordered-Set =
+    pr1 (pr2 (pr2 A))
+
+  is-transitive-le-Strictly-Preordered-Set :
+    is-transitive le-Strictly-Preordered-Set
+  is-transitive-le-Strictly-Preordered-Set =
+    pr2 (pr2 (pr2 A))
+
+  strictly-preordered-type-Strictly-Preordered-Set :
+    Strictly-Preordered-Type l1 l2
+  pr1 strictly-preordered-type-Strictly-Preordered-Set =
+    type-Strictly-Preordered-Set
+  pr1 (pr2 strictly-preordered-type-Strictly-Preordered-Set) =
+    le-prop-Strictly-Preordered-Set
+  pr1 (pr2 (pr2 strictly-preordered-type-Strictly-Preordered-Set)) =
+    is-irreflexive-le-Strictly-Preordered-Set
+  pr2 (pr2 (pr2 strictly-preordered-type-Strictly-Preordered-Set)) =
+    is-transitive-le-Strictly-Preordered-Set
+```
+
+## Properties
+
+### The ordering of a strictly preordered set is antisymmetric
+
+```agda
+module _
+  {l1 l2 : Level} (A : Strictly-Preordered-Set l1 l2)
+  where
+
+  is-antisymmetric-le-Strictly-Preordered-Set :
+    is-antisymmetric (le-Strictly-Preordered-Set A)
+  is-antisymmetric-le-Strictly-Preordered-Set =
+    is-antisymmetric-le-Strictly-Preordered-Type
+      ( strictly-preordered-type-Strictly-Preordered-Set A)
+```
diff --git a/src/order-theory/strictly-preordered-types.lagda.md b/src/order-theory/strictly-preordered-types.lagda.md
new file mode 100644
index 0000000000..b9dc5c9640
--- /dev/null
+++ b/src/order-theory/strictly-preordered-types.lagda.md
@@ -0,0 +1,96 @@
+# Strictly preordered types
+
+```agda
+module order-theory.strictly-preordered-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "strictly preordered type" Agda=Strictly-Preordered-Type}} consists
+of a type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$
+valued in the [propositions](foundation-core.propositions.md), such that the
+relation $<$ is {{#concept "irreflexive"}} and transitive:
+
+- For any $x:A$ we have $x \nle x$.
+- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
+
+Strictly preordered types satisfy antisymmetry by irreflexivity and
+transitivity.
+
+## Definitions
+
+### The type of strictly preordered types
+
+```agda
+Strictly-Preordered-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Strictly-Preordered-Type l1 l2 =
+  Σ ( UU l1)
+    ( λ A →
+      Σ ( Relation-Prop l2 A)
+        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
+
+module _
+  {l1 l2 : Level} (A : Strictly-Preordered-Type l1 l2)
+  where
+
+  type-Strictly-Preordered-Type :
+    UU l1
+  type-Strictly-Preordered-Type =
+    pr1 A
+
+  le-prop-Strictly-Preordered-Type :
+    Relation-Prop l2 type-Strictly-Preordered-Type
+  le-prop-Strictly-Preordered-Type =
+    pr1 (pr2 A)
+
+  le-Strictly-Preordered-Type :
+    Relation l2 type-Strictly-Preordered-Type
+  le-Strictly-Preordered-Type =
+    type-Relation-Prop le-prop-Strictly-Preordered-Type
+
+  is-prop-le-Strictly-Preordered-Type :
+    (x y : type-Strictly-Preordered-Type) → is-prop (le-Strictly-Preordered-Type x y)
+  is-prop-le-Strictly-Preordered-Type =
+    is-prop-type-Relation-Prop le-prop-Strictly-Preordered-Type
+
+  is-irreflexive-le-Strictly-Preordered-Type :
+    is-irreflexive le-Strictly-Preordered-Type
+  is-irreflexive-le-Strictly-Preordered-Type =
+    pr1 (pr2 (pr2 A))
+
+  is-transitive-le-Strictly-Preordered-Type :
+    is-transitive le-Strictly-Preordered-Type
+  is-transitive-le-Strictly-Preordered-Type =
+    pr2 (pr2 (pr2 A))
+```
+
+## Properties
+
+### The ordering of a strictly preordered type is antisymmetric
+
+```agda
+module _
+  {l1 l2 : Level} (A : Strictly-Preordered-Type l1 l2)
+  where
+
+  is-antisymmetric-le-Strictly-Preordered-Type :
+    is-antisymmetric (le-Strictly-Preordered-Type A)
+  is-antisymmetric-le-Strictly-Preordered-Type x y H K =
+    ex-falso
+      ( is-irreflexive-le-Strictly-Preordered-Type A x
+        ( is-transitive-le-Strictly-Preordered-Type A x y x K H))
+```

From 28374b887635aa9bc1ea4d72e7c8ae6afddc17ca Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 16:08:45 -0500
Subject: [PATCH 12/17] fixes

---
 src/elementary-number-theory.lagda.md         |  2 +-
 ...-ordered-pairs-of-natural-numbers.lagda.md | 50 +++++++++----------
 src/foundation/repetitions-sequences.lagda.md |  8 +--
 ...ry-maps-strictly-preordered-types.lagda.md |  3 +-
 .../strictly-preordered-sets.lagda.md         |  3 +-
 .../strictly-preordered-types.lagda.md        |  3 +-
 6 files changed, 36 insertions(+), 33 deletions(-)

diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index 2c044fc6b3..befe9c31fc 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -161,7 +161,7 @@ open import elementary-number-theory.strict-inequality-integers public
 open import elementary-number-theory.strict-inequality-natural-numbers public
 open import elementary-number-theory.strict-inequality-rational-numbers public
 open import elementary-number-theory.strict-inequality-standard-finite-types public
-open import elementary-number-theory.strictly-preordered-pairs-of-natural-numbers public
+open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
 open import elementary-number-theory.strong-induction-natural-numbers public
 open import elementary-number-theory.sums-of-natural-numbers public
 open import elementary-number-theory.sylvesters-sequence public
diff --git a/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md b/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
index 4c9cec59c8..faab496e28 100644
--- a/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
@@ -1,7 +1,7 @@
 # Strictly ordered pairs of natural numbers
 
 ```agda
-module elementary-number-theory.strictly-preordered-pairs-of-natural-numbers where
+module elementary-number-theory.strictly-ordered-pairs-of-natural-numbers where
 ```
 
 <details><summary>Imports</summary>
@@ -32,22 +32,22 @@ A strictly ordered pair of natural numbers consists of `x y : ℕ` such that
 ## Definition
 
 ```agda
-strictly-preordered-pair-ℕ : UU lzero
-strictly-preordered-pair-ℕ = Σ ℕ (λ x → Σ ℕ (λ y → le-ℕ x y))
+strictly-ordered-pair-ℕ : UU lzero
+strictly-ordered-pair-ℕ = Σ ℕ (λ x → Σ ℕ (λ y → le-ℕ x y))
 
 module _
-  (p : strictly-preordered-pair-ℕ)
+  (p : strictly-ordered-pair-ℕ)
   where
 
-  first-strictly-preordered-pair-ℕ : ℕ
-  first-strictly-preordered-pair-ℕ = pr1 p
+  first-strictly-ordered-pair-ℕ : ℕ
+  first-strictly-ordered-pair-ℕ = pr1 p
 
-  second-strictly-preordered-pair-ℕ : ℕ
-  second-strictly-preordered-pair-ℕ = pr1 (pr2 p)
+  second-strictly-ordered-pair-ℕ : ℕ
+  second-strictly-ordered-pair-ℕ = pr1 (pr2 p)
 
-  strict-inequality-strictly-preordered-pair-ℕ :
-    le-ℕ first-strictly-preordered-pair-ℕ second-strictly-preordered-pair-ℕ
-  strict-inequality-strictly-preordered-pair-ℕ = pr2 (pr2 p)
+  strict-inequality-strictly-ordered-pair-ℕ :
+    le-ℕ first-strictly-ordered-pair-ℕ second-strictly-ordered-pair-ℕ
+  strict-inequality-strictly-ordered-pair-ℕ = pr2 (pr2 p)
 ```
 
 ## Properties
@@ -55,34 +55,34 @@ module _
 ### Strictly ordered pairs of natural numbers are pairs of distinct elements
 
 ```agda
-pair-of-distinct-elements-strictly-preordered-pair-ℕ :
-  strictly-preordered-pair-ℕ → pair-of-distinct-elements ℕ
-pair-of-distinct-elements-strictly-preordered-pair-ℕ (a , b , H) =
+pair-of-distinct-elements-strictly-ordered-pair-ℕ :
+  strictly-ordered-pair-ℕ → pair-of-distinct-elements ℕ
+pair-of-distinct-elements-strictly-ordered-pair-ℕ (a , b , H) =
   (a , b , neq-le-ℕ H)
 ```
 
 ### Any pair of distinct elements of natural numbers can be strictly ordered
 
 ```agda
-strictly-preordered-pair-pair-of-distinct-elements-ℕ' :
-  (a b : ℕ) → a ≠ b → strictly-preordered-pair-ℕ
-strictly-preordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ zero-ℕ H =
+strictly-ordered-pair-pair-of-distinct-elements-ℕ' :
+  (a b : ℕ) → a ≠ b → strictly-ordered-pair-ℕ
+strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ zero-ℕ H =
   ex-falso (H refl)
-strictly-preordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ (succ-ℕ b) H =
+strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ (succ-ℕ b) H =
   (0 , succ-ℕ b , star)
-strictly-preordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) zero-ℕ H =
+strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) zero-ℕ H =
   (0 , succ-ℕ a , star)
-strictly-preordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) (succ-ℕ b) H =
+strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) (succ-ℕ b) H =
   map-Σ
     ( λ x → Σ ℕ (λ y → le-ℕ x y))
     ( succ-ℕ)
     ( λ x →
       map-Σ (le-ℕ (succ-ℕ x)) succ-ℕ (λ y → id))
-    ( strictly-preordered-pair-pair-of-distinct-elements-ℕ' a b
+    ( strictly-ordered-pair-pair-of-distinct-elements-ℕ' a b
       ( λ p → H (ap succ-ℕ p)))
 
-strictly-preordered-pair-pair-of-distinct-elements-ℕ :
-  pair-of-distinct-elements ℕ → strictly-preordered-pair-ℕ
-strictly-preordered-pair-pair-of-distinct-elements-ℕ (a , b , H) =
-  strictly-preordered-pair-pair-of-distinct-elements-ℕ' a b H
+strictly-ordered-pair-pair-of-distinct-elements-ℕ :
+  pair-of-distinct-elements ℕ → strictly-ordered-pair-ℕ
+strictly-ordered-pair-pair-of-distinct-elements-ℕ (a , b , H) =
+  strictly-ordered-pair-pair-of-distinct-elements-ℕ' a b H
 ```
diff --git a/src/foundation/repetitions-sequences.lagda.md b/src/foundation/repetitions-sequences.lagda.md
index 1d7a764730..c52b33a71d 100644
--- a/src/foundation/repetitions-sequences.lagda.md
+++ b/src/foundation/repetitions-sequences.lagda.md
@@ -8,7 +8,7 @@ module foundation.repetitions-sequences where
 
 ```agda
 open import elementary-number-theory.natural-numbers
-open import elementary-number-theory.strictly-preordered-pairs-of-natural-numbers
+open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
@@ -84,14 +84,14 @@ module _
 
 ```agda
 is-ordered-repetition-of-values-ℕ :
-  {l1 : Level} {A : UU l1} (f : ℕ → A) (x : strictly-preordered-pair-ℕ) → UU l1
+  {l1 : Level} {A : UU l1} (f : ℕ → A) (x : strictly-ordered-pair-ℕ) → UU l1
 is-ordered-repetition-of-values-ℕ f x =
-  f (first-strictly-preordered-pair-ℕ x) ＝ f (second-strictly-preordered-pair-ℕ x)
+  f (first-strictly-ordered-pair-ℕ x) ＝ f (second-strictly-ordered-pair-ℕ x)
 
 ordered-repetition-of-values-ℕ :
   {l1 : Level} {A : UU l1} (f : ℕ → A) → UU l1
 ordered-repetition-of-values-ℕ f =
-  Σ strictly-preordered-pair-ℕ (is-ordered-repetition-of-values-ℕ f)
+  Σ strictly-ordered-pair-ℕ (is-ordered-repetition-of-values-ℕ f)
 
 ordered-repetition-of-values-comp-ℕ :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : A → B) {f : ℕ → A} →
diff --git a/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md b/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
index 2bbcbfe244..bad8fec727 100644
--- a/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
+++ b/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
@@ -144,7 +144,8 @@ module _
   map-inflationary-hom-Strictly-Preordered-Type :
     type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P
   map-inflationary-hom-Strictly-Preordered-Type =
-    map-hom-Strictly-Preordered-Type P P hom-inflationary-hom-Strictly-Preordered-Type
+    map-hom-Strictly-Preordered-Type P P
+      ( hom-inflationary-hom-Strictly-Preordered-Type)
 
   preserves-order-inflationary-hom-Strictly-Preordered-Type :
     preserves-strict-order-map-Strictly-Preordered-Type P P
diff --git a/src/order-theory/strictly-preordered-sets.lagda.md b/src/order-theory/strictly-preordered-sets.lagda.md
index 60f8b7d338..6037f8f381 100644
--- a/src/order-theory/strictly-preordered-sets.lagda.md
+++ b/src/order-theory/strictly-preordered-sets.lagda.md
@@ -78,7 +78,8 @@ module _
     type-Relation-Prop le-prop-Strictly-Preordered-Set
 
   is-prop-le-Strictly-Preordered-Set :
-    (x y : type-Strictly-Preordered-Set) → is-prop (le-Strictly-Preordered-Set x y)
+    (x y : type-Strictly-Preordered-Set) →
+    is-prop (le-Strictly-Preordered-Set x y)
   is-prop-le-Strictly-Preordered-Set =
     is-prop-type-Relation-Prop le-prop-Strictly-Preordered-Set
 
diff --git a/src/order-theory/strictly-preordered-types.lagda.md b/src/order-theory/strictly-preordered-types.lagda.md
index b9dc5c9640..a7fed3c0e2 100644
--- a/src/order-theory/strictly-preordered-types.lagda.md
+++ b/src/order-theory/strictly-preordered-types.lagda.md
@@ -63,7 +63,8 @@ module _
     type-Relation-Prop le-prop-Strictly-Preordered-Type
 
   is-prop-le-Strictly-Preordered-Type :
-    (x y : type-Strictly-Preordered-Type) → is-prop (le-Strictly-Preordered-Type x y)
+    (x y : type-Strictly-Preordered-Type) →
+    is-prop (le-Strictly-Preordered-Type x y)
   is-prop-le-Strictly-Preordered-Type =
     is-prop-type-Relation-Prop le-prop-Strictly-Preordered-Type
 

From de912a60e46b897508aaf198d627668a482b3ee7 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 16:12:17 -0500
Subject: [PATCH 13/17] irreflexive

---
 src/order-theory/strictly-preordered-sets.lagda.md  | 2 +-
 src/order-theory/strictly-preordered-types.lagda.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/order-theory/strictly-preordered-sets.lagda.md b/src/order-theory/strictly-preordered-sets.lagda.md
index 6037f8f381..9ce0db23f5 100644
--- a/src/order-theory/strictly-preordered-sets.lagda.md
+++ b/src/order-theory/strictly-preordered-sets.lagda.md
@@ -29,7 +29,7 @@ underlying type is a [set](foundation-core.sets.md). More specifically, a
 strictly preordered set consists of a set $A$, a
 [binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the
 [propositions](foundation-core.propositions.md), such that the relation $<$ is
-{{#concept "irreflexive"}} and transitive:
+irreflexive and transitive:
 
 - For any $x:A$ we have $x \nle x$.
 - For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
diff --git a/src/order-theory/strictly-preordered-types.lagda.md b/src/order-theory/strictly-preordered-types.lagda.md
index a7fed3c0e2..e65b5756f1 100644
--- a/src/order-theory/strictly-preordered-types.lagda.md
+++ b/src/order-theory/strictly-preordered-types.lagda.md
@@ -23,7 +23,7 @@ open import foundation.universe-levels
 A {{#concept "strictly preordered type" Agda=Strictly-Preordered-Type}} consists
 of a type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$
 valued in the [propositions](foundation-core.propositions.md), such that the
-relation $<$ is {{#concept "irreflexive"}} and transitive:
+relation $<$ is irreflexive and transitive:
 
 - For any $x:A$ we have $x \nle x$.
 - For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.

From c4aa22f7805edc803aba036616912161efa2ecb4 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 16:37:33 -0500
Subject: [PATCH 14/17] rename strictly inflationary maps

---
 ...y-maps-strictly-preordered-types.lagda.md} | 62 +++++++++----------
 1 file changed, 31 insertions(+), 31 deletions(-)
 rename src/order-theory/{inflationary-maps-strictly-preordered-types.lagda.md => strictly-inflationary-maps-strictly-preordered-types.lagda.md} (65%)

diff --git a/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md b/src/order-theory/strictly-inflationary-maps-strictly-preordered-types.lagda.md
similarity index 65%
rename from src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
rename to src/order-theory/strictly-inflationary-maps-strictly-preordered-types.lagda.md
index bad8fec727..edca001001 100644
--- a/src/order-theory/inflationary-maps-strictly-preordered-types.lagda.md
+++ b/src/order-theory/strictly-inflationary-maps-strictly-preordered-types.lagda.md
@@ -1,7 +1,7 @@
-# Inflationary maps on a strictly preordered type
+# Strictly inflationary maps on a strictly preordered type
 
 ```agda
-module order-theory.inflationary-maps-strictly-preordered-types where
+module order-theory.strictly-inflationary-maps-strictly-preordered-types where
 ```
 
 <details><summary>Imports</summary>
@@ -22,8 +22,8 @@ open import order-theory.strictly-preordered-types
 
 A map $f : P → P$ on a
 [strictly preordered type](order-theory.strictly-preordered-types.md) $P$ is
-said to be an
-{{#concept "inflationary map" Disambiguation="strictly preordered type" Agda=inflationary-map-Strictly-Preordered-Type}}
+said to be a
+{{#concept "strictly inflationary map" Disambiguation="strictly preordered type" Agda=strictly-inflationary-map}}
 if the inequality
 
 $$
@@ -32,12 +32,12 @@ $$
 
 holds for any element $x : P$. If $f$ is also
 [order preserving](order-theory.strict-order-preserving-maps.md) we say that $f$
-is an
-{{#concept "inflationary morphism" Disambiguation="strictly preordered type" Agda=inflationary-hom-Strictly-Preordered-Type}}.
+is a
+{{#concept "strictly inflationary morphism" Disambiguation="strictly preordered type" Agda=inflationary-hom-Strictly-Preordered-Type}}.
 
 ## Definitions
 
-### The predicate of being an inflationary map
+### The predicate of being a strictly inflationary map
 
 ```agda
 module _
@@ -45,22 +45,22 @@ module _
   (f : type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P)
   where
 
-  is-inflationary-prop-map-Strictly-Preordered-Type :
+  is-strictly-inflationary-map-prop-Strictly-Preordered-Type :
     Prop (l1 ⊔ l2)
-  is-inflationary-prop-map-Strictly-Preordered-Type =
+  is-strictly-inflationary-map-prop-Strictly-Preordered-Type =
     Π-Prop
       ( type-Strictly-Preordered-Type P)
       ( λ x → le-prop-Strictly-Preordered-Type P x (f x))
 
-  is-inflationary-map-Strictly-Preordered-Type :
+  is-strictly-inflationary-map-Strictly-Preordered-Type :
     UU (l1 ⊔ l2)
-  is-inflationary-map-Strictly-Preordered-Type =
-    type-Prop is-inflationary-prop-map-Strictly-Preordered-Type
+  is-strictly-inflationary-map-Strictly-Preordered-Type =
+    type-Prop is-strictly-inflationary-map-prop-Strictly-Preordered-Type
 
-  is-prop-is-inflationary-map-Strictly-Preordered-Type :
-    is-prop is-inflationary-map-Strictly-Preordered-Type
-  is-prop-is-inflationary-map-Strictly-Preordered-Type =
-    is-prop-type-Prop is-inflationary-prop-map-Strictly-Preordered-Type
+  is-prop-is-strictly-inflationary-map-Strictly-Preordered-Type :
+    is-prop is-strictly-inflationary-map-Strictly-Preordered-Type
+  is-prop-is-strictly-inflationary-map-Strictly-Preordered-Type =
+    is-prop-type-Prop is-strictly-inflationary-map-prop-Strictly-Preordered-Type
 ```
 
 ### The type of inflationary maps on a strictly preordered type
@@ -70,25 +70,25 @@ module _
   {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
   where
 
-  inflationary-map-Strictly-Preordered-Type :
+  strictly-inflationary-map-Strictly-Preordered-Type :
     UU (l1 ⊔ l2)
-  inflationary-map-Strictly-Preordered-Type =
-    type-subtype (is-inflationary-prop-map-Strictly-Preordered-Type P)
+  strictly-inflationary-map-Strictly-Preordered-Type =
+    type-subtype (is-strictly-inflationary-map-prop-Strictly-Preordered-Type P)
 
 module _
   {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
-  (f : inflationary-map-Strictly-Preordered-Type P)
+  (f : strictly-inflationary-map-Strictly-Preordered-Type P)
   where
 
-  map-inflationary-map-Strictly-Preordered-Type :
+  map-strictly-inflationary-map-Strictly-Preordered-Type :
     type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P
-  map-inflationary-map-Strictly-Preordered-Type =
+  map-strictly-inflationary-map-Strictly-Preordered-Type =
     pr1 f
 
-  is-inflationary-inflationary-map-Strictly-Preordered-Type :
-    is-inflationary-map-Strictly-Preordered-Type P
-      ( map-inflationary-map-Strictly-Preordered-Type)
-  is-inflationary-inflationary-map-Strictly-Preordered-Type =
+  is-inflationary-strictly-inflationary-map-Strictly-Preordered-Type :
+    is-strictly-inflationary-map-Strictly-Preordered-Type P
+      ( map-strictly-inflationary-map-Strictly-Preordered-Type)
+  is-inflationary-strictly-inflationary-map-Strictly-Preordered-Type =
     pr2 f
 ```
 
@@ -103,19 +103,19 @@ module _
   is-inflationary-prop-hom-Strictly-Preordered-Type :
     Prop (l1 ⊔ l2)
   is-inflationary-prop-hom-Strictly-Preordered-Type =
-    is-inflationary-prop-map-Strictly-Preordered-Type P
+    is-strictly-inflationary-map-prop-Strictly-Preordered-Type P
       ( map-hom-Strictly-Preordered-Type P P f)
 
   is-inflationary-hom-Strictly-Preordered-Type :
     UU (l1 ⊔ l2)
   is-inflationary-hom-Strictly-Preordered-Type =
-    is-inflationary-map-Strictly-Preordered-Type P
+    is-strictly-inflationary-map-Strictly-Preordered-Type P
       ( map-hom-Strictly-Preordered-Type P P f)
 
   is-prop-is-inflationary-hom-Strictly-Preordered-Type :
     is-prop is-inflationary-hom-Strictly-Preordered-Type
   is-prop-is-inflationary-hom-Strictly-Preordered-Type =
-    is-prop-is-inflationary-map-Strictly-Preordered-Type P
+    is-prop-is-strictly-inflationary-map-Strictly-Preordered-Type P
       ( map-hom-Strictly-Preordered-Type P P f)
 ```
 
@@ -155,13 +155,13 @@ module _
       ( hom-inflationary-hom-Strictly-Preordered-Type)
 
   is-inflationary-inflationary-hom-Strictly-Preordered-Type :
-    is-inflationary-map-Strictly-Preordered-Type P
+    is-strictly-inflationary-map-Strictly-Preordered-Type P
       ( map-inflationary-hom-Strictly-Preordered-Type)
   is-inflationary-inflationary-hom-Strictly-Preordered-Type =
     pr2 f
 
   inflationary-map-inflationary-hom-Strictly-Preordered-Type :
-    inflationary-map-Strictly-Preordered-Type P
+    strictly-inflationary-map-Strictly-Preordered-Type P
   pr1 inflationary-map-inflationary-hom-Strictly-Preordered-Type =
     map-inflationary-hom-Strictly-Preordered-Type
   pr2 inflationary-map-inflationary-hom-Strictly-Preordered-Type =

From ed1905cb8e9047ca325cfbc741bb66c468b7aa20 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 16:37:57 -0500
Subject: [PATCH 15/17] make pre-commit

---
 src/order-theory.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index a1e9bc7fd1..a2ec2195c2 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -53,7 +53,6 @@ open import order-theory.ideals-preorders public
 open import order-theory.incidence-algebras public
 open import order-theory.inflationary-maps-posets public
 open import order-theory.inflationary-maps-preorders public
-open import order-theory.inflationary-maps-strictly-preordered-types public
 open import order-theory.inflattices public
 open import order-theory.inhabited-chains-posets public
 open import order-theory.inhabited-chains-preorders public
@@ -117,6 +116,7 @@ open import order-theory.similarity-of-elements-large-preorders public
 open import order-theory.similarity-of-order-preserving-maps-large-posets public
 open import order-theory.similarity-of-order-preserving-maps-large-preorders public
 open import order-theory.strict-order-preserving-maps public
+open import order-theory.strictly-inflationary-maps-strictly-preordered-types public
 open import order-theory.strictly-preordered-sets public
 open import order-theory.strictly-preordered-types public
 open import order-theory.subposets public

From 43ac3445fad08937f702964806e32cb4f5464dee Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 16:47:49 -0500
Subject: [PATCH 16/17] rename strictly preordered type to strict preorder

---
 src/order-theory.lagda.md                     |   4 +-
 .../strict-order-preserving-maps.lagda.md     |  91 +++++-----
 src/order-theory/strict-preorders.lagda.md    |  97 ++++++++++
 ...nflationary-maps-strict-preorders.lagda.md | 168 +++++++++++++++++
 ...ry-maps-strictly-preordered-types.lagda.md | 169 ------------------
 .../strictly-preordered-sets.lagda.md         |  24 +--
 .../strictly-preordered-types.lagda.md        |  97 ----------
 7 files changed, 324 insertions(+), 326 deletions(-)
 create mode 100644 src/order-theory/strict-preorders.lagda.md
 create mode 100644 src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md
 delete mode 100644 src/order-theory/strictly-inflationary-maps-strictly-preordered-types.lagda.md
 delete mode 100644 src/order-theory/strictly-preordered-types.lagda.md

diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index a2ec2195c2..4cf6f35d78 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -116,9 +116,9 @@ open import order-theory.similarity-of-elements-large-preorders public
 open import order-theory.similarity-of-order-preserving-maps-large-posets public
 open import order-theory.similarity-of-order-preserving-maps-large-preorders public
 open import order-theory.strict-order-preserving-maps public
-open import order-theory.strictly-inflationary-maps-strictly-preordered-types public
+open import order-theory.strictly-inflationary-maps-strict-preorders public
 open import order-theory.strictly-preordered-sets public
-open import order-theory.strictly-preordered-types public
+open import order-theory.strict-preorders public
 open import order-theory.subposets public
 open import order-theory.subpreorders public
 open import order-theory.suplattices public
diff --git a/src/order-theory/strict-order-preserving-maps.lagda.md b/src/order-theory/strict-order-preserving-maps.lagda.md
index 2fe8b9d85b..f0ea631fc1 100644
--- a/src/order-theory/strict-order-preserving-maps.lagda.md
+++ b/src/order-theory/strict-order-preserving-maps.lagda.md
@@ -14,82 +14,81 @@ open import foundation.subtypes
 open import foundation.universe-levels
 
 open import order-theory.strictly-preordered-sets
-open import order-theory.strictly-preordered-types
+open import order-theory.strict-preorders
 ```
 
 </details>
 
 ## Idea
 
-Consider two
-[strictly preordered types](order-theory.strictly-preordered-types.md) $P$ and
-$Q$, with orderings $<_P$ and $<_Q$ respectively. A
-{{#concept "strict order preserving map" Agda=hom-Strictly-Preordered-Type}}
-consists of map $f : P → Q$ between their underlying types such that for any two
-elements $x<_P y$ in $P$ we have $f(x)<_Q f(y)$ in $Q$.
+Consider two [strict preorders](order-theory.strict-preorders.md) $P$
+and $Q$, with orderings $<_P$ and $<_Q$ respectively. A
+{{#concept "strict order preserving map" Agda=hom-Strict-Preorder}} consists of
+map $f : P → Q$ between their underlying types such that for any two elements
+$x<_P y$ in $P$ we have $f(x)<_Q f(y)$ in $Q$.
 
 ## Definitions
 
-### The predicate on maps between strictly preordered types of preserving the strict ordering
+### The predicate on maps between strict preorders of preserving the strict ordering
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Preordered-Type l1 l2) (Q : Strictly-Preordered-Type l3 l4)
-  (f : type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type Q)
+  (P : Strict-Preorder l1 l2) (Q : Strict-Preorder l3 l4)
+  (f : type-Strict-Preorder P → type-Strict-Preorder Q)
   where
 
-  preserves-strict-order-prop-map-Strictly-Preordered-Type :
+  preserves-strict-order-prop-map-Strict-Preorder :
     Prop (l1 ⊔ l2 ⊔ l4)
-  preserves-strict-order-prop-map-Strictly-Preordered-Type =
+  preserves-strict-order-prop-map-Strict-Preorder =
     Π-Prop
-      ( type-Strictly-Preordered-Type P)
+      ( type-Strict-Preorder P)
       ( λ x →
         Π-Prop
-          ( type-Strictly-Preordered-Type P)
+          ( type-Strict-Preorder P)
           ( λ y →
             hom-Prop
-              ( le-prop-Strictly-Preordered-Type P x y)
-              ( le-prop-Strictly-Preordered-Type Q (f x) (f y))))
+              ( le-prop-Strict-Preorder P x y)
+              ( le-prop-Strict-Preorder Q (f x) (f y))))
 
-  preserves-strict-order-map-Strictly-Preordered-Type :
+  preserves-strict-order-map-Strict-Preorder :
     UU (l1 ⊔ l2 ⊔ l4)
-  preserves-strict-order-map-Strictly-Preordered-Type =
-    type-Prop preserves-strict-order-prop-map-Strictly-Preordered-Type
+  preserves-strict-order-map-Strict-Preorder =
+    type-Prop preserves-strict-order-prop-map-Strict-Preorder
 
-  is-prop-preserves-strict-order-map-Strictly-Preordered-Type :
-    is-prop preserves-strict-order-map-Strictly-Preordered-Type
-  is-prop-preserves-strict-order-map-Strictly-Preordered-Type =
-    is-prop-type-Prop preserves-strict-order-prop-map-Strictly-Preordered-Type
+  is-prop-preserves-strict-order-map-Strict-Preorder :
+    is-prop preserves-strict-order-map-Strict-Preorder
+  is-prop-preserves-strict-order-map-Strict-Preorder =
+    is-prop-type-Prop preserves-strict-order-prop-map-Strict-Preorder
 ```
 
-### The type of strict order preserving maps between strictly preordered types
+### The type of strict order preserving maps between strict preorders
 
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Preordered-Type l1 l2) (Q : Strictly-Preordered-Type l3 l4)
+  (P : Strict-Preorder l1 l2) (Q : Strict-Preorder l3 l4)
   where
 
-  hom-Strictly-Preordered-Type : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  hom-Strictly-Preordered-Type =
-    type-subtype (preserves-strict-order-prop-map-Strictly-Preordered-Type P Q)
+  hom-Strict-Preorder : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  hom-Strict-Preorder =
+    type-subtype (preserves-strict-order-prop-map-Strict-Preorder P Q)
 
 module _
   {l1 l2 l3 l4 : Level}
-  (P : Strictly-Preordered-Type l1 l2) (Q : Strictly-Preordered-Type l3 l4)
-  (f : hom-Strictly-Preordered-Type P Q)
+  (P : Strict-Preorder l1 l2) (Q : Strict-Preorder l3 l4)
+  (f : hom-Strict-Preorder P Q)
   where
 
-  map-hom-Strictly-Preordered-Type :
-    type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type Q
-  map-hom-Strictly-Preordered-Type =
+  map-hom-Strict-Preorder :
+    type-Strict-Preorder P → type-Strict-Preorder Q
+  map-hom-Strict-Preorder =
     pr1 f
 
-  preserves-strict-order-hom-Strictly-Preordered-Type :
-    preserves-strict-order-map-Strictly-Preordered-Type P Q
-      ( map-hom-Strictly-Preordered-Type)
-  preserves-strict-order-hom-Strictly-Preordered-Type =
+  preserves-strict-order-hom-Strict-Preorder :
+    preserves-strict-order-map-Strict-Preorder P Q
+      ( map-hom-Strict-Preorder)
+  preserves-strict-order-hom-Strict-Preorder =
     pr2 f
 ```
 
@@ -105,25 +104,25 @@ module _
   preserves-strict-order-prop-map-Strictly-Preordered-Set :
     Prop (l1 ⊔ l2 ⊔ l4)
   preserves-strict-order-prop-map-Strictly-Preordered-Set =
-    preserves-strict-order-prop-map-Strictly-Preordered-Type
-      ( strictly-preordered-type-Strictly-Preordered-Set P)
-      ( strictly-preordered-type-Strictly-Preordered-Set Q)
+    preserves-strict-order-prop-map-Strict-Preorder
+      ( strict-preorder-Strictly-Preordered-Set P)
+      ( strict-preorder-Strictly-Preordered-Set Q)
       ( f)
 
   preserves-strict-order-map-Strictly-Preordered-Set :
     UU (l1 ⊔ l2 ⊔ l4)
   preserves-strict-order-map-Strictly-Preordered-Set =
-    preserves-strict-order-map-Strictly-Preordered-Type
-      ( strictly-preordered-type-Strictly-Preordered-Set P)
-      ( strictly-preordered-type-Strictly-Preordered-Set Q)
+    preserves-strict-order-map-Strict-Preorder
+      ( strict-preorder-Strictly-Preordered-Set P)
+      ( strict-preorder-Strictly-Preordered-Set Q)
       ( f)
 
   is-prop-preserves-strict-order-map-Strictly-Preordered-Set :
     is-prop preserves-strict-order-map-Strictly-Preordered-Set
   is-prop-preserves-strict-order-map-Strictly-Preordered-Set =
-    is-prop-preserves-strict-order-map-Strictly-Preordered-Type
-      ( strictly-preordered-type-Strictly-Preordered-Set P)
-      ( strictly-preordered-type-Strictly-Preordered-Set Q)
+    is-prop-preserves-strict-order-map-Strict-Preorder
+      ( strict-preorder-Strictly-Preordered-Set P)
+      ( strict-preorder-Strictly-Preordered-Set Q)
       ( f)
 ```
 
diff --git a/src/order-theory/strict-preorders.lagda.md b/src/order-theory/strict-preorders.lagda.md
new file mode 100644
index 0000000000..3751d8916c
--- /dev/null
+++ b/src/order-theory/strict-preorders.lagda.md
@@ -0,0 +1,97 @@
+# Strict preorders
+
+```agda
+module order-theory.strict-preorders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A {{#concept "strict preorder" Agda=Strict-Preorder}} consists of a
+type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued
+in the [propositions](foundation-core.propositions.md), such that the relation
+$<$ is irreflexive and transitive:
+
+- For any $x:A$ we have $x \nle x$.
+- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
+
+Strict preorders satisfy antisymmetry by irreflexivity and
+transitivity.
+
+## Definitions
+
+### The type of strict preorders
+
+```agda
+Strict-Preorder : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Strict-Preorder l1 l2 =
+  Σ ( UU l1)
+    ( λ A →
+      Σ ( Relation-Prop l2 A)
+        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
+
+module _
+  {l1 l2 : Level} (A : Strict-Preorder l1 l2)
+  where
+
+  type-Strict-Preorder :
+    UU l1
+  type-Strict-Preorder =
+    pr1 A
+
+  le-prop-Strict-Preorder :
+    Relation-Prop l2 type-Strict-Preorder
+  le-prop-Strict-Preorder =
+    pr1 (pr2 A)
+
+  le-Strict-Preorder :
+    Relation l2 type-Strict-Preorder
+  le-Strict-Preorder =
+    type-Relation-Prop le-prop-Strict-Preorder
+
+  is-prop-le-Strict-Preorder :
+    (x y : type-Strict-Preorder) →
+    is-prop (le-Strict-Preorder x y)
+  is-prop-le-Strict-Preorder =
+    is-prop-type-Relation-Prop le-prop-Strict-Preorder
+
+  is-irreflexive-le-Strict-Preorder :
+    is-irreflexive le-Strict-Preorder
+  is-irreflexive-le-Strict-Preorder =
+    pr1 (pr2 (pr2 A))
+
+  is-transitive-le-Strict-Preorder :
+    is-transitive le-Strict-Preorder
+  is-transitive-le-Strict-Preorder =
+    pr2 (pr2 (pr2 A))
+```
+
+## Properties
+
+### The ordering of a strict preorder is antisymmetric
+
+```agda
+module _
+  {l1 l2 : Level} (A : Strict-Preorder l1 l2)
+  where
+
+  is-antisymmetric-le-Strict-Preorder :
+    is-antisymmetric (le-Strict-Preorder A)
+  is-antisymmetric-le-Strict-Preorder x y H K =
+    ex-falso
+      ( is-irreflexive-le-Strict-Preorder A x
+        ( is-transitive-le-Strict-Preorder A x y x K H))
+```
diff --git a/src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md b/src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md
new file mode 100644
index 0000000000..e1d3af9685
--- /dev/null
+++ b/src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md
@@ -0,0 +1,168 @@
+# Strictly inflationary maps on a strictly preordered type
+
+```agda
+module order-theory.strictly-inflationary-maps-strict-preorders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import order-theory.strict-order-preserving-maps
+open import order-theory.strict-preorders
+```
+
+</details>
+
+## Idea
+
+A map $f : P → P$ on a
+[strict preorder](order-theory.strict-preorders.md) $P$ is said to be a
+{{#concept "strictly inflationary map" Disambiguation="strict preorder" Agda=strictly-inflationary-map-Strict-Preorder}}
+if the inequality
+
+$$
+  x < f(x)
+$$
+
+holds for any element $x : P$. If $f$ is also
+[order preserving](order-theory.strict-order-preserving-maps.md) we say that $f$
+is a
+{{#concept "strictly inflationary morphism" Disambiguation="strict preorder" Agda=inflationary-hom-Strict-Preorder}}.
+
+## Definitions
+
+### The predicate of being a strictly inflationary map
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strict-Preorder l1 l2)
+  (f : type-Strict-Preorder P → type-Strict-Preorder P)
+  where
+
+  is-strictly-inflationary-map-prop-Strict-Preorder :
+    Prop (l1 ⊔ l2)
+  is-strictly-inflationary-map-prop-Strict-Preorder =
+    Π-Prop
+      ( type-Strict-Preorder P)
+      ( λ x → le-prop-Strict-Preorder P x (f x))
+
+  is-strictly-inflationary-map-Strict-Preorder :
+    UU (l1 ⊔ l2)
+  is-strictly-inflationary-map-Strict-Preorder =
+    type-Prop is-strictly-inflationary-map-prop-Strict-Preorder
+
+  is-prop-is-strictly-inflationary-map-Strict-Preorder :
+    is-prop is-strictly-inflationary-map-Strict-Preorder
+  is-prop-is-strictly-inflationary-map-Strict-Preorder =
+    is-prop-type-Prop is-strictly-inflationary-map-prop-Strict-Preorder
+```
+
+### The type of inflationary maps on a strict preorder
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strict-Preorder l1 l2)
+  where
+
+  strictly-inflationary-map-Strict-Preorder :
+    UU (l1 ⊔ l2)
+  strictly-inflationary-map-Strict-Preorder =
+    type-subtype (is-strictly-inflationary-map-prop-Strict-Preorder P)
+
+module _
+  {l1 l2 : Level} (P : Strict-Preorder l1 l2)
+  (f : strictly-inflationary-map-Strict-Preorder P)
+  where
+
+  map-strictly-inflationary-map-Strict-Preorder :
+    type-Strict-Preorder P → type-Strict-Preorder P
+  map-strictly-inflationary-map-Strict-Preorder =
+    pr1 f
+
+  is-inflationary-strictly-inflationary-map-Strict-Preorder :
+    is-strictly-inflationary-map-Strict-Preorder P
+      ( map-strictly-inflationary-map-Strict-Preorder)
+  is-inflationary-strictly-inflationary-map-Strict-Preorder =
+    pr2 f
+```
+
+### The predicate on order preserving maps of being inflationary
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strict-Preorder l1 l2)
+  (f : hom-Strict-Preorder P P)
+  where
+
+  is-inflationary-prop-hom-Strict-Preorder :
+    Prop (l1 ⊔ l2)
+  is-inflationary-prop-hom-Strict-Preorder =
+    is-strictly-inflationary-map-prop-Strict-Preorder P
+      ( map-hom-Strict-Preorder P P f)
+
+  is-inflationary-hom-Strict-Preorder :
+    UU (l1 ⊔ l2)
+  is-inflationary-hom-Strict-Preorder =
+    is-strictly-inflationary-map-Strict-Preorder P
+      ( map-hom-Strict-Preorder P P f)
+
+  is-prop-is-inflationary-hom-Strict-Preorder :
+    is-prop is-inflationary-hom-Strict-Preorder
+  is-prop-is-inflationary-hom-Strict-Preorder =
+    is-prop-is-strictly-inflationary-map-Strict-Preorder P
+      ( map-hom-Strict-Preorder P P f)
+```
+
+### The type of inflationary morphisms on a strict preorder
+
+```agda
+module _
+  {l1 l2 : Level} (P : Strict-Preorder l1 l2)
+  where
+
+  inflationary-hom-Strict-Preorder :
+    UU (l1 ⊔ l2)
+  inflationary-hom-Strict-Preorder =
+    type-subtype (is-inflationary-prop-hom-Strict-Preorder P)
+
+module _
+  {l1 l2 : Level} (P : Strict-Preorder l1 l2)
+  (f : inflationary-hom-Strict-Preorder P)
+  where
+
+  hom-inflationary-hom-Strict-Preorder :
+    hom-Strict-Preorder P P
+  hom-inflationary-hom-Strict-Preorder =
+    pr1 f
+
+  map-inflationary-hom-Strict-Preorder :
+    type-Strict-Preorder P → type-Strict-Preorder P
+  map-inflationary-hom-Strict-Preorder =
+    map-hom-Strict-Preorder P P
+      ( hom-inflationary-hom-Strict-Preorder)
+
+  preserves-order-inflationary-hom-Strict-Preorder :
+    preserves-strict-order-map-Strict-Preorder P P
+      ( map-inflationary-hom-Strict-Preorder)
+  preserves-order-inflationary-hom-Strict-Preorder =
+    preserves-strict-order-hom-Strict-Preorder P P
+      ( hom-inflationary-hom-Strict-Preorder)
+
+  is-inflationary-inflationary-hom-Strict-Preorder :
+    is-strictly-inflationary-map-Strict-Preorder P
+      ( map-inflationary-hom-Strict-Preorder)
+  is-inflationary-inflationary-hom-Strict-Preorder =
+    pr2 f
+
+  inflationary-map-inflationary-hom-Strict-Preorder :
+    strictly-inflationary-map-Strict-Preorder P
+  pr1 inflationary-map-inflationary-hom-Strict-Preorder =
+    map-inflationary-hom-Strict-Preorder
+  pr2 inflationary-map-inflationary-hom-Strict-Preorder =
+    is-inflationary-inflationary-hom-Strict-Preorder
+```
diff --git a/src/order-theory/strictly-inflationary-maps-strictly-preordered-types.lagda.md b/src/order-theory/strictly-inflationary-maps-strictly-preordered-types.lagda.md
deleted file mode 100644
index edca001001..0000000000
--- a/src/order-theory/strictly-inflationary-maps-strictly-preordered-types.lagda.md
+++ /dev/null
@@ -1,169 +0,0 @@
-# Strictly inflationary maps on a strictly preordered type
-
-```agda
-module order-theory.strictly-inflationary-maps-strictly-preordered-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.dependent-pair-types
-open import foundation.propositions
-open import foundation.subtypes
-open import foundation.universe-levels
-
-open import order-theory.strict-order-preserving-maps
-open import order-theory.strictly-preordered-types
-```
-
-</details>
-
-## Idea
-
-A map $f : P → P$ on a
-[strictly preordered type](order-theory.strictly-preordered-types.md) $P$ is
-said to be a
-{{#concept "strictly inflationary map" Disambiguation="strictly preordered type" Agda=strictly-inflationary-map}}
-if the inequality
-
-$$
-  x < f(x)
-$$
-
-holds for any element $x : P$. If $f$ is also
-[order preserving](order-theory.strict-order-preserving-maps.md) we say that $f$
-is a
-{{#concept "strictly inflationary morphism" Disambiguation="strictly preordered type" Agda=inflationary-hom-Strictly-Preordered-Type}}.
-
-## Definitions
-
-### The predicate of being a strictly inflationary map
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
-  (f : type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P)
-  where
-
-  is-strictly-inflationary-map-prop-Strictly-Preordered-Type :
-    Prop (l1 ⊔ l2)
-  is-strictly-inflationary-map-prop-Strictly-Preordered-Type =
-    Π-Prop
-      ( type-Strictly-Preordered-Type P)
-      ( λ x → le-prop-Strictly-Preordered-Type P x (f x))
-
-  is-strictly-inflationary-map-Strictly-Preordered-Type :
-    UU (l1 ⊔ l2)
-  is-strictly-inflationary-map-Strictly-Preordered-Type =
-    type-Prop is-strictly-inflationary-map-prop-Strictly-Preordered-Type
-
-  is-prop-is-strictly-inflationary-map-Strictly-Preordered-Type :
-    is-prop is-strictly-inflationary-map-Strictly-Preordered-Type
-  is-prop-is-strictly-inflationary-map-Strictly-Preordered-Type =
-    is-prop-type-Prop is-strictly-inflationary-map-prop-Strictly-Preordered-Type
-```
-
-### The type of inflationary maps on a strictly preordered type
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
-  where
-
-  strictly-inflationary-map-Strictly-Preordered-Type :
-    UU (l1 ⊔ l2)
-  strictly-inflationary-map-Strictly-Preordered-Type =
-    type-subtype (is-strictly-inflationary-map-prop-Strictly-Preordered-Type P)
-
-module _
-  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
-  (f : strictly-inflationary-map-Strictly-Preordered-Type P)
-  where
-
-  map-strictly-inflationary-map-Strictly-Preordered-Type :
-    type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P
-  map-strictly-inflationary-map-Strictly-Preordered-Type =
-    pr1 f
-
-  is-inflationary-strictly-inflationary-map-Strictly-Preordered-Type :
-    is-strictly-inflationary-map-Strictly-Preordered-Type P
-      ( map-strictly-inflationary-map-Strictly-Preordered-Type)
-  is-inflationary-strictly-inflationary-map-Strictly-Preordered-Type =
-    pr2 f
-```
-
-### The predicate on order preserving maps of being inflationary
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
-  (f : hom-Strictly-Preordered-Type P P)
-  where
-
-  is-inflationary-prop-hom-Strictly-Preordered-Type :
-    Prop (l1 ⊔ l2)
-  is-inflationary-prop-hom-Strictly-Preordered-Type =
-    is-strictly-inflationary-map-prop-Strictly-Preordered-Type P
-      ( map-hom-Strictly-Preordered-Type P P f)
-
-  is-inflationary-hom-Strictly-Preordered-Type :
-    UU (l1 ⊔ l2)
-  is-inflationary-hom-Strictly-Preordered-Type =
-    is-strictly-inflationary-map-Strictly-Preordered-Type P
-      ( map-hom-Strictly-Preordered-Type P P f)
-
-  is-prop-is-inflationary-hom-Strictly-Preordered-Type :
-    is-prop is-inflationary-hom-Strictly-Preordered-Type
-  is-prop-is-inflationary-hom-Strictly-Preordered-Type =
-    is-prop-is-strictly-inflationary-map-Strictly-Preordered-Type P
-      ( map-hom-Strictly-Preordered-Type P P f)
-```
-
-### The type of inflationary morphisms on a strictly preordered type
-
-```agda
-module _
-  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
-  where
-
-  inflationary-hom-Strictly-Preordered-Type :
-    UU (l1 ⊔ l2)
-  inflationary-hom-Strictly-Preordered-Type =
-    type-subtype (is-inflationary-prop-hom-Strictly-Preordered-Type P)
-
-module _
-  {l1 l2 : Level} (P : Strictly-Preordered-Type l1 l2)
-  (f : inflationary-hom-Strictly-Preordered-Type P)
-  where
-
-  hom-inflationary-hom-Strictly-Preordered-Type :
-    hom-Strictly-Preordered-Type P P
-  hom-inflationary-hom-Strictly-Preordered-Type =
-    pr1 f
-
-  map-inflationary-hom-Strictly-Preordered-Type :
-    type-Strictly-Preordered-Type P → type-Strictly-Preordered-Type P
-  map-inflationary-hom-Strictly-Preordered-Type =
-    map-hom-Strictly-Preordered-Type P P
-      ( hom-inflationary-hom-Strictly-Preordered-Type)
-
-  preserves-order-inflationary-hom-Strictly-Preordered-Type :
-    preserves-strict-order-map-Strictly-Preordered-Type P P
-      ( map-inflationary-hom-Strictly-Preordered-Type)
-  preserves-order-inflationary-hom-Strictly-Preordered-Type =
-    preserves-strict-order-hom-Strictly-Preordered-Type P P
-      ( hom-inflationary-hom-Strictly-Preordered-Type)
-
-  is-inflationary-inflationary-hom-Strictly-Preordered-Type :
-    is-strictly-inflationary-map-Strictly-Preordered-Type P
-      ( map-inflationary-hom-Strictly-Preordered-Type)
-  is-inflationary-inflationary-hom-Strictly-Preordered-Type =
-    pr2 f
-
-  inflationary-map-inflationary-hom-Strictly-Preordered-Type :
-    strictly-inflationary-map-Strictly-Preordered-Type P
-  pr1 inflationary-map-inflationary-hom-Strictly-Preordered-Type =
-    map-inflationary-hom-Strictly-Preordered-Type
-  pr2 inflationary-map-inflationary-hom-Strictly-Preordered-Type =
-    is-inflationary-inflationary-hom-Strictly-Preordered-Type
-```
diff --git a/src/order-theory/strictly-preordered-sets.lagda.md b/src/order-theory/strictly-preordered-sets.lagda.md
index 9ce0db23f5..c639e6fe02 100644
--- a/src/order-theory/strictly-preordered-sets.lagda.md
+++ b/src/order-theory/strictly-preordered-sets.lagda.md
@@ -16,7 +16,7 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
-open import order-theory.strictly-preordered-types
+open import order-theory.strict-preorders
 ```
 
 </details>
@@ -24,9 +24,9 @@ open import order-theory.strictly-preordered-types
 ## Idea
 
 A {{#concept "strictly preordered set" Agda=Strictly-Preordered-Set}} is a
-[strictly preordered type](order-theory.strictly-preordered-types.md) whose
-underlying type is a [set](foundation-core.sets.md). More specifically, a
-strictly preordered set consists of a set $A$, a
+[strictly preordered type](order-theory.strict-preorders.md) whose underlying
+type is a [set](foundation-core.sets.md). More specifically, a strictly
+preordered set consists of a set $A$, a
 [binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the
 [propositions](foundation-core.propositions.md), such that the relation $<$ is
 irreflexive and transitive:
@@ -93,15 +93,15 @@ module _
   is-transitive-le-Strictly-Preordered-Set =
     pr2 (pr2 (pr2 A))
 
-  strictly-preordered-type-Strictly-Preordered-Set :
-    Strictly-Preordered-Type l1 l2
-  pr1 strictly-preordered-type-Strictly-Preordered-Set =
+  strict-preorder-Strictly-Preordered-Set :
+    Strict-Preorder l1 l2
+  pr1 strict-preorder-Strictly-Preordered-Set =
     type-Strictly-Preordered-Set
-  pr1 (pr2 strictly-preordered-type-Strictly-Preordered-Set) =
+  pr1 (pr2 strict-preorder-Strictly-Preordered-Set) =
     le-prop-Strictly-Preordered-Set
-  pr1 (pr2 (pr2 strictly-preordered-type-Strictly-Preordered-Set)) =
+  pr1 (pr2 (pr2 strict-preorder-Strictly-Preordered-Set)) =
     is-irreflexive-le-Strictly-Preordered-Set
-  pr2 (pr2 (pr2 strictly-preordered-type-Strictly-Preordered-Set)) =
+  pr2 (pr2 (pr2 strict-preorder-Strictly-Preordered-Set)) =
     is-transitive-le-Strictly-Preordered-Set
 ```
 
@@ -117,6 +117,6 @@ module _
   is-antisymmetric-le-Strictly-Preordered-Set :
     is-antisymmetric (le-Strictly-Preordered-Set A)
   is-antisymmetric-le-Strictly-Preordered-Set =
-    is-antisymmetric-le-Strictly-Preordered-Type
-      ( strictly-preordered-type-Strictly-Preordered-Set A)
+    is-antisymmetric-le-Strict-Preorder
+      ( strict-preorder-Strictly-Preordered-Set A)
 ```
diff --git a/src/order-theory/strictly-preordered-types.lagda.md b/src/order-theory/strictly-preordered-types.lagda.md
deleted file mode 100644
index e65b5756f1..0000000000
--- a/src/order-theory/strictly-preordered-types.lagda.md
+++ /dev/null
@@ -1,97 +0,0 @@
-# Strictly preordered types
-
-```agda
-module order-theory.strictly-preordered-types where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.binary-relations
-open import foundation.cartesian-product-types
-open import foundation.dependent-pair-types
-open import foundation.empty-types
-open import foundation.negation
-open import foundation.propositions
-open import foundation.universe-levels
-```
-
-</details>
-
-## Idea
-
-A {{#concept "strictly preordered type" Agda=Strictly-Preordered-Type}} consists
-of a type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$
-valued in the [propositions](foundation-core.propositions.md), such that the
-relation $<$ is irreflexive and transitive:
-
-- For any $x:A$ we have $x \nle x$.
-- For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
-
-Strictly preordered types satisfy antisymmetry by irreflexivity and
-transitivity.
-
-## Definitions
-
-### The type of strictly preordered types
-
-```agda
-Strictly-Preordered-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Strictly-Preordered-Type l1 l2 =
-  Σ ( UU l1)
-    ( λ A →
-      Σ ( Relation-Prop l2 A)
-        ( λ R → is-irreflexive-Relation-Prop R × is-transitive-Relation-Prop R))
-
-module _
-  {l1 l2 : Level} (A : Strictly-Preordered-Type l1 l2)
-  where
-
-  type-Strictly-Preordered-Type :
-    UU l1
-  type-Strictly-Preordered-Type =
-    pr1 A
-
-  le-prop-Strictly-Preordered-Type :
-    Relation-Prop l2 type-Strictly-Preordered-Type
-  le-prop-Strictly-Preordered-Type =
-    pr1 (pr2 A)
-
-  le-Strictly-Preordered-Type :
-    Relation l2 type-Strictly-Preordered-Type
-  le-Strictly-Preordered-Type =
-    type-Relation-Prop le-prop-Strictly-Preordered-Type
-
-  is-prop-le-Strictly-Preordered-Type :
-    (x y : type-Strictly-Preordered-Type) →
-    is-prop (le-Strictly-Preordered-Type x y)
-  is-prop-le-Strictly-Preordered-Type =
-    is-prop-type-Relation-Prop le-prop-Strictly-Preordered-Type
-
-  is-irreflexive-le-Strictly-Preordered-Type :
-    is-irreflexive le-Strictly-Preordered-Type
-  is-irreflexive-le-Strictly-Preordered-Type =
-    pr1 (pr2 (pr2 A))
-
-  is-transitive-le-Strictly-Preordered-Type :
-    is-transitive le-Strictly-Preordered-Type
-  is-transitive-le-Strictly-Preordered-Type =
-    pr2 (pr2 (pr2 A))
-```
-
-## Properties
-
-### The ordering of a strictly preordered type is antisymmetric
-
-```agda
-module _
-  {l1 l2 : Level} (A : Strictly-Preordered-Type l1 l2)
-  where
-
-  is-antisymmetric-le-Strictly-Preordered-Type :
-    is-antisymmetric (le-Strictly-Preordered-Type A)
-  is-antisymmetric-le-Strictly-Preordered-Type x y H K =
-    ex-falso
-      ( is-irreflexive-le-Strictly-Preordered-Type A x
-        ( is-transitive-le-Strictly-Preordered-Type A x y x K H))
-```

From c799ca3c25fd2900485cd24204cf16ddef83dd57 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 9 Feb 2025 16:48:23 -0500
Subject: [PATCH 17/17] make pre-commit

---
 src/order-theory.lagda.md                             |  2 +-
 .../strict-order-preserving-maps.lagda.md             |  6 +++---
 src/order-theory/strict-preorders.lagda.md            | 11 +++++------
 ...rictly-inflationary-maps-strict-preorders.lagda.md |  4 ++--
 4 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index 4cf6f35d78..f285009bbb 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -116,9 +116,9 @@ open import order-theory.similarity-of-elements-large-preorders public
 open import order-theory.similarity-of-order-preserving-maps-large-posets public
 open import order-theory.similarity-of-order-preserving-maps-large-preorders public
 open import order-theory.strict-order-preserving-maps public
+open import order-theory.strict-preorders public
 open import order-theory.strictly-inflationary-maps-strict-preorders public
 open import order-theory.strictly-preordered-sets public
-open import order-theory.strict-preorders public
 open import order-theory.subposets public
 open import order-theory.subpreorders public
 open import order-theory.suplattices public
diff --git a/src/order-theory/strict-order-preserving-maps.lagda.md b/src/order-theory/strict-order-preserving-maps.lagda.md
index f0ea631fc1..44b8225347 100644
--- a/src/order-theory/strict-order-preserving-maps.lagda.md
+++ b/src/order-theory/strict-order-preserving-maps.lagda.md
@@ -13,16 +13,16 @@ open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
 
-open import order-theory.strictly-preordered-sets
 open import order-theory.strict-preorders
+open import order-theory.strictly-preordered-sets
 ```
 
 </details>
 
 ## Idea
 
-Consider two [strict preorders](order-theory.strict-preorders.md) $P$
-and $Q$, with orderings $<_P$ and $<_Q$ respectively. A
+Consider two [strict preorders](order-theory.strict-preorders.md) $P$ and $Q$,
+with orderings $<_P$ and $<_Q$ respectively. A
 {{#concept "strict order preserving map" Agda=hom-Strict-Preorder}} consists of
 map $f : P → Q$ between their underlying types such that for any two elements
 $x<_P y$ in $P$ we have $f(x)<_Q f(y)$ in $Q$.
diff --git a/src/order-theory/strict-preorders.lagda.md b/src/order-theory/strict-preorders.lagda.md
index 3751d8916c..071d017b3d 100644
--- a/src/order-theory/strict-preorders.lagda.md
+++ b/src/order-theory/strict-preorders.lagda.md
@@ -20,16 +20,15 @@ open import foundation.universe-levels
 
 ## Idea
 
-A {{#concept "strict preorder" Agda=Strict-Preorder}} consists of a
-type $A$, a [binary relation](foundation.binary-relations.md) $<$ on $A$ valued
-in the [propositions](foundation-core.propositions.md), such that the relation
-$<$ is irreflexive and transitive:
+A {{#concept "strict preorder" Agda=Strict-Preorder}} consists of a type $A$, a
+[binary relation](foundation.binary-relations.md) $<$ on $A$ valued in the
+[propositions](foundation-core.propositions.md), such that the relation $<$ is
+irreflexive and transitive:
 
 - For any $x:A$ we have $x \nle x$.
 - For any $x,y,z:A$ we have $y<z \to x<y \to x<z$.
 
-Strict preorders satisfy antisymmetry by irreflexivity and
-transitivity.
+Strict preorders satisfy antisymmetry by irreflexivity and transitivity.
 
 ## Definitions
 
diff --git a/src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md b/src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md
index e1d3af9685..d8a4672caa 100644
--- a/src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md
+++ b/src/order-theory/strictly-inflationary-maps-strict-preorders.lagda.md
@@ -20,8 +20,8 @@ open import order-theory.strict-preorders
 
 ## Idea
 
-A map $f : P → P$ on a
-[strict preorder](order-theory.strict-preorders.md) $P$ is said to be a
+A map $f : P → P$ on a [strict preorder](order-theory.strict-preorders.md) $P$
+is said to be a
 {{#concept "strictly inflationary map" Disambiguation="strict preorder" Agda=strictly-inflationary-map-Strict-Preorder}}
 if the inequality