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)))
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
diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index a5f5985c0f..f285009bbb 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,8 @@ 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.inflattices public
 open import order-theory.inhabited-chains-posets public
 open import order-theory.inhabited-chains-preorders public
@@ -111,6 +115,10 @@ 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.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.subposets public
 open import order-theory.subpreorders public
 open import order-theory.suplattices public
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/deflationary-maps-posets.lagda.md b/src/order-theory/deflationary-maps-posets.lagda.md
new file mode 100644
index 0000000000..ffeb8f4da5
--- /dev/null
+++ b/src/order-theory/deflationary-maps-posets.lagda.md
@@ -0,0 +1,151 @@
+# 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 a
+{{#concept "deflationary map" Disambiguation="poset" Agda=deflationary-map-Poset}}
+if the inequality
+
+$$
+  f(x) ≤ 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 a
+{{#concept "deflationary morphism" Disambiguation="poset" Agda=deflationary-hom-Poset}}.
+
+## Definitions
+
+### The predicate of being a 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..508b702878
--- /dev/null
+++ b/src/order-theory/deflationary-maps-preorders.lagda.md
@@ -0,0 +1,150 @@
+# 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 a
+{{#concept "deflationary map" Disambiguation="preorder" Agda=deflationary-map-Preorder}}
+if the inequality
+
+$$
+  f(x) ≤ 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 a
+{{#concept "deflationary morphism" Disambiguation="preorder" Agda=deflationary-hom-Preorder}}.
+
+## Definitions
+
+### The predicate of being a 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..00c3374a3b
--- /dev/null
+++ b/src/order-theory/inflationary-maps-posets.lagda.md
@@ -0,0 +1,151 @@
+# 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 ≤ 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..aa2d482b97
--- /dev/null
+++ b/src/order-theory/inflationary-maps-preorders.lagda.md
@@ -0,0 +1,151 @@
+# 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 ≤ 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/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..44b8225347
--- /dev/null
+++ b/src/order-theory/strict-order-preserving-maps.lagda.md
@@ -0,0 +1,157 @@
+# 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.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
+{{#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 strict preorders of preserving the strict ordering
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (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-Strict-Preorder :
+    Prop (l1 ⊔ l2 ⊔ l4)
+  preserves-strict-order-prop-map-Strict-Preorder =
+    Π-Prop
+      ( type-Strict-Preorder P)
+      ( λ x →
+        Π-Prop
+          ( type-Strict-Preorder P)
+          ( λ y →
+            hom-Prop
+              ( le-prop-Strict-Preorder P x y)
+              ( le-prop-Strict-Preorder Q (f x) (f y))))
+
+  preserves-strict-order-map-Strict-Preorder :
+    UU (l1 ⊔ l2 ⊔ l4)
+  preserves-strict-order-map-Strict-Preorder =
+    type-Prop preserves-strict-order-prop-map-Strict-Preorder
+
+  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 strict preorders
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strict-Preorder l1 l2) (Q : Strict-Preorder l3 l4)
+  where
+
+  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 : Strict-Preorder l1 l2) (Q : Strict-Preorder l3 l4)
+  (f : hom-Strict-Preorder P Q)
+  where
+
+  map-hom-Strict-Preorder :
+    type-Strict-Preorder P → type-Strict-Preorder Q
+  map-hom-Strict-Preorder =
+    pr1 f
+
+  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
+```
+
+### The predicate on maps between strictly preordered sets of preserving the strict ordering
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (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-Preordered-Set :
+    Prop (l1 ⊔ l2 ⊔ l4)
+  preserves-strict-order-prop-map-Strictly-Preordered-Set =
+    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-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-Strict-Preorder
+      ( strict-preorder-Strictly-Preordered-Set P)
+      ( strict-preorder-Strictly-Preordered-Set Q)
+      ( f)
+```
+
+### The type of strict order preserving maps between strictly preordered sets
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (P : Strictly-Preordered-Set l1 l2) (Q : Strictly-Preordered-Set l3 l4)
+  where
+
+  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-Preordered-Set l1 l2) (Q : Strictly-Preordered-Set l3 l4)
+  (f : hom-Strictly-Preordered-Set P Q)
+  where
+
+  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-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/strict-preorders.lagda.md b/src/order-theory/strict-preorders.lagda.md
new file mode 100644
index 0000000000..071d017b3d
--- /dev/null
+++ b/src/order-theory/strict-preorders.lagda.md
@@ -0,0 +1,96 @@
+# 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..d8a4672caa
--- /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-preordered-sets.lagda.md b/src/order-theory/strictly-preordered-sets.lagda.md
new file mode 100644
index 0000000000..c639e6fe02
--- /dev/null
+++ b/src/order-theory/strictly-preordered-sets.lagda.md
@@ -0,0 +1,122 @@
+# 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.strict-preorders
+```
+
+</details>
+
+## Idea
+
+A {{#concept "strictly preordered set" Agda=Strictly-Preordered-Set}} is 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:
+
+- 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))
+
+  strict-preorder-Strictly-Preordered-Set :
+    Strict-Preorder l1 l2
+  pr1 strict-preorder-Strictly-Preordered-Set =
+    type-Strictly-Preordered-Set
+  pr1 (pr2 strict-preorder-Strictly-Preordered-Set) =
+    le-prop-Strictly-Preordered-Set
+  pr1 (pr2 (pr2 strict-preorder-Strictly-Preordered-Set)) =
+    is-irreflexive-le-Strictly-Preordered-Set
+  pr2 (pr2 (pr2 strict-preorder-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-Strict-Preorder
+      ( strict-preorder-Strictly-Preordered-Set A)
+```