Order theory from @spcfox's modal logic (#1205)

Subset of #1146 #1170 

---------

Co-authored-by: spcfox
Co-authored-by: Egbert Rijke <[email protected]>

src/order-theory.lagda.md

@@ -107,9 +107,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,40 +7,49 @@ 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
+## Definitions
+
+### The predicate on subsets of posets to be a chain
 
 ```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 : UU (l1 ⊔ l2 ⊔ l3)
+  is-chain-Subposet = is-chain-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-prop-is-chain-Subposet : is-prop is-chain-Subposet
+  is-prop-is-chain-Subposet = is-prop-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)
+### Chains in posets
 
+```agda
 chain-Poset :
   {l1 l2 : Level} (l : Level) (X : Poset l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l)
 chain-Poset l X = chain-Preorder l (preorder-Poset X)
@@ -49,29 +58,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,31 +21,34 @@ 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
+## Definitions
+
+### The predicate on subsets of preorders to be a chain
 
 ```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 : is-prop is-chain-Subpreorder
+  is-prop-is-chain-Subpreorder = is-prop-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)
+### Chains in preorders
 
+```agda
 chain-Preorder :
   {l1 l2 : Level} (l : Level) (X : Preorder l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l)
 chain-Preorder l X =
@@ -55,32 +58,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/finitely-graded-posets.lagda.md

@@ -403,7 +403,7 @@ module _
 
     is-top-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
     is-top-element-Finitely-Graded-Poset-Prop =
-      is-top-element-Poset-Prop
+      is-top-element-prop-Poset
         ( poset-Finitely-Graded-Poset X)
         ( element-face-Finitely-Graded-Poset X x)
 

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

src/order-theory/subpreorders.lagda.md

@@ -82,16 +82,16 @@ module _
     (T : type-Preorder P → Prop l4)
     where
 
-    inclusion-Subpreorder-Prop : Prop (l1 ⊔ l3 ⊔ l4)
-    inclusion-Subpreorder-Prop =
+    inclusion-prop-Subpreorder : Prop (l1 ⊔ l3 ⊔ l4)
+    inclusion-prop-Subpreorder =
       Π-Prop (type-Preorder P) (λ x → hom-Prop (S x) (T x))
 
     inclusion-Subpreorder : UU (l1 ⊔ l3 ⊔ l4)
-    inclusion-Subpreorder = type-Prop inclusion-Subpreorder-Prop
+    inclusion-Subpreorder = type-Prop inclusion-prop-Subpreorder
 
     is-prop-inclusion-Subpreorder : is-prop inclusion-Subpreorder
     is-prop-inclusion-Subpreorder =
-      is-prop-type-Prop inclusion-Subpreorder-Prop
+      is-prop-type-Prop inclusion-prop-Subpreorder
 
   refl-inclusion-Subpreorder :
     {l3 : Level} → is-reflexive (inclusion-Subpreorder {l3})
@@ -108,7 +108,7 @@ module _
 
   Sub-Preorder : (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
   pr1 (Sub-Preorder l) = type-Preorder P → Prop l
-  pr1 (pr2 (Sub-Preorder l)) = inclusion-Subpreorder-Prop
+  pr1 (pr2 (Sub-Preorder l)) = inclusion-prop-Subpreorder
   pr1 (pr2 (pr2 (Sub-Preorder l))) = refl-inclusion-Subpreorder
   pr2 (pr2 (pr2 (Sub-Preorder l))) = transitive-inclusion-Subpreorder
 ```

src/order-theory/top-elements-large-posets.lagda.md

@@ -17,9 +17,10 @@ open import order-theory.large-posets
 
 ## Idea
 
-We say that a [large poset](order-theory.large-posets.md) `P` has a **largest
-element** if it comes equipped with an element `t : type-Large-Poset P lzero`
-such that `x ≤ t` holds for every `x : P`
+We say that a [large poset](order-theory.large-posets.md) `P` has a
+{{#concept "largest element" Disambiguation="in a large poset" WD="maximal and minimal elements" WDID=Q1475294 Agda=is-top-element-Large-Poset}}
+if it comes equipped with an element `t : type-Large-Poset P lzero` such that
+`x ≤ t` holds for every `x : P`
 
 ## Definition