Strict preorders

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)))

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

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

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))

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 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
+```

src/order-theory/deflationary-maps-preorders.lagda.md

@@ -0,0 +1,151 @@
+# 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
+```