Order theory from @spcfox's modal logic

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,47 @@ 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
+```
+
+### 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 +56,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/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