Order theory from @spcfox's modal logic

src/order-theory.lagda.md

@@ -75,6 +75,7 @@ open import order-theory.lower-sets-large-posets public
 open import order-theory.lower-types-preorders public
 open import order-theory.maximal-chains-posets public
 open import order-theory.maximal-chains-preorders public
+open import order-theory.maximal-elements-posets public
 open import order-theory.meet-semilattices public
 open import order-theory.meet-suplattices public
 open import order-theory.nuclei-large-locales public
@@ -107,9 +108,11 @@ open import order-theory.top-elements-posets public
 open import order-theory.top-elements-preorders public
 open import order-theory.total-orders public
 open import order-theory.total-preorders public
+open import order-theory.upper-bounds-chains-posets public
 open import order-theory.upper-bounds-large-posets public
 open import order-theory.upper-bounds-posets public
 open import order-theory.upper-sets-large-posets public
 open import order-theory.well-founded-orders public
 open import order-theory.well-founded-relations public
+open import order-theory.zorns-lemma public
 ```

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

@@ -7,39 +7,42 @@ module order-theory.chains-posets where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.function-types
 open import foundation.propositions
+open import foundation.subtypes
 open import foundation.universe-levels
 
 open import order-theory.chains-preorders
 open import order-theory.posets
+open import order-theory.subposets
 ```
 
 </details>
 
 ## Idea
 
-A **chain** in a poset `P` is a subtype `S` of `P` such that the ordering of `P`
-restricted to `S` is linear.
+A {{#concept "chain" Disambiguation="in a poset" Agda=chain-Poset}} in a
+[poset](order-theory.posets.md) `P` is a [subtype](foundation-core.subtypes.md)
+`S` of `P` such that the ordering of `P` restricted to `S` is
+[linear](order-theory.total-orders.md).
 
 ## Definition
 
 ```agda
 module _
-  {l1 l2 : Level} (X : Poset l1 l2)
+  {l1 l2 l3 : Level} (X : Poset l1 l2) (S : Subposet l3 X)
   where
 
-  is-chain-Subposet-Prop :
-    {l3 : Level} (S : type-Poset X → Prop l3) → Prop (l1 ⊔ l2 ⊔ l3)
-  is-chain-Subposet-Prop = is-chain-Subpreorder-Prop (preorder-Poset X)
+  is-chain-prop-Subposet : Prop (l1 ⊔ l2 ⊔ l3)
+  is-chain-prop-Subposet = is-chain-prop-Subpreorder (preorder-Poset X) S
 
-  is-chain-Subposet :
-    {l3 : Level} (S : type-Poset X → Prop l3) → UU (l1 ⊔ l2 ⊔ l3)
-  is-chain-Subposet = is-chain-Subpreorder (preorder-Poset X)
+  is-chain-Subposet : UU (l1 ⊔ l2 ⊔ l3)
+  is-chain-Subposet = is-chain-Subpreorder (preorder-Poset X) S
 
-  is-prop-is-chain-Subposet :
-    {l3 : Level} (S : type-Poset X → Prop l3) →
-    is-prop (is-chain-Subposet S)
-  is-prop-is-chain-Subposet = is-prop-is-chain-Subpreorder (preorder-Poset X)
+  is-prop-is-chain-Subposet : is-prop is-chain-Subposet
+  is-prop-is-chain-Subposet = is-prop-is-chain-Subpreorder (preorder-Poset X) S
 
 chain-Poset :
   {l1 l2 : Level} (l : Level) (X : Poset l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l)
@@ -49,29 +52,40 @@ module _
   {l1 l2 l3 : Level} (X : Poset l1 l2) (C : chain-Poset l3 X)
   where
 
-  sub-preorder-chain-Poset : type-Poset X → Prop l3
-  sub-preorder-chain-Poset =
-    sub-preorder-chain-Preorder (preorder-Poset X) C
+  subposet-chain-Poset : Subposet l3 X
+  subposet-chain-Poset =
+    subpreorder-chain-Preorder (preorder-Poset X) C
+
+  is-chain-subposet-chain-Poset :
+    is-chain-Subposet X subposet-chain-Poset
+  is-chain-subposet-chain-Poset =
+    is-chain-subpreorder-chain-Preorder (preorder-Poset X) C
 
   type-chain-Poset : UU (l1 ⊔ l3)
   type-chain-Poset = type-chain-Preorder (preorder-Poset X) C
 
+  inclusion-type-chain-Poset : type-chain-Poset → type-Poset X
+  inclusion-type-chain-Poset =
+    inclusion-subpreorder-chain-Preorder (preorder-Poset X) C
+
 module _
-  {l1 l2 : Level} (X : Poset l1 l2)
+  {l1 l2 l3 l4 : Level} (X : Poset l1 l2)
+  (C : chain-Poset l3 X) (D : chain-Poset l4 X)
   where
 
-  inclusion-chain-Poset-Prop :
-    {l3 l4 : Level} → chain-Poset l3 X → chain-Poset l4 X →
-    Prop (l1 ⊔ l3 ⊔ l4)
-  inclusion-chain-Poset-Prop = inclusion-chain-Preorder-Prop (preorder-Poset X)
+  inclusion-chain-prop-Poset : Prop (l1 ⊔ l3 ⊔ l4)
+  inclusion-chain-prop-Poset =
+    inclusion-prop-chain-Preorder (preorder-Poset X) C D
 
-  inclusion-chain-Poset :
-    {l3 l4 : Level} → chain-Poset l3 X → chain-Poset l4 X → UU (l1 ⊔ l3 ⊔ l4)
-  inclusion-chain-Poset = inclusion-chain-Preorder (preorder-Poset X)
+  inclusion-chain-Poset : UU (l1 ⊔ l3 ⊔ l4)
+  inclusion-chain-Poset = inclusion-chain-Preorder (preorder-Poset X) C D
 
-  is-prop-inclusion-chain-Poset :
-    {l3 l4 : Level} (C : chain-Poset l3 X) (D : chain-Poset l4 X) →
-    is-prop (inclusion-chain-Poset C D)
+  is-prop-inclusion-chain-Poset : is-prop inclusion-chain-Poset
   is-prop-inclusion-chain-Poset =
-    is-prop-inclusion-chain-Preorder (preorder-Poset X)
+    is-prop-inclusion-chain-Preorder (preorder-Poset X) C D
 ```
+
+## External links
+
+- [chain#in order theory](https://ncatlab.org/nlab/show/chain#in_order_theory)
+  at $n$Lab

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

@@ -21,30 +21,27 @@ open import order-theory.total-preorders
 
 ## Idea
 
-A **chain** in a preorder `P` is a subtype `S` of `P` such that the ordering of
-`P` restricted to `S` is linear.
+A {{#concept "chain" Disambiguation="in a preorder" Agda=chain-Preorder}} in a
+[preorder](order-theory.preorders.md) `P` is a
+[subtype](foundation-core.subtypes.md) `S` of `P` such that the ordering of `P`
+restricted to `S` is [linear](order-theory.total-preorders.md).
 
 ## Definition
 
 ```agda
 module _
-  {l1 l2 : Level} (X : Preorder l1 l2)
+  {l1 l2 l3 : Level} (X : Preorder l1 l2) (S : Subpreorder l3 X)
   where
 
-  is-chain-Subpreorder-Prop :
-    {l3 : Level} (S : type-Preorder X → Prop l3) → Prop (l1 ⊔ l2 ⊔ l3)
-  is-chain-Subpreorder-Prop S =
+  is-chain-prop-Subpreorder : Prop (l1 ⊔ l2 ⊔ l3)
+  is-chain-prop-Subpreorder =
     is-total-Preorder-Prop (preorder-Subpreorder X S)
 
-  is-chain-Subpreorder :
-    {l3 : Level} (S : type-Preorder X → Prop l3) → UU (l1 ⊔ l2 ⊔ l3)
-  is-chain-Subpreorder S = type-Prop (is-chain-Subpreorder-Prop S)
+  is-chain-Subpreorder : UU (l1 ⊔ l2 ⊔ l3)
+  is-chain-Subpreorder = type-Prop is-chain-prop-Subpreorder
 
-  is-prop-is-chain-Subpreorder :
-    {l3 : Level} (S : type-Preorder X → Prop l3) →
-    is-prop (is-chain-Subpreorder S)
-  is-prop-is-chain-Subpreorder S =
-    is-prop-type-Prop (is-chain-Subpreorder-Prop S)
+  is-prop-is-chain-Subpreorder : is-prop is-chain-Subpreorder
+  is-prop-is-chain-Subpreorder = is-prop-type-Prop is-chain-prop-Subpreorder
 
 chain-Preorder :
   {l1 l2 : Level} (l : Level) (X : Preorder l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l)
@@ -55,32 +52,41 @@ module _
   {l1 l2 l3 : Level} (X : Preorder l1 l2) (C : chain-Preorder l3 X)
   where
 
-  sub-preorder-chain-Preorder : type-Preorder X → Prop l3
-  sub-preorder-chain-Preorder = pr1 C
+  subpreorder-chain-Preorder : Subpreorder l3 X
+  subpreorder-chain-Preorder = pr1 C
+
+  is-chain-subpreorder-chain-Preorder :
+    is-chain-Subpreorder X subpreorder-chain-Preorder
+  is-chain-subpreorder-chain-Preorder = pr2 C
 
   type-chain-Preorder : UU (l1 ⊔ l3)
-  type-chain-Preorder = type-subtype sub-preorder-chain-Preorder
+  type-chain-Preorder = type-subtype subpreorder-chain-Preorder
+
+  inclusion-subpreorder-chain-Preorder : type-chain-Preorder → type-Preorder X
+  inclusion-subpreorder-chain-Preorder =
+    inclusion-subtype subpreorder-chain-Preorder
 
 module _
-  {l1 l2 : Level} (X : Preorder l1 l2)
+  {l1 l2 l3 l4 : Level} (X : Preorder l1 l2)
+  (C : chain-Preorder l3 X) (D : chain-Preorder l4 X)
   where
 
-  inclusion-chain-Preorder-Prop :
-    {l3 l4 : Level} → chain-Preorder l3 X → chain-Preorder l4 X →
-    Prop (l1 ⊔ l3 ⊔ l4)
-  inclusion-chain-Preorder-Prop C D =
-    inclusion-Subpreorder-Prop X
-      ( sub-preorder-chain-Preorder X C)
-      ( sub-preorder-chain-Preorder X D)
+  inclusion-prop-chain-Preorder : Prop (l1 ⊔ l3 ⊔ l4)
+  inclusion-prop-chain-Preorder =
+    inclusion-prop-Subpreorder X
+      ( subpreorder-chain-Preorder X C)
+      ( subpreorder-chain-Preorder X D)
 
-  inclusion-chain-Preorder :
-    {l3 l4 : Level} → chain-Preorder l3 X → chain-Preorder l4 X →
-    UU (l1 ⊔ l3 ⊔ l4)
-  inclusion-chain-Preorder C D = type-Prop (inclusion-chain-Preorder-Prop C D)
+  inclusion-chain-Preorder : UU (l1 ⊔ l3 ⊔ l4)
+  inclusion-chain-Preorder = type-Prop inclusion-prop-chain-Preorder
 
   is-prop-inclusion-chain-Preorder :
-    {l3 l4 : Level} (C : chain-Preorder l3 X) (D : chain-Preorder l4 X) →
-    is-prop (inclusion-chain-Preorder C D)
-  is-prop-inclusion-chain-Preorder C D =
-    is-prop-type-Prop (inclusion-chain-Preorder-Prop C D)
+    is-prop inclusion-chain-Preorder
+  is-prop-inclusion-chain-Preorder =
+    is-prop-type-Prop inclusion-prop-chain-Preorder
 ```
+
+## External links
+
+- [chain#in order theory](https://ncatlab.org/nlab/show/chain#in_order_theory)
+  at $n$Lab

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

@@ -173,7 +173,7 @@ module _
   pr2 is-finite-preorder-Preorder-𝔽 = is-decidable-leq-Preorder-𝔽
 ```
 
-### Decidable sub-preorders of finite preorders
+### Decidable subpreorders of finite preorders
 
 ```agda
 module _

src/order-theory/maximal-chains-preorders.lagda.md

@@ -37,7 +37,7 @@ module _
       ( λ D →
         function-Prop
           ( inclusion-chain-Preorder X C D)
-          ( inclusion-chain-Preorder-Prop X D C))
+          ( inclusion-prop-chain-Preorder X D C))
 
   is-maximal-chain-Preorder :
     {l3 : Level} → chain-Preorder l3 X → UU (l1 ⊔ l2 ⊔ lsuc l3)

src/order-theory/maximal-elements-posets.lagda.md

@@ -0,0 +1,55 @@
+# Maximal elements in posets
+
+```agda
+module order-theory.maximal-elements-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.propositions
+
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "maximal" Disambiguation="element in a poset" WD="maximal and minimal elements" WDID=Q1475294 Agda=is-maximal-element-Poset}}
+element in a [poset](order-theory.posets.md) is an element `y` such that every
+other element `x` that is greater than it `y ≤ x` is
+[equal](foundation-core.identity-types.md) to it `y = x`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (X : Poset l1 l2)
+  where
+
+  is-maximal-element-prop-Poset : type-Poset X → Prop (l1 ⊔ l2)
+  is-maximal-element-prop-Poset x =
+    Π-Prop
+      ( type-Poset X)
+      ( λ y → function-Prop (leq-Poset X x y) (y ＝ x , is-set-type-Poset X y x))
+
+  is-maximal-element-Poset : type-Poset X → UU (l1 ⊔ l2)
+  is-maximal-element-Poset x = type-Prop (is-maximal-element-prop-Poset x)
+
+  is-prop-is-maximal-element-Poset :
+    (x : type-Poset X) → is-prop (is-maximal-element-Poset x)
+  is-prop-is-maximal-element-Poset x =
+    is-prop-type-Prop (is-maximal-element-prop-Poset x)
+```
+
+## External links
+
+- [Maximal and minimal elements](https://en.wikipedia.org/wiki/Maximal_and_minimal_elements)
+  at Wikipedia
+- [maximal element](https://ncatlab.org/nlab/show/maximal+element) at $n$Lab

src/order-theory/subposets.lagda.md

@@ -30,8 +30,12 @@ ordering on `P`, subposets have again the structure of a poset.
 ### Subposets
 
 ```agda
+Subposet :
+  {l1 l2 : Level} (l3 : Level) → Poset l1 l2 → UU (l1 ⊔ lsuc l3)
+Subposet l3 P = Subpreorder l3 (preorder-Poset P)
+
 module _
-  {l1 l2 l3 : Level} (X : Poset l1 l2) (S : type-Poset X → Prop l3)
+  {l1 l2 l3 : Level} (X : Poset l1 l2) (S : Subposet l3 X)
   where
 
   type-Subposet : UU (l1 ⊔ l3)
@@ -72,21 +76,20 @@ module _
   pr2 poset-Subposet = antisymmetric-leq-Subposet
 ```
 
-### Inclusion of sub-posets
+### Inclusion of subposets
 
 ```agda
 module _
   {l1 l2 : Level} (X : Poset l1 l2)
   where
 
   module _
-    {l3 l4 : Level} (S : type-Poset X → Prop l3)
-    (T : type-Poset X → Prop l4)
+    {l3 l4 : Level} (S : Subposet l3 X) (T : Subposet l4 X)
     where
 
-    inclusion-Subposet-Prop : Prop (l1 ⊔ l3 ⊔ l4)
-    inclusion-Subposet-Prop =
-      inclusion-Subpreorder-Prop (preorder-Poset X) S T
+    inclusion-prop-Subposet : Prop (l1 ⊔ l3 ⊔ l4)
+    inclusion-prop-Subposet =
+      inclusion-prop-Subpreorder (preorder-Poset X) S T
 
     inclusion-Subposet : UU (l1 ⊔ l3 ⊔ l4)
     inclusion-Subposet = inclusion-Subpreorder (preorder-Poset X) S T
@@ -96,23 +99,21 @@ module _
       is-prop-inclusion-Subpreorder (preorder-Poset X) S T
 
   refl-inclusion-Subposet :
-    {l3 : Level} (S : type-Poset X → Prop l3) →
-    inclusion-Subposet S S
+    {l3 : Level} (S : Subposet l3 X) → inclusion-Subposet S S
   refl-inclusion-Subposet = refl-inclusion-Subpreorder (preorder-Poset X)
 
   transitive-inclusion-Subposet :
-    {l3 l4 l5 : Level} (S : type-Poset X → Prop l3)
-    (T : type-Poset X → Prop l4)
-    (U : type-Poset X → Prop l5) →
+    {l3 l4 l5 : Level}
+    (S : Subposet l3 X) (T : Subposet l4 X) (U : Subposet l5 X) →
     inclusion-Subposet T U →
     inclusion-Subposet S T →
     inclusion-Subposet S U
   transitive-inclusion-Subposet =
     transitive-inclusion-Subpreorder (preorder-Poset X)
 
-  sub-poset-Preorder : (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
-  pr1 (sub-poset-Preorder l) = type-Poset X → Prop l
-  pr1 (pr2 (sub-poset-Preorder l)) = inclusion-Subposet-Prop
-  pr1 (pr2 (pr2 (sub-poset-Preorder l))) = refl-inclusion-Subposet
-  pr2 (pr2 (pr2 (sub-poset-Preorder l))) = transitive-inclusion-Subposet
+  subposet-Preorder : (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
+  pr1 (subposet-Preorder l) = Subposet l X
+  pr1 (pr2 (subposet-Preorder l)) = inclusion-prop-Subposet
+  pr1 (pr2 (pr2 (subposet-Preorder l))) = refl-inclusion-Subposet
+  pr2 (pr2 (pr2 (subposet-Preorder l))) = transitive-inclusion-Subposet
 ```