review chains

UniMath · Oct 19, 2024 · a4212d8 · a4212d8
1 parent b7d5e58
commit a4212d8
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md
@@ -28,7 +28,7 @@ A {{#concept "chain" Disambiguation="in a poset" Agda=chain-Poset}} in a
 `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
 
@@ -93,5 +93,5 @@ module _
 
 ## External links
 
-- [chain#in order theory](https://ncatlab.org/nlab/show/chain#in_order_theory)
+- [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
@@ -26,7 +26,9 @@ A {{#concept "chain" Disambiguation="in a preorder" Agda=chain-Preorder}} in 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 _
@@ -42,7 +44,11 @@ module _
 
   is-prop-is-chain-Subpreorder : is-prop is-chain-Subpreorder
   is-prop-is-chain-Subpreorder = is-prop-type-Prop is-chain-prop-Subpreorder
+```
 
+### Chains in preorders
+
+```agda
 chain-Preorder :
   {l1 l2 : Level} (l : Level) (X : Preorder l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l)
 chain-Preorder l X =
@@ -88,5 +94,5 @@ module _
 
 ## External links
 
-- [chain#in order theory](https://ncatlab.org/nlab/show/chain#in_order_theory)
+- [chain, in order theory](https://ncatlab.org/nlab/show/chain#in_order_theory)
   at $n$Lab