diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index fdb7cae0eb..1de24c0872 100644
--- a/src/order-theory.lagda.md
+++ b/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
 ```
diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md
index 609bdfb03e..99d9811a4b 100644
--- a/src/order-theory/chains-posets.lagda.md
+++ b/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
diff --git a/src/order-theory/chains-preorders.lagda.md b/src/order-theory/chains-preorders.lagda.md
index edcc516f32..f620d50ff1 100644
--- a/src/order-theory/chains-preorders.lagda.md
+++ b/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
diff --git a/src/order-theory/finite-preorders.lagda.md b/src/order-theory/finite-preorders.lagda.md
index 1e5829d497..23c83dcdd3 100644
--- a/src/order-theory/finite-preorders.lagda.md
+++ b/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 _
diff --git a/src/order-theory/finitely-graded-posets.lagda.md b/src/order-theory/finitely-graded-posets.lagda.md
index 35ff0bedae..b4fb4a404b 100644
--- a/src/order-theory/finitely-graded-posets.lagda.md
+++ b/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)
 
diff --git a/src/order-theory/maximal-chains-preorders.lagda.md b/src/order-theory/maximal-chains-preorders.lagda.md
index 7eab487356..f79f5015d3 100644
--- a/src/order-theory/maximal-chains-preorders.lagda.md
+++ b/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)
diff --git a/src/order-theory/subposets.lagda.md b/src/order-theory/subposets.lagda.md
index 9134556681..d7cd52162e 100644
--- a/src/order-theory/subposets.lagda.md
+++ b/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,7 +76,7 @@ module _
   pr2 poset-Subposet = antisymmetric-leq-Subposet
 ```
 
-### Inclusion of sub-posets
+### Inclusion of subposets
 
 ```agda
 module _
@@ -80,13 +84,12 @@ module _
   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
 ```
diff --git a/src/order-theory/subpreorders.lagda.md b/src/order-theory/subpreorders.lagda.md
index 3bdd286fa6..1ca4e51888 100644
--- a/src/order-theory/subpreorders.lagda.md
+++ b/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
 ```
diff --git a/src/order-theory/top-elements-large-posets.lagda.md b/src/order-theory/top-elements-large-posets.lagda.md
index 8031a04f25..f861a1a336 100644
--- a/src/order-theory/top-elements-large-posets.lagda.md
+++ b/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
 
diff --git a/src/order-theory/top-elements-posets.lagda.md b/src/order-theory/top-elements-posets.lagda.md
index 0d092d4e38..658fc977cc 100644
--- a/src/order-theory/top-elements-posets.lagda.md
+++ b/src/order-theory/top-elements-posets.lagda.md
@@ -20,8 +20,10 @@ open import order-theory.top-elements-preorders
 
 ## Idea
 
-A **largest element** in a poset is an element `t` such that `x ≤ t` holds for
-every `x : P`.
+A
+{{#concept "largest element" Disambiguation="in a poset" WD="maximal and minimal elements" WDID=Q1475294 Agda=is-top-element-Poset}}
+in a [poset](order-theory.posets.md) is an element `t` such that `x ≤ t` holds
+for every `x : P`.
 
 ## Definition
 
@@ -30,9 +32,9 @@ module _
   {l1 l2 : Level} (X : Poset l1 l2)
   where
 
-  is-top-element-Poset-Prop : type-Poset X → Prop (l1 ⊔ l2)
-  is-top-element-Poset-Prop =
-    is-top-element-Preorder-Prop (preorder-Poset X)
+  is-top-element-prop-Poset : type-Poset X → Prop (l1 ⊔ l2)
+  is-top-element-prop-Poset =
+    is-top-element-prop-Preorder (preorder-Poset X)
 
   is-top-element-Poset : type-Poset X → UU (l1 ⊔ l2)
   is-top-element-Poset = is-top-element-Preorder (preorder-Poset X)
@@ -49,14 +51,20 @@ module _
     all-elements-equal has-top-element-Poset
   all-elements-equal-has-top-element-Poset (pair x H) (pair y K) =
     eq-type-subtype
-      ( is-top-element-Poset-Prop)
+      ( is-top-element-prop-Poset)
       ( antisymmetric-leq-Poset X x y (K x) (H y))
 
   is-prop-has-top-element-Poset : is-prop has-top-element-Poset
   is-prop-has-top-element-Poset =
     is-prop-all-elements-equal all-elements-equal-has-top-element-Poset
 
-  has-top-element-Poset-Prop : Prop (l1 ⊔ l2)
-  pr1 has-top-element-Poset-Prop = has-top-element-Poset
-  pr2 has-top-element-Poset-Prop = is-prop-has-top-element-Poset
+  has-top-element-prop-Poset : Prop (l1 ⊔ l2)
+  pr1 has-top-element-prop-Poset = has-top-element-Poset
+  pr2 has-top-element-prop-Poset = is-prop-has-top-element-Poset
 ```
+
+## 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
diff --git a/src/order-theory/top-elements-preorders.lagda.md b/src/order-theory/top-elements-preorders.lagda.md
index 93e6197c05..3e024bad5d 100644
--- a/src/order-theory/top-elements-preorders.lagda.md
+++ b/src/order-theory/top-elements-preorders.lagda.md
@@ -18,8 +18,10 @@ open import order-theory.preorders
 
 ## Idea
 
-A **largest element** in a preorder `P` is an element `t` such that `x ≤ t`
-holds for every `x : P`.
+A
+{{#concept "largest element" Disambiguation="in a preorder" WD="maximal and minimal elements" WDID=Q1475294 Agda=is-top-element-Preorder}}
+in a [preorder](order-theory.preorders.md) `P` is an element `t` such that
+`x ≤ t` holds for every `x : P`.
 
 ## Definition
 
@@ -28,18 +30,24 @@ module _
   {l1 l2 : Level} (X : Preorder l1 l2)
   where
 
-  is-top-element-Preorder-Prop : type-Preorder X → Prop (l1 ⊔ l2)
-  is-top-element-Preorder-Prop x =
+  is-top-element-prop-Preorder : type-Preorder X → Prop (l1 ⊔ l2)
+  is-top-element-prop-Preorder x =
     Π-Prop (type-Preorder X) (λ y → leq-Preorder-Prop X y x)
 
   is-top-element-Preorder : type-Preorder X → UU (l1 ⊔ l2)
-  is-top-element-Preorder x = type-Prop (is-top-element-Preorder-Prop x)
+  is-top-element-Preorder x = type-Prop (is-top-element-prop-Preorder x)
 
   is-prop-is-top-element-Preorder :
     (x : type-Preorder X) → is-prop (is-top-element-Preorder x)
   is-prop-is-top-element-Preorder x =
-    is-prop-type-Prop (is-top-element-Preorder-Prop x)
+    is-prop-type-Prop (is-top-element-prop-Preorder x)
 
   has-top-element-Preorder : UU (l1 ⊔ l2)
   has-top-element-Preorder = Σ (type-Preorder X) is-top-element-Preorder
 ```
+
+## 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
diff --git a/src/order-theory/upper-bounds-chains-posets.lagda.md b/src/order-theory/upper-bounds-chains-posets.lagda.md
new file mode 100644
index 0000000000..4326fd679f
--- /dev/null
+++ b/src/order-theory/upper-bounds-chains-posets.lagda.md
@@ -0,0 +1,52 @@
+# Upper bounds of chains in posets
+
+```agda
+module order-theory.upper-bounds-chains-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.existential-quantification
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.propositions
+
+open import order-theory.chains-posets
+open import order-theory.posets
+open import order-theory.upper-bounds-posets
+```
+
+</details>
+
+## Idea
+
+An
+{{#concept "upper bound" Disambiguation="on a chain in a poset" Agda=is-upper-bound-chain-Poset}}
+on a [chain](order-theory.chains-posets.md) `C` in a
+[poset](order-theory.posets.md) `P` is an element `x` such that for every
+element `y` in `C`, `y ≤ x` holds.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level} (X : Poset l1 l2) (C : chain-Poset l3 X)
+  where
+
+  is-upper-bound-chain-prop-Poset : type-Poset X → Prop (l1 ⊔ l2 ⊔ l3)
+  is-upper-bound-chain-prop-Poset =
+    is-upper-bound-family-of-elements-Poset-Prop X
+      ( inclusion-type-chain-Poset X C)
+
+  is-upper-bound-chain-Poset : type-Poset X → UU (l1 ⊔ l2 ⊔ l3)
+  is-upper-bound-chain-Poset = type-Prop ∘ is-upper-bound-chain-prop-Poset
+
+  has-upper-bound-chain-prop-Poset : Prop (l1 ⊔ l2 ⊔ l3)
+  has-upper-bound-chain-prop-Poset =
+    ∃ (type-Poset X) is-upper-bound-chain-prop-Poset
+
+  has-upper-bound-chain-Poset : UU (l1 ⊔ l2 ⊔ l3)
+  has-upper-bound-chain-Poset = type-Prop has-upper-bound-chain-prop-Poset
+```
diff --git a/src/order-theory/zorns-lemma.lagda.md b/src/order-theory/zorns-lemma.lagda.md
new file mode 100644
index 0000000000..a2e403817a
--- /dev/null
+++ b/src/order-theory/zorns-lemma.lagda.md
@@ -0,0 +1,139 @@
+# Zorn's lemma
+
+```agda
+module order-theory.zorns-lemma where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.existential-quantification
+open import foundation.inhabited-types
+open import foundation.law-of-excluded-middle
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.universe-levels
+
+open import foundation-core.coproduct-types
+open import foundation-core.propositions
+
+open import order-theory.chains-posets
+open import order-theory.posets
+open import order-theory.top-elements-posets
+open import order-theory.upper-bounds-chains-posets
+```
+
+</details>
+
+## Idea
+
+{{#concept "Zorn's lemma" Disambiguation="for posets" WD="Zorn's lemma" WDID=Q290810 Agda=zorns-lemma}}
+states that a [poset](order-theory.posets.md) where every
+[chain](order-theory.chains-posets.md) has an
+[upper bound](order-theory.upper-bounds-chains-posets.md) has a
+[top element](order-theory.top-elements-posets.md).
+
+## Statement
+
+### Zorn's lemma
+
+```agda
+module _
+  (l1 l2 l3 : Level)
+  where
+
+  zorns-lemma-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
+  zorns-lemma-Prop =
+    Π-Prop
+      ( Poset l1 l2)
+      ( λ X →
+          function-Prop
+            ( (C : chain-Poset l3 X) → has-upper-bound-chain-Poset X C)
+            ( ∃ (type-Poset X) (is-top-element-prop-Poset X)))
+
+  zorns-lemma : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
+  zorns-lemma = type-Prop zorns-lemma-Prop
+```
+
+### Zorn's lemma for inhabited chains
+
+```agda
+module _
+  (l1 l2 l3 : Level)
+  where
+
+  inhabited-zorns-lemma-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
+  inhabited-zorns-lemma-Prop =
+    Π-Prop
+      ( Poset l1 l2)
+      ( λ X →
+        function-Prop
+          ( is-inhabited (type-Poset X))
+          ( function-Prop
+            ( (C : chain-Poset l3 X) →
+              is-inhabited (type-chain-Poset X C) →
+              has-upper-bound-chain-Poset X C)
+            ( ∃ (type-Poset X) (is-top-element-prop-Poset X))))
+
+  inhabited-zorns-lemma : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
+  inhabited-zorns-lemma = type-Prop inhabited-zorns-lemma-Prop
+```
+
+## Properties
+
+### Zorn's lemma for inhabited chains implies Zorn's lemma
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  where
+
+  zorns-lemma-inhabited-zorns-lemma :
+    inhabited-zorns-lemma l1 l2 l3 → zorns-lemma l1 l2 l3
+  zorns-lemma-inhabited-zorns-lemma zorn X H =
+    zorn X
+      ( apply-universal-property-trunc-Prop
+        ( H ((λ _ → raise-empty-Prop l3) , (λ p → raise-ex-falso l3 (pr2 p))))
+        ( is-inhabited-Prop (type-Poset X))
+        ( λ p → unit-trunc-Prop (pr1 p)))
+      ( λ C _ → H C)
+```
+
+### Assuming the law of excluded middle, Zorn's lemma implies Zorn's lemma for inhabited chains
+
+```agda
+module _
+  {l1 l2 l3 : Level} (lem : LEM (l1 ⊔ l3))
+  where
+
+  inhabited-zorns-lemma-zorns-lemma :
+    zorns-lemma l1 l2 l3 → inhabited-zorns-lemma l1 l2 l3
+  inhabited-zorns-lemma-zorns-lemma zorn X is-inhabited-X H =
+    zorn X chain-upper-bound
+    where
+    chain-upper-bound : (C : chain-Poset l3 X) → has-upper-bound-chain-Poset X C
+    chain-upper-bound C with lem (is-inhabited-Prop (type-chain-Poset X C))
+    ... | inl is-inhabited-C = H C is-inhabited-C
+    ... | inr is-empty-C =
+      apply-universal-property-trunc-Prop
+        ( is-inhabited-X)
+        ( has-upper-bound-chain-prop-Poset X C)
+        ( λ x →
+          intro-exists x (λ w → ex-falso (is-empty-C (unit-trunc-Prop w))))
+
+  iff-inhabited-zorns-lemma-zorns-lemma :
+    type-iff-Prop
+      ( inhabited-zorns-lemma-Prop l1 l2 l3)
+      ( zorns-lemma-Prop l1 l2 l3)
+  iff-inhabited-zorns-lemma-zorns-lemma =
+    ( zorns-lemma-inhabited-zorns-lemma , inhabited-zorns-lemma-zorns-lemma)
+```
+
+## External links
+
+- [Zorn's lemma](https://en.wikipedia.org/wiki/Zorn%27s_lemma) at Wikipedia
+- [Zorn's lemma](https://ncatlab.org/nlab/show/Zorn%27s+lemma) at $n$Lab
+- [Zorn's lemma](https://mathworld.wolfram.com/ZornsLemma.html) at Wolfram
+  MathWorld