diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
index f2e8762494..d53f0377e8 100644
--- a/src/category-theory.lagda.md
+++ b/src/category-theory.lagda.md
@@ -16,6 +16,7 @@ module category-theory where
 open import category-theory.adjunctions-large-precategories public
 open import category-theory.anafunctors-categories public
 open import category-theory.anafunctors-precategories public
+open import category-theory.augmented-simplex-category public
 open import category-theory.categories public
 open import category-theory.category-of-functors public
 open import category-theory.category-of-functors-from-small-to-large-categories public
@@ -29,6 +30,8 @@ open import category-theory.dependent-products-of-large-categories public
 open import category-theory.dependent-products-of-large-precategories public
 open import category-theory.dependent-products-of-precategories public
 open import category-theory.discrete-categories public
+open import category-theory.embedding-maps-precategories public
+open import category-theory.embeddings-precategories public
 open import category-theory.endomorphisms-in-categories public
 open import category-theory.endomorphisms-in-precategories public
 open import category-theory.epimorphisms-in-large-precategories public
@@ -37,6 +40,7 @@ open import category-theory.equivalences-of-large-precategories public
 open import category-theory.equivalences-of-precategories public
 open import category-theory.exponential-objects-precategories public
 open import category-theory.faithful-functors-precategories public
+open import category-theory.faithful-maps-precategories public
 open import category-theory.full-large-subcategories public
 open import category-theory.full-large-subprecategories public
 open import category-theory.function-categories public
@@ -96,6 +100,7 @@ open import category-theory.representable-functors-large-precategories public
 open import category-theory.representable-functors-precategories public
 open import category-theory.representing-arrow-category public
 open import category-theory.sieves-in-categories public
+open import category-theory.simplex-category public
 open import category-theory.slice-precategories public
 open import category-theory.subprecategories public
 open import category-theory.terminal-objects-precategories public
diff --git a/src/category-theory/augmented-simplex-category.lagda.md b/src/category-theory/augmented-simplex-category.lagda.md
new file mode 100644
index 0000000000..03eaf5a276
--- /dev/null
+++ b/src/category-theory/augmented-simplex-category.lagda.md
@@ -0,0 +1,143 @@
+# The augmented simplex category
+
+```agda
+module category-theory.augmented-simplex-category where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.precategories
+
+open import elementary-number-theory.inequality-standard-finite-types
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-posets
+```
+
+</details>
+
+## Idea
+
+**The augmented simplex category** is the category consisting of
+[finite total orders](order-theory.finite-total-orders.md) and
+[order-preserving maps](order-theory.order-preserving-maps-posets.md). However,
+we define it as the category whose objects are
+[natural numbers](elementary-number-theory.natural-numbers.md) and whose
+hom-[sets](foundation-core.sets.md) `hom n m` are order-preserving maps between
+the [standard finite types](univalent-combinatorics.standard-finite-types.md)
+`Fin n` to `Fin m` [equipped](foundation.structure.md) with the
+[standard ordering](elementary-number-theory.inequality-standard-finite-types.md),
+and then show that it is
+[equivalent](category-theory.equivalences-of-precategories.md) to the former.
+
+## Definition
+
+### The augmented simplex precategory
+
+```agda
+obj-augmented-simplex-Category : UU lzero
+obj-augmented-simplex-Category = ℕ
+
+hom-set-augmented-simplex-Category :
+  obj-augmented-simplex-Category → obj-augmented-simplex-Category → Set lzero
+hom-set-augmented-simplex-Category n m =
+  hom-set-Poset (Fin-Poset n) (Fin-Poset m)
+
+hom-augmented-simplex-Category :
+  obj-augmented-simplex-Category → obj-augmented-simplex-Category → UU lzero
+hom-augmented-simplex-Category n m =
+  type-Set (hom-set-augmented-simplex-Category n m)
+
+comp-hom-augmented-simplex-Category :
+  {n m r : obj-augmented-simplex-Category} →
+  hom-augmented-simplex-Category m r →
+  hom-augmented-simplex-Category n m →
+  hom-augmented-simplex-Category n r
+comp-hom-augmented-simplex-Category {n} {m} {r} =
+  comp-hom-Poset (Fin-Poset n) (Fin-Poset m) (Fin-Poset r)
+
+associative-comp-hom-augmented-simplex-Category :
+  {n m r s : obj-augmented-simplex-Category}
+  (h : hom-augmented-simplex-Category r s)
+  (g : hom-augmented-simplex-Category m r)
+  (f : hom-augmented-simplex-Category n m) →
+  ( comp-hom-augmented-simplex-Category {n} {m} {s}
+    ( comp-hom-augmented-simplex-Category {m} {r} {s} h g)
+    ( f)) ＝
+  ( comp-hom-augmented-simplex-Category {n} {r} {s}
+    ( h)
+    ( comp-hom-augmented-simplex-Category {n} {m} {r} g f))
+associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} =
+  associative-comp-hom-Poset
+    ( Fin-Poset n)
+    ( Fin-Poset m)
+    ( Fin-Poset r)
+    ( Fin-Poset s)
+
+associative-composition-structure-augmented-simplex-Category :
+  associative-composition-structure-Set hom-set-augmented-simplex-Category
+pr1 associative-composition-structure-augmented-simplex-Category {n} {m} {r} =
+  comp-hom-augmented-simplex-Category {n} {m} {r}
+pr2
+  associative-composition-structure-augmented-simplex-Category {n} {m} {r} {s} =
+  associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s}
+
+id-hom-augmented-simplex-Category :
+  (n : obj-augmented-simplex-Category) → hom-augmented-simplex-Category n n
+id-hom-augmented-simplex-Category n = id-hom-Poset (Fin-Poset n)
+
+left-unit-law-comp-hom-augmented-simplex-Category :
+  {n m : obj-augmented-simplex-Category}
+  (f : hom-augmented-simplex-Category n m) →
+  comp-hom-augmented-simplex-Category {n} {m} {m}
+    ( id-hom-augmented-simplex-Category m)
+    ( f) ＝
+  f
+left-unit-law-comp-hom-augmented-simplex-Category {n} {m} =
+  left-unit-law-comp-hom-Poset (Fin-Poset n) (Fin-Poset m)
+
+right-unit-law-comp-hom-augmented-simplex-Category :
+  {n m : obj-augmented-simplex-Category}
+  (f : hom-augmented-simplex-Category n m) →
+  comp-hom-augmented-simplex-Category {n} {n} {m}
+    ( f)
+    ( id-hom-augmented-simplex-Category n) ＝
+  f
+right-unit-law-comp-hom-augmented-simplex-Category {n} {m} =
+  right-unit-law-comp-hom-Poset (Fin-Poset n) (Fin-Poset m)
+
+is-unital-composition-structure-augmented-simplex-Category :
+  is-unital-composition-structure-Set
+    ( hom-set-augmented-simplex-Category)
+    ( associative-composition-structure-augmented-simplex-Category)
+pr1 is-unital-composition-structure-augmented-simplex-Category =
+  id-hom-augmented-simplex-Category
+pr1 (pr2 is-unital-composition-structure-augmented-simplex-Category) {n} {m} =
+  left-unit-law-comp-hom-augmented-simplex-Category {n} {m}
+pr2 (pr2 is-unital-composition-structure-augmented-simplex-Category) {n} {m} =
+  right-unit-law-comp-hom-augmented-simplex-Category {n} {m}
+
+augmented-simplex-Precategory : Precategory lzero lzero
+pr1 augmented-simplex-Precategory = obj-augmented-simplex-Category
+pr1 (pr2 augmented-simplex-Precategory) = hom-set-augmented-simplex-Category
+pr1 (pr2 (pr2 augmented-simplex-Precategory)) =
+  associative-composition-structure-augmented-simplex-Category
+pr2 (pr2 (pr2 augmented-simplex-Precategory)) =
+  is-unital-composition-structure-augmented-simplex-Category
+```
+
+### The augmented simplex category
+
+It remains to be formalized that the augmented simplex category is univalent.
+
+## Properties
+
+### The augmented simplex category is equivalent to the category of finite total orders
+
+This remains to be formalized.
diff --git a/src/category-theory/embedding-maps-precategories.lagda.md b/src/category-theory/embedding-maps-precategories.lagda.md
new file mode 100644
index 0000000000..3b3ea5e582
--- /dev/null
+++ b/src/category-theory/embedding-maps-precategories.lagda.md
@@ -0,0 +1,88 @@
+# Embedding maps between precategories
+
+```agda
+module category-theory.embedding-maps-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.faithful-maps-precategories
+open import category-theory.functors-precategories
+open import category-theory.maps-precategories
+open import category-theory.precategories
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.injective-maps
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [map](category-theory.maps-precategories.md) between
+[precategories](category-theory.precategories.md) `C` and `D` is an **embedding
+map** if it's an embedding on objects and
+[faithful](category-theory.faithful-maps-precategories.md). Hence embedding maps
+are maps that are embeddings on objects and hom-sets.
+
+Note that for a map of precategories to be called _an embedding_, it must also
+be a [functor](category-theory.functors-precategories.md). This notion is
+considered in
+[`category-theory.embeddings-precategories`](category-theory.embeddings-precategories.md).
+
+## Definition
+
+### The predicate of being an embedding map on maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : map-Precategory C D)
+  where
+
+  is-embedding-map-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-map-prop-map-Precategory =
+    prod-Prop
+      ( is-emb-Prop (obj-map-Precategory C D F))
+      ( is-faithful-prop-map-Precategory C D F)
+
+  is-embedding-map-map-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-map-map-Precategory =
+    type-Prop is-embedding-map-prop-map-Precategory
+
+  is-prop-is-embedding-map-map-Precategory :
+    is-prop is-embedding-map-map-Precategory
+  is-prop-is-embedding-map-map-Precategory =
+    is-prop-type-Prop is-embedding-map-prop-map-Precategory
+```
+
+### The type of embedding maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  where
+
+  embedding-map-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  embedding-map-Precategory =
+    Σ (map-Precategory C D) (is-embedding-map-map-Precategory C D)
+
+  map-embedding-map-Precategory :
+    embedding-map-Precategory → map-Precategory C D
+  map-embedding-map-Precategory = pr1
+
+  is-embedding-map-embedding-map-Precategory :
+    (e : embedding-map-Precategory) →
+    is-embedding-map-map-Precategory C D (map-embedding-map-Precategory e)
+  is-embedding-map-embedding-map-Precategory = pr2
+```
diff --git a/src/category-theory/embeddings-precategories.lagda.md b/src/category-theory/embeddings-precategories.lagda.md
new file mode 100644
index 0000000000..1614c05880
--- /dev/null
+++ b/src/category-theory/embeddings-precategories.lagda.md
@@ -0,0 +1,105 @@
+# Embeddings between precategories
+
+```agda
+module category-theory.embeddings-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.embedding-maps-precategories
+open import category-theory.functors-precategories
+open import category-theory.maps-precategories
+open import category-theory.precategories
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [functor](category-theory.functors-precategories.md) between
+[precategories](category-theory.precategories.md) `C` and `D` is an
+**embedding** if it's an embedding on objects and
+[faithful](category-theory.faithful-functors-precategories.md). Hence embeddings
+are functors that are embeddings on objects and hom-sets.
+
+## Definition
+
+### The predicate of being an embedding on maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : map-Precategory C D)
+  where
+
+  is-embedding-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-prop-map-Precategory =
+    prod-Prop
+      ( is-functor-prop-map-Precategory C D F)
+      ( is-embedding-map-prop-map-Precategory C D F)
+
+  is-embedding-map-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-map-Precategory =
+    type-Prop is-embedding-prop-map-Precategory
+
+  is-prop-is-embedding-map-Precategory : is-prop is-embedding-map-Precategory
+  is-prop-is-embedding-map-Precategory =
+    is-prop-type-Prop is-embedding-prop-map-Precategory
+```
+
+### The predicate of being an embedding on functors between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : functor-Precategory C D)
+  where
+
+  is-embedding-prop-functor-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-prop-functor-Precategory =
+    is-embedding-map-prop-map-Precategory C D (map-functor-Precategory C D F)
+
+  is-embedding-functor-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-functor-Precategory =
+    type-Prop is-embedding-prop-functor-Precategory
+
+  is-prop-is-embedding-functor-Precategory :
+    is-prop is-embedding-functor-Precategory
+  is-prop-is-embedding-functor-Precategory =
+    is-prop-type-Prop is-embedding-prop-functor-Precategory
+```
+
+### The type of embeddings between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  where
+
+  embedding-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  embedding-Precategory =
+    Σ (functor-Precategory C D) (is-embedding-functor-Precategory C D)
+
+  functor-embedding-Precategory :
+    embedding-Precategory → functor-Precategory C D
+  functor-embedding-Precategory = pr1
+
+  is-embedding-embedding-Precategory :
+    (e : embedding-Precategory) →
+    is-embedding-functor-Precategory C D (functor-embedding-Precategory e)
+  is-embedding-embedding-Precategory = pr2
+```
diff --git a/src/category-theory/faithful-functors-precategories.lagda.md b/src/category-theory/faithful-functors-precategories.lagda.md
index 0816a06279..06d56f459d 100644
--- a/src/category-theory/faithful-functors-precategories.lagda.md
+++ b/src/category-theory/faithful-functors-precategories.lagda.md
@@ -7,6 +7,7 @@ module category-theory.faithful-functors-precategories where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.faithful-maps-precategories
 open import category-theory.functors-precategories
 open import category-theory.maps-precategories
 open import category-theory.precategories
@@ -33,29 +34,6 @@ in terms of embeddings because this is the notion that generalizes.
 
 ## Definition
 
-### The predicate of being faithful on maps between precategories
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level}
-  (C : Precategory l1 l2)
-  (D : Precategory l3 l4)
-  (F : map-Precategory C D)
-  where
-
-  is-faithful-map-Precategory : UU (l1 ⊔ l2 ⊔ l4)
-  is-faithful-map-Precategory =
-    (x y : obj-Precategory C) → is-emb (hom-map-Precategory C D F {x} {y})
-
-  is-prop-is-faithful-map-Precategory : is-prop is-faithful-map-Precategory
-  is-prop-is-faithful-map-Precategory =
-    is-prop-Π² (λ x y → is-prop-is-emb (hom-map-Precategory C D F {x} {y}))
-
-  is-faithful-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
-  pr1 is-faithful-prop-map-Precategory = is-faithful-map-Precategory
-  pr2 is-faithful-prop-map-Precategory = is-prop-is-faithful-map-Precategory
-```
-
 ### The predicate of being faithful on functors between precategories
 
 ```agda
@@ -80,36 +58,7 @@ module _
     is-faithful-prop-map-Precategory C D (map-functor-Precategory C D F)
 ```
 
-### The predicate of being injective on hom-sets on maps between precategories
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level}
-  (C : Precategory l1 l2)
-  (D : Precategory l3 l4)
-  (F : map-Precategory C D)
-  where
-
-  is-injective-hom-map-Precategory : UU (l1 ⊔ l2 ⊔ l4)
-  is-injective-hom-map-Precategory =
-    (x y : obj-Precategory C) → is-injective (hom-map-Precategory C D F {x} {y})
-
-  is-prop-is-injective-hom-map-Precategory :
-    is-prop is-injective-hom-map-Precategory
-  is-prop-is-injective-hom-map-Precategory =
-    is-prop-Π²
-      ( λ x y →
-        is-prop-is-injective
-          ( is-set-hom-Precategory C x y)
-          ( hom-map-Precategory C D F {x} {y}))
-
-  is-injective-hom-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
-  pr1 is-injective-hom-prop-map-Precategory = is-injective-hom-map-Precategory
-  pr2 is-injective-hom-prop-map-Precategory =
-    is-prop-is-injective-hom-map-Precategory
-```
-
-### The predicate of being injective on hom-sets on functors between precategories
+### The predicate of being faithful on functors between precategories
 
 ```agda
 module _
@@ -137,65 +86,6 @@ module _
 
 ## Properties
 
-### A map of precategories is faithful if and only if it is injective on hom-sets
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level}
-  (C : Precategory l1 l2)
-  (D : Precategory l3 l4)
-  (F : map-Precategory C D)
-  where
-
-  is-injective-hom-is-faithful-map-Precategory :
-    is-faithful-map-Precategory C D F →
-    is-injective-hom-map-Precategory C D F
-  is-injective-hom-is-faithful-map-Precategory is-faithful-F x y =
-    is-injective-is-emb (is-faithful-F x y)
-
-  is-faithful-is-injective-hom-map-Precategory :
-    is-injective-hom-map-Precategory C D F →
-    is-faithful-map-Precategory C D F
-  is-faithful-is-injective-hom-map-Precategory is-injective-hom-F x y =
-    is-emb-is-injective
-      ( is-set-hom-Precategory D
-        ( obj-map-Precategory C D F x)
-        ( obj-map-Precategory C D F y))
-      ( is-injective-hom-F x y)
-
-  is-equiv-is-injective-hom-is-faithful-map-Precategory :
-    is-equiv is-injective-hom-is-faithful-map-Precategory
-  is-equiv-is-injective-hom-is-faithful-map-Precategory =
-    is-equiv-is-prop
-      ( is-prop-is-faithful-map-Precategory C D F)
-      ( is-prop-is-injective-hom-map-Precategory C D F)
-      ( is-faithful-is-injective-hom-map-Precategory)
-
-  is-equiv-is-faithful-is-injective-hom-map-Precategory :
-    is-equiv is-faithful-is-injective-hom-map-Precategory
-  is-equiv-is-faithful-is-injective-hom-map-Precategory =
-    is-equiv-is-prop
-      ( is-prop-is-injective-hom-map-Precategory C D F)
-      ( is-prop-is-faithful-map-Precategory C D F)
-      ( is-injective-hom-is-faithful-map-Precategory)
-
-  equiv-is-injective-hom-is-faithful-map-Precategory :
-    is-faithful-map-Precategory C D F ≃
-    is-injective-hom-map-Precategory C D F
-  pr1 equiv-is-injective-hom-is-faithful-map-Precategory =
-    is-injective-hom-is-faithful-map-Precategory
-  pr2 equiv-is-injective-hom-is-faithful-map-Precategory =
-    is-equiv-is-injective-hom-is-faithful-map-Precategory
-
-  equiv-is-faithful-is-injective-hom-map-Precategory :
-    is-injective-hom-map-Precategory C D F ≃
-    is-faithful-map-Precategory C D F
-  pr1 equiv-is-faithful-is-injective-hom-map-Precategory =
-    is-faithful-is-injective-hom-map-Precategory
-  pr2 equiv-is-faithful-is-injective-hom-map-Precategory =
-    is-equiv-is-faithful-is-injective-hom-map-Precategory
-```
-
 ### A functor of precategories is faithful if and only if it is injective on hom-sets
 
 ```agda
diff --git a/src/category-theory/faithful-maps-precategories.lagda.md b/src/category-theory/faithful-maps-precategories.lagda.md
new file mode 100644
index 0000000000..644445effd
--- /dev/null
+++ b/src/category-theory/faithful-maps-precategories.lagda.md
@@ -0,0 +1,151 @@
+# Faithful maps between precategories
+
+```agda
+module category-theory.faithful-maps-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.functors-precategories
+open import category-theory.maps-precategories
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.injective-maps
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [map](category-theory.maps-precategories.md) between
+[precategories](category-theory.precategories.md) `C` and `D` is **faithful** if
+its an [embedding](foundation-core.embeddings.md) on hom-sets.
+
+Note that embeddings on [sets](foundation-core.sets.md) happen to coincide with
+[injections](foundation.injective-maps.md), but we define it in terms of the
+stronger notion, as this is the notion that generalizes.
+
+## Definition
+
+### The predicate of being faithful on maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : map-Precategory C D)
+  where
+
+  is-faithful-map-Precategory : UU (l1 ⊔ l2 ⊔ l4)
+  is-faithful-map-Precategory =
+    (x y : obj-Precategory C) → is-emb (hom-map-Precategory C D F {x} {y})
+
+  is-prop-is-faithful-map-Precategory : is-prop is-faithful-map-Precategory
+  is-prop-is-faithful-map-Precategory =
+    is-prop-Π² (λ x y → is-prop-is-emb (hom-map-Precategory C D F {x} {y}))
+
+  is-faithful-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
+  pr1 is-faithful-prop-map-Precategory = is-faithful-map-Precategory
+  pr2 is-faithful-prop-map-Precategory = is-prop-is-faithful-map-Precategory
+```
+
+### The predicate of being injective on hom-sets on maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : map-Precategory C D)
+  where
+
+  is-injective-hom-map-Precategory : UU (l1 ⊔ l2 ⊔ l4)
+  is-injective-hom-map-Precategory =
+    (x y : obj-Precategory C) → is-injective (hom-map-Precategory C D F {x} {y})
+
+  is-prop-is-injective-hom-map-Precategory :
+    is-prop is-injective-hom-map-Precategory
+  is-prop-is-injective-hom-map-Precategory =
+    is-prop-Π²
+      ( λ x y →
+        is-prop-is-injective
+          ( is-set-hom-Precategory C x y)
+          ( hom-map-Precategory C D F {x} {y}))
+
+  is-injective-hom-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
+  pr1 is-injective-hom-prop-map-Precategory = is-injective-hom-map-Precategory
+  pr2 is-injective-hom-prop-map-Precategory =
+    is-prop-is-injective-hom-map-Precategory
+```
+
+## Properties
+
+### A map of precategories is faithful if and only if it is injective on hom-sets
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : map-Precategory C D)
+  where
+
+  is-injective-hom-is-faithful-map-Precategory :
+    is-faithful-map-Precategory C D F →
+    is-injective-hom-map-Precategory C D F
+  is-injective-hom-is-faithful-map-Precategory is-faithful-F x y =
+    is-injective-is-emb (is-faithful-F x y)
+
+  is-faithful-is-injective-hom-map-Precategory :
+    is-injective-hom-map-Precategory C D F →
+    is-faithful-map-Precategory C D F
+  is-faithful-is-injective-hom-map-Precategory is-injective-hom-F x y =
+    is-emb-is-injective
+      ( is-set-hom-Precategory D
+        ( obj-map-Precategory C D F x)
+        ( obj-map-Precategory C D F y))
+      ( is-injective-hom-F x y)
+
+  is-equiv-is-injective-hom-is-faithful-map-Precategory :
+    is-equiv is-injective-hom-is-faithful-map-Precategory
+  is-equiv-is-injective-hom-is-faithful-map-Precategory =
+    is-equiv-is-prop
+      ( is-prop-is-faithful-map-Precategory C D F)
+      ( is-prop-is-injective-hom-map-Precategory C D F)
+      ( is-faithful-is-injective-hom-map-Precategory)
+
+  is-equiv-is-faithful-is-injective-hom-map-Precategory :
+    is-equiv is-faithful-is-injective-hom-map-Precategory
+  is-equiv-is-faithful-is-injective-hom-map-Precategory =
+    is-equiv-is-prop
+      ( is-prop-is-injective-hom-map-Precategory C D F)
+      ( is-prop-is-faithful-map-Precategory C D F)
+      ( is-injective-hom-is-faithful-map-Precategory)
+
+  equiv-is-injective-hom-is-faithful-map-Precategory :
+    is-faithful-map-Precategory C D F ≃
+    is-injective-hom-map-Precategory C D F
+  pr1 equiv-is-injective-hom-is-faithful-map-Precategory =
+    is-injective-hom-is-faithful-map-Precategory
+  pr2 equiv-is-injective-hom-is-faithful-map-Precategory =
+    is-equiv-is-injective-hom-is-faithful-map-Precategory
+
+  equiv-is-faithful-is-injective-hom-map-Precategory :
+    is-injective-hom-map-Precategory C D F ≃
+    is-faithful-map-Precategory C D F
+  pr1 equiv-is-faithful-is-injective-hom-map-Precategory =
+    is-faithful-is-injective-hom-map-Precategory
+  pr2 equiv-is-faithful-is-injective-hom-map-Precategory =
+    is-equiv-is-faithful-is-injective-hom-map-Precategory
+```
+
+## See also
+
+- [Faithful functors between precategories](category-theory.faithful-functors-precategories.md)
diff --git a/src/category-theory/precategories.lagda.md b/src/category-theory/precategories.lagda.md
index 68dae96c7f..e6804555a4 100644
--- a/src/category-theory/precategories.lagda.md
+++ b/src/category-theory/precategories.lagda.md
@@ -22,12 +22,12 @@ open import foundation.universe-levels
 
 ## Idea
 
-A precategory in Homotopy Type Theory consists of:
+A **precategory** in Homotopy Type Theory consists of:
 
 - a type `A` of objects,
-- for each pair of objects `x y : A`, a set of morphisms `hom x y : Set`,
-  together with a composition operation `_∘_ : hom y z → hom x y → hom x z` such
-  that:
+- for each pair of objects `x y : A`, a [set](foundation-core.sets.md) of
+  morphisms `hom x y : Set`, together with a composition operation
+  `_∘_ : hom y z → hom x y → hom x z` such that:
 - `(h ∘ g) ∘ f = h ∘ (g ∘ f)` for any morphisms `h : hom z w`, `g : hom y z` and
   `f : hom x y`,
 - for each object `x : A` there is a morphism `id_x : hom x x` such that
diff --git a/src/category-theory/simplex-category.lagda.md b/src/category-theory/simplex-category.lagda.md
new file mode 100644
index 0000000000..d711836f67
--- /dev/null
+++ b/src/category-theory/simplex-category.lagda.md
@@ -0,0 +1,145 @@
+# The simplex category
+
+```agda
+module category-theory.simplex-category where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.precategories
+
+open import elementary-number-theory.inequality-standard-finite-types
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-posets
+```
+
+</details>
+
+## Idea
+
+**The simplex category** is the category consisting of inhabited finite total
+orders and
+[order-preserving maps](order-theory.order-preserving-maps-posets.md). However,
+we define it as the category whose objects are
+[natural numbers](elementary-number-theory.natural-numbers.md) and whose
+hom-[sets](foundation-core.sets.md) `hom n m` are order-preserving maps between
+the [standard finite types](univalent-combinatorics.standard-finite-types.md)
+`Fin (succ-ℕ n)` to `Fin (succ-ℕ m)` [equipped](foundation.structure.md) with
+the
+[standard ordering](elementary-number-theory.inequality-standard-finite-types.md),
+and then show that it is
+[equivalent](category-theory.equivalences-of-precategories.md) to the former.
+
+## Definition
+
+### The simplex precategory
+
+```agda
+obj-simplex-Category : UU lzero
+obj-simplex-Category = ℕ
+
+hom-set-simplex-Category :
+  obj-simplex-Category → obj-simplex-Category → Set lzero
+hom-set-simplex-Category n m =
+  hom-set-Poset (Fin-Poset (succ-ℕ n)) (Fin-Poset (succ-ℕ m))
+
+hom-simplex-Category :
+  obj-simplex-Category → obj-simplex-Category → UU lzero
+hom-simplex-Category n m = type-Set (hom-set-simplex-Category n m)
+
+comp-hom-simplex-Category :
+  {n m r : obj-simplex-Category} →
+  hom-simplex-Category m r → hom-simplex-Category n m → hom-simplex-Category n r
+comp-hom-simplex-Category {n} {m} {r} =
+  comp-hom-Poset
+    ( Fin-Poset (succ-ℕ n))
+    ( Fin-Poset (succ-ℕ m))
+    ( Fin-Poset (succ-ℕ r))
+
+associative-comp-hom-simplex-Category :
+  {n m r s : obj-simplex-Category}
+  (h : hom-simplex-Category r s)
+  (g : hom-simplex-Category m r)
+  (f : hom-simplex-Category n m) →
+  ( comp-hom-simplex-Category {n} {m} {s}
+    ( comp-hom-simplex-Category {m} {r} {s} h g)
+    ( f)) ＝
+  ( comp-hom-simplex-Category {n} {r} {s}
+    ( h)
+    ( comp-hom-simplex-Category {n} {m} {r} g f))
+associative-comp-hom-simplex-Category {n} {m} {r} {s} =
+  associative-comp-hom-Poset
+    ( Fin-Poset (succ-ℕ n))
+    ( Fin-Poset (succ-ℕ m))
+    ( Fin-Poset (succ-ℕ r))
+    ( Fin-Poset (succ-ℕ s))
+
+associative-composition-structure-simplex-Category :
+  associative-composition-structure-Set hom-set-simplex-Category
+pr1 associative-composition-structure-simplex-Category {n} {m} {r} =
+  comp-hom-simplex-Category {n} {m} {r}
+pr2 associative-composition-structure-simplex-Category {n} {m} {r} {s} =
+  associative-comp-hom-simplex-Category {n} {m} {r} {s}
+
+id-hom-simplex-Category : (n : obj-simplex-Category) → hom-simplex-Category n n
+id-hom-simplex-Category n = id-hom-Poset (Fin-Poset (succ-ℕ n))
+
+left-unit-law-comp-hom-simplex-Category :
+  {n m : obj-simplex-Category} (f : hom-simplex-Category n m) →
+  comp-hom-simplex-Category {n} {m} {m} (id-hom-simplex-Category m) f ＝ f
+left-unit-law-comp-hom-simplex-Category {n} {m} =
+  left-unit-law-comp-hom-Poset (Fin-Poset (succ-ℕ n)) (Fin-Poset (succ-ℕ m))
+
+right-unit-law-comp-hom-simplex-Category :
+  {n m : obj-simplex-Category} (f : hom-simplex-Category n m) →
+  comp-hom-simplex-Category {n} {n} {m} f (id-hom-simplex-Category n) ＝ f
+right-unit-law-comp-hom-simplex-Category {n} {m} =
+  right-unit-law-comp-hom-Poset (Fin-Poset (succ-ℕ n)) (Fin-Poset (succ-ℕ m))
+
+is-unital-composition-structure-simplex-Category :
+  is-unital-composition-structure-Set
+    ( hom-set-simplex-Category)
+    ( associative-composition-structure-simplex-Category)
+pr1 is-unital-composition-structure-simplex-Category = id-hom-simplex-Category
+pr1 (pr2 is-unital-composition-structure-simplex-Category) {n} {m} =
+  left-unit-law-comp-hom-simplex-Category {n} {m}
+pr2 (pr2 is-unital-composition-structure-simplex-Category) {n} {m} =
+  right-unit-law-comp-hom-simplex-Category {n} {m}
+
+simplex-Precategory : Precategory lzero lzero
+pr1 simplex-Precategory = obj-simplex-Category
+pr1 (pr2 simplex-Precategory) = hom-set-simplex-Category
+pr1 (pr2 (pr2 simplex-Precategory)) =
+  associative-composition-structure-simplex-Category
+pr2 (pr2 (pr2 simplex-Precategory)) =
+  is-unital-composition-structure-simplex-Category
+```
+
+### The simplex category
+
+It remains to be formalized that the simplex category is univalent.
+
+## Properties
+
+### The simplex category is equivalent to the category of inhabited finite total orders
+
+This remains to be formalized.
+
+### The simplex category has a face map and degeneracy unique factorization system
+
+This remains to be formalized.
+
+### The simplex category has a degeneracy and face map unique factorization system
+
+This remains to be formalized.
+
+### There is a unique non-trivial involution on the simplex category
+
+This remains to be formalized.
diff --git a/src/category-theory/subprecategories.lagda.md b/src/category-theory/subprecategories.lagda.md
index 7882df6624..4026e9bfd0 100644
--- a/src/category-theory/subprecategories.lagda.md
+++ b/src/category-theory/subprecategories.lagda.md
@@ -7,7 +7,9 @@ module category-theory.subprecategories where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.embeddings-precategories
 open import category-theory.faithful-functors-precategories
+open import category-theory.faithful-maps-precategories
 open import category-theory.functors-precategories
 open import category-theory.maps-precategories
 open import category-theory.precategories
@@ -381,7 +383,7 @@ module _
 
 ## Properties
 
-### The inclusion functor is faithful and an embedding on objects
+### The inclusion functor is an embedding
 
 ```agda
 module _
@@ -390,31 +392,46 @@ module _
   (P : Subprecategory l3 l4 C)
   where
 
-  is-faithful-inclusion-map-Precategory :
+  is-faithful-inclusion-map-Subprecategory :
     is-faithful-map-Precategory
       ( precategory-Subprecategory C P)
       ( C)
       ( inclusion-map-Subprecategory C P)
-  is-faithful-inclusion-map-Precategory x y =
+  is-faithful-inclusion-map-Subprecategory x y =
     is-emb-inclusion-subtype
       ( subtype-hom-Subprecategory C P
         ( inclusion-obj-Subprecategory C P x)
         ( inclusion-obj-Subprecategory C P y))
 
-  is-faithful-inclusion-functor-Precategory :
+  is-faithful-inclusion-functor-Subprecategory :
     is-faithful-functor-Precategory
       ( precategory-Subprecategory C P)
       ( C)
       ( inclusion-functor-Subprecategory C P)
-  is-faithful-inclusion-functor-Precategory =
-    is-faithful-inclusion-map-Precategory
+  is-faithful-inclusion-functor-Subprecategory =
+    is-faithful-inclusion-map-Subprecategory
 
-  is-emb-obj-inclusion-functor-Precategory :
+  is-emb-obj-inclusion-functor-Subprecategory :
     is-emb
       ( obj-functor-Precategory
         ( precategory-Subprecategory C P)
         ( C)
         ( inclusion-functor-Subprecategory C P))
-  is-emb-obj-inclusion-functor-Precategory =
+  is-emb-obj-inclusion-functor-Subprecategory =
     is-emb-inclusion-subtype (subtype-obj-Subprecategory C P)
+
+  is-embedding-inclusion-functor-Subprecategory :
+    is-embedding-functor-Precategory
+      ( precategory-Subprecategory C P)
+      ( C)
+      ( inclusion-functor-Subprecategory C P)
+  pr1 is-embedding-inclusion-functor-Subprecategory =
+    is-emb-obj-inclusion-functor-Subprecategory
+  pr2 is-embedding-inclusion-functor-Subprecategory =
+    is-faithful-inclusion-functor-Subprecategory
+
+  embedding-Subprecategory :
+    embedding-Precategory (precategory-Subprecategory C P) C
+  pr1 embedding-Subprecategory = inclusion-functor-Subprecategory C P
+  pr2 embedding-Subprecategory = is-embedding-inclusion-functor-Subprecategory
 ```
diff --git a/src/finite-group-theory/finite-semigroups.lagda.md b/src/finite-group-theory/finite-semigroups.lagda.md
index 41e1c80077..95c63559fb 100644
--- a/src/finite-group-theory/finite-semigroups.lagda.md
+++ b/src/finite-group-theory/finite-semigroups.lagda.md
@@ -150,8 +150,7 @@ is-π-finite-Semigroup-of-Order {l} k n =
             ( λ X →
               is-proof-irrelevant-is-prop
                 ( is-prop-is-set _)
-                ( is-set-is-finite
-                  ( is-finite-has-cardinality n (pr2 X))))) ∘e
+                ( is-set-is-finite (is-finite-has-cardinality n (pr2 X))))) ∘e
           ( equiv-right-swap-Σ))
         ( λ X → id-equiv)) ∘e
       ( equiv-right-swap-Σ
diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index e8dd83ea59..63bb2e593b 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -30,6 +30,7 @@ open import order-theory.distributive-lattices public
 open import order-theory.finite-coverings-locales public
 open import order-theory.finite-posets public
 open import order-theory.finite-preorders public
+open import order-theory.finite-total-orders public
 open import order-theory.finitely-graded-posets public
 open import order-theory.frames public
 open import order-theory.galois-connections public
@@ -45,6 +46,7 @@ open import order-theory.homomorphisms-meet-semilattices public
 open import order-theory.homomorphisms-meet-sup-lattices public
 open import order-theory.homomorphisms-sup-lattices public
 open import order-theory.ideals-preorders public
+open import order-theory.inhabited-finite-total-orders public
 open import order-theory.interval-subposets public
 open import order-theory.join-semilattices public
 open import order-theory.large-frames public
@@ -78,6 +80,12 @@ open import order-theory.order-preserving-maps-posets public
 open import order-theory.order-preserving-maps-preorders public
 open import order-theory.posets public
 open import order-theory.powers-of-large-locales public
+open import order-theory.precategory-of-decidable-total-orders public
+open import order-theory.precategory-of-finite-posets public
+open import order-theory.precategory-of-finite-total-orders public
+open import order-theory.precategory-of-inhabited-finite-total-orders public
+open import order-theory.precategory-of-posets public
+open import order-theory.precategory-of-total-orders public
 open import order-theory.preorders public
 open import order-theory.reflective-galois-connections-large-posets public
 open import order-theory.similarity-of-elements-large-posets public
diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md
index b39c7659d1..fcbb19892f 100644
--- a/src/order-theory/decidable-total-orders.lagda.md
+++ b/src/order-theory/decidable-total-orders.lagda.md
@@ -8,7 +8,6 @@ module order-theory.decidable-total-orders where
 
 ```agda
 open import foundation.binary-relations
-open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
@@ -34,10 +33,27 @@ which the inequality [relation](foundation.binary-relations.md) is
 
 ## Definitions
 
+### The predicate on posets of being decidable total orders
+
+```agda
+is-decidable-total-prop-Poset : {l1 l2 : Level} → Poset l1 l2 → Prop (l1 ⊔ l2)
+is-decidable-total-prop-Poset P =
+  prod-Prop (is-total-Poset-Prop P) (is-decidable-leq-Poset-Prop P)
+
+is-decidable-total-Poset : {l1 l2 : Level} → Poset l1 l2 → UU (l1 ⊔ l2)
+is-decidable-total-Poset P = type-Prop (is-decidable-total-prop-Poset P)
+
+is-prop-is-decidable-total-Poset :
+  {l1 l2 : Level} (P : Poset l1 l2) → is-prop (is-decidable-total-Poset P)
+is-prop-is-decidable-total-Poset P =
+  is-prop-type-Prop (is-decidable-total-prop-Poset P)
+```
+
+### The type of decidable total orders
+
 ```agda
 Decidable-Total-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Decidable-Total-Order l1 l2 =
-  Σ (Poset l1 l2) (λ P → is-total-Poset P × is-decidable-leq-Poset P)
+Decidable-Total-Order l1 l2 = Σ (Poset l1 l2) (is-decidable-total-Poset)
 
 module _
   {l1 l2 : Level} (P : Decidable-Total-Order l1 l2)
diff --git a/src/order-theory/finite-posets.lagda.md b/src/order-theory/finite-posets.lagda.md
index 5ac41e6e17..299060d532 100644
--- a/src/order-theory/finite-posets.lagda.md
+++ b/src/order-theory/finite-posets.lagda.md
@@ -9,11 +9,13 @@ module order-theory.finite-posets where
 ```agda
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.propositions
 open import foundation.universe-levels
 
 open import order-theory.finite-preorders
 open import order-theory.posets
+open import order-theory.preorders
 
 open import univalent-combinatorics.finite-types
 ```
@@ -22,8 +24,9 @@ open import univalent-combinatorics.finite-types
 
 ## Definitions
 
-A **finite poset** is a poset of which the underlying type is finite, and of
-which the ordering relation is decidable.
+A **finite poset** is a [poset](order-theory.posets.md) of which the underlying
+type is [finite](univalent-combinatorics.finite-types.md), and of which the
+ordering relation is [decidable](foundation.decidable-relations.md).
 
 ```agda
 module _
@@ -45,8 +48,7 @@ module _
     is-finite-type-is-finite-Preorder (preorder-Poset P)
 
   is-decidable-leq-is-finite-Poset :
-    is-finite-Poset →
-    (x y : type-Poset P) → is-decidable (leq-Poset P x y)
+    is-finite-Poset → (x y : type-Poset P) → is-decidable (leq-Poset P x y)
   is-decidable-leq-is-finite-Poset =
     is-decidable-leq-is-finite-Preorder (preorder-Poset P)
 
@@ -54,4 +56,19 @@ Poset-𝔽 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
 Poset-𝔽 l1 l2 =
   Σ ( Preorder-𝔽 l1 l2)
     ( λ P → is-antisymmetric-leq-Preorder (preorder-Preorder-𝔽 P))
+
+preorder-𝔽-Poset-𝔽 : {l1 l2 : Level} → Poset-𝔽 l1 l2 → Preorder-𝔽 l1 l2
+preorder-𝔽-Poset-𝔽 = pr1
+
+preorder-Poset-𝔽 : {l1 l2 : Level} → Poset-𝔽 l1 l2 → Preorder l1 l2
+preorder-Poset-𝔽 = preorder-Preorder-𝔽 ∘ pr1
+
+is-antisymmetric-leq-Poset-𝔽 :
+  {l1 l2 : Level} (P : Poset-𝔽 l1 l2) →
+  is-antisymmetric-leq-Preorder (preorder-Poset-𝔽 P)
+is-antisymmetric-leq-Poset-𝔽 = pr2
+
+poset-Poset-𝔽 : {l1 l2 : Level} → Poset-𝔽 l1 l2 → Poset l1 l2
+pr1 (poset-Poset-𝔽 P) = preorder-Poset-𝔽 P
+pr2 (poset-Poset-𝔽 P) = is-antisymmetric-leq-Poset-𝔽 P
 ```
diff --git a/src/order-theory/finite-preorders.lagda.md b/src/order-theory/finite-preorders.lagda.md
index 91c3f601ef..5043ea8a9d 100644
--- a/src/order-theory/finite-preorders.lagda.md
+++ b/src/order-theory/finite-preorders.lagda.md
@@ -35,8 +35,9 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-We say that a preorder `P` is **finite** if `P` has finitely many elements and
-the ordering relation on `P` is decidable.
+We say that a [preorder](order-theory.preorders.md) `P` is **finite** if `P` has
+[finitely many elements](univalent-combinatorics.finite-types.md) and the
+ordering relation on `P` is [decidable](foundation.decidable-relations.md).
 
 ```agda
 module _
diff --git a/src/order-theory/finite-total-orders.lagda.md b/src/order-theory/finite-total-orders.lagda.md
new file mode 100644
index 0000000000..5d960e0ae0
--- /dev/null
+++ b/src/order-theory/finite-total-orders.lagda.md
@@ -0,0 +1,90 @@
+# Finite total orders
+
+```agda
+module order-theory.finite-total-orders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import order-theory.finite-posets
+open import order-theory.finite-preorders
+open import order-theory.posets
+open import order-theory.total-orders
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Definitions
+
+A **finite total order** is a [total order](order-theory.total-orders.md) of
+which the underlying type is [finite](univalent-combinatorics.finite-types.md),
+and of which the ordering relation is
+[decidable](foundation.decidable-relations.md).
+
+```agda
+module _
+  {l1 l2 : Level} (P : Total-Order l1 l2)
+  where
+
+  is-finite-Total-Order-Prop : Prop (l1 ⊔ l2)
+  is-finite-Total-Order-Prop = is-finite-Poset-Prop (poset-Total-Order P)
+
+  is-finite-Total-Order : UU (l1 ⊔ l2)
+  is-finite-Total-Order = is-finite-Poset (poset-Total-Order P)
+
+  is-prop-is-finite-Total-Order : is-prop is-finite-Total-Order
+  is-prop-is-finite-Total-Order =
+    is-prop-is-finite-Poset (poset-Total-Order P)
+
+  is-finite-type-is-finite-Total-Order :
+    is-finite-Total-Order → is-finite (type-Total-Order P)
+  is-finite-type-is-finite-Total-Order =
+    is-finite-type-is-finite-Poset (poset-Total-Order P)
+
+  is-decidable-leq-is-finite-Total-Order :
+    is-finite-Total-Order →
+    (x y : type-Total-Order P) → is-decidable (leq-Total-Order P x y)
+  is-decidable-leq-is-finite-Total-Order =
+    is-decidable-leq-is-finite-Poset (poset-Total-Order P)
+
+is-finite-total-order-Poset-Prop :
+  {l1 l2 : Level} (P : Poset l1 l2) → Prop (l1 ⊔ l2)
+is-finite-total-order-Poset-Prop P =
+  prod-Prop
+    ( is-total-Poset-Prop P)
+    ( is-finite-Poset-Prop P)
+
+Total-Order-𝔽 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Total-Order-𝔽 l1 l2 =
+  Σ ( Poset-𝔽 l1 l2)
+    ( λ P → is-total-Poset (poset-Poset-𝔽 P))
+
+poset-𝔽-Total-Order-𝔽 : {l1 l2 : Level} → Total-Order-𝔽 l1 l2 → Poset-𝔽 l1 l2
+poset-𝔽-Total-Order-𝔽 = pr1
+
+poset-Total-Order-𝔽 : {l1 l2 : Level} → Total-Order-𝔽 l1 l2 → Poset l1 l2
+poset-Total-Order-𝔽 = poset-Poset-𝔽 ∘ poset-𝔽-Total-Order-𝔽
+
+is-total-Total-Order-𝔽 :
+  {l1 l2 : Level} (P : Total-Order-𝔽 l1 l2) →
+  is-total-Poset (poset-Total-Order-𝔽 P)
+is-total-Total-Order-𝔽 = pr2
+
+total-order-Total-Order-𝔽 :
+  {l1 l2 : Level} → Total-Order-𝔽 l1 l2 → Total-Order l1 l2
+pr1 (total-order-Total-Order-𝔽 P) = poset-Total-Order-𝔽 P
+pr2 (total-order-Total-Order-𝔽 P) = is-total-Total-Order-𝔽 P
+
+type-Total-Order-𝔽 :
+  {l1 l2 : Level} → Total-Order-𝔽 l1 l2 → UU l1
+type-Total-Order-𝔽 = type-Poset ∘ poset-Total-Order-𝔽
+```
diff --git a/src/order-theory/inhabited-finite-total-orders.lagda.md b/src/order-theory/inhabited-finite-total-orders.lagda.md
new file mode 100644
index 0000000000..0da80cd350
--- /dev/null
+++ b/src/order-theory/inhabited-finite-total-orders.lagda.md
@@ -0,0 +1,62 @@
+# Inhabited finite total orders
+
+```agda
+module order-theory.inhabited-finite-total-orders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import order-theory.finite-posets
+open import order-theory.finite-preorders
+open import order-theory.finite-total-orders
+open import order-theory.posets
+open import order-theory.total-orders
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## Definitions
+
+An **inhabited finite total order** is a
+[finite total order](order-theory.finite-total-orders.md) of which the
+underlying type is [inhabited](foundation.inhabited-types.md).
+
+```agda
+module _
+  {l1 l2 : Level} (P : Total-Order-𝔽 l1 l2)
+  where
+
+  is-inhabited-Total-Order-𝔽-Prop : Prop l1
+  is-inhabited-Total-Order-𝔽-Prop = is-inhabited-Prop (type-Total-Order-𝔽 P)
+
+  is-inhabited-Total-Order-𝔽 : UU (l1 ⊔ l2)
+  is-inhabited-Total-Order-𝔽 = is-finite-Poset (poset-Total-Order-𝔽 P)
+
+  is-prop-is-inhabited-Total-Order-𝔽 : is-prop is-inhabited-Total-Order-𝔽
+  is-prop-is-inhabited-Total-Order-𝔽 =
+    is-prop-is-finite-Poset (poset-Total-Order-𝔽 P)
+
+  is-finite-type-is-inhabited-Total-Order-𝔽 :
+    is-inhabited-Total-Order-𝔽 → is-finite (type-Total-Order-𝔽 P)
+  is-finite-type-is-inhabited-Total-Order-𝔽 =
+    is-finite-type-is-finite-Poset (poset-Total-Order-𝔽 P)
+
+is-inhabited-finite-total-order-Poset-Prop :
+  {l1 l2 : Level} (P : Poset l1 l2) → Prop (l1 ⊔ l2)
+is-inhabited-finite-total-order-Poset-Prop P =
+  prod-Prop
+    ( is-total-Poset-Prop P)
+    ( prod-Prop
+      ( is-finite-Poset-Prop P)
+      ( is-inhabited-Prop (type-Poset P)))
+```
diff --git a/src/order-theory/posets.lagda.md b/src/order-theory/posets.lagda.md
index 0c945aee5c..1a3c6eb992 100644
--- a/src/order-theory/posets.lagda.md
+++ b/src/order-theory/posets.lagda.md
@@ -27,8 +27,10 @@ open import order-theory.preorders
 
 ## Idea
 
-A **poset** is a set equipped with a reflexive, antisymmetric, transitive
-relation that takes values in propositions.
+A **poset** is a [set](foundation-core.sets.md)
+[equipped](foundation.structure.md) with a reflexive, antisymmetric, transitive
+[relation](foundation.binary-relations.md) that takes values in
+[propositions](foundation-core.propositions.md).
 
 ## Definition
 
diff --git a/src/order-theory/precategory-of-decidable-total-orders.lagda.md b/src/order-theory/precategory-of-decidable-total-orders.lagda.md
new file mode 100644
index 0000000000..7632fb7f60
--- /dev/null
+++ b/src/order-theory/precategory-of-decidable-total-orders.lagda.md
@@ -0,0 +1,60 @@
+# The precategory of decidable total orders
+
+```agda
+module order-theory.precategory-of-decidable-total-orders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.full-large-subprecategories
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.universe-levels
+
+open import order-theory.decidable-total-orders
+open import order-theory.precategory-of-posets
+```
+
+</details>
+
+## Idea
+
+The **(large) precategory of decidable total orders** consists of
+[decidable total orders](order-theory.decidable-total-orders.md) and
+[order preserving maps](order-theory.order-preserving-maps-posets.md) and is
+exhibited as a
+[full subprecategory](category-theory.full-large-subprecategories.md) of the
+[precategory of posets](order-theory.precategory-of-posets.md).
+
+## Definitions
+
+### The large precategory of decidable total orders
+
+```agda
+parametric-Decidable-Total-Order-Full-Large-Subprecategory :
+  (α β : Level → Level) →
+  Full-Large-Subprecategory
+    ( λ l → α l ⊔ β l)
+    ( parametric-Poset-Large-Precategory α β)
+parametric-Decidable-Total-Order-Full-Large-Subprecategory α β =
+  is-decidable-total-prop-Poset
+
+Decidable-Total-Order-Large-Precategory :
+  Large-Precategory lsuc (_⊔_)
+Decidable-Total-Order-Large-Precategory =
+  large-precategory-Full-Large-Subprecategory
+    ( Poset-Large-Precategory)
+    ( parametric-Decidable-Total-Order-Full-Large-Subprecategory
+      ( λ l → l)
+      ( λ l → l))
+```
+
+### The precategory or total orders of universe level `l`
+
+```agda
+Decidable-Total-Order-Precategory : (l : Level) → Precategory (lsuc l) l
+Decidable-Total-Order-Precategory =
+  precategory-Large-Precategory Decidable-Total-Order-Large-Precategory
+```
diff --git a/src/order-theory/precategory-of-finite-posets.lagda.md b/src/order-theory/precategory-of-finite-posets.lagda.md
new file mode 100644
index 0000000000..d992226f6e
--- /dev/null
+++ b/src/order-theory/precategory-of-finite-posets.lagda.md
@@ -0,0 +1,58 @@
+# The precategory of finite posets
+
+```agda
+module order-theory.precategory-of-finite-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.full-large-subprecategories
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.cartesian-product-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import order-theory.finite-posets
+open import order-theory.precategory-of-posets
+```
+
+</details>
+
+## Idea
+
+The **(large) precategory of finite posets** consists of
+[finite posets](order-theory.finite-posets.md) and
+[order preserving maps](order-theory.order-preserving-maps-posets.md) and is
+exhibited as a
+[full subprecategory](category-theory.full-large-subprecategories.md) of the
+[precategory of posets](order-theory.precategory-of-posets.md).
+
+## Definitions
+
+### The large precategory of finite posets
+
+```agda
+parametric-Poset-𝔽-Full-Large-Subprecategory :
+  (α β : Level → Level) →
+  Full-Large-Subprecategory
+    ( λ l → α l ⊔ β l)
+    ( parametric-Poset-Large-Precategory α β)
+parametric-Poset-𝔽-Full-Large-Subprecategory α β = is-finite-Poset-Prop
+
+Poset-𝔽-Large-Precategory :
+  Large-Precategory lsuc (_⊔_)
+Poset-𝔽-Large-Precategory =
+  large-precategory-Full-Large-Subprecategory
+    ( Poset-Large-Precategory)
+    ( parametric-Poset-𝔽-Full-Large-Subprecategory (λ l → l) (λ l → l))
+```
+
+### The precategory of finite posets of universe level `l`
+
+```agda
+Poset-𝔽-Precategory : (l : Level) → Precategory (lsuc l) l
+Poset-𝔽-Precategory = precategory-Large-Precategory Poset-𝔽-Large-Precategory
+```
diff --git a/src/order-theory/precategory-of-finite-total-orders.lagda.md b/src/order-theory/precategory-of-finite-total-orders.lagda.md
new file mode 100644
index 0000000000..9e98270f0f
--- /dev/null
+++ b/src/order-theory/precategory-of-finite-total-orders.lagda.md
@@ -0,0 +1,60 @@
+# The precategory of finite total orders
+
+```agda
+module order-theory.precategory-of-finite-total-orders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.full-large-subprecategories
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.cartesian-product-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import order-theory.finite-total-orders
+open import order-theory.precategory-of-posets
+open import order-theory.precategory-of-total-orders
+```
+
+</details>
+
+## Idea
+
+The **(large) precategory of finite total orders** consists of
+[finite total orders](order-theory.finite-total-orders.md) and
+[order preserving maps](order-theory.order-preserving-maps-posets.md) and is
+exhibited as a
+[full subprecategory](category-theory.full-large-subprecategories.md) of the
+[precategory of posets](order-theory.precategory-of-posets.md).
+
+## Definitions
+
+### The large precategory of finite total orders
+
+```agda
+parametric-Total-Order-𝔽-Full-Large-Subprecategory :
+  (α β : Level → Level) →
+  Full-Large-Subprecategory
+    ( λ l → α l ⊔ β l)
+    ( parametric-Poset-Large-Precategory α β)
+parametric-Total-Order-𝔽-Full-Large-Subprecategory α β =
+  is-finite-total-order-Poset-Prop
+
+Total-Order-𝔽-Large-Precategory : Large-Precategory lsuc (_⊔_)
+Total-Order-𝔽-Large-Precategory =
+  large-precategory-Full-Large-Subprecategory
+    ( Poset-Large-Precategory)
+    ( parametric-Total-Order-𝔽-Full-Large-Subprecategory (λ l → l) (λ l → l))
+```
+
+### The precategory of finite total orders of universe level `l`
+
+```agda
+Total-Order-𝔽-Precategory : (l : Level) → Precategory (lsuc l) l
+Total-Order-𝔽-Precategory =
+  precategory-Large-Precategory Total-Order-𝔽-Large-Precategory
+```
diff --git a/src/order-theory/precategory-of-inhabited-finite-total-orders.lagda.md b/src/order-theory/precategory-of-inhabited-finite-total-orders.lagda.md
new file mode 100644
index 0000000000..d71b8d8b7e
--- /dev/null
+++ b/src/order-theory/precategory-of-inhabited-finite-total-orders.lagda.md
@@ -0,0 +1,63 @@
+# The precategory of inhabited finite total orders
+
+```agda
+module order-theory.precategory-of-inhabited-finite-total-orders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.full-large-subprecategories
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.cartesian-product-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import order-theory.finite-total-orders
+open import order-theory.inhabited-finite-total-orders
+open import order-theory.precategory-of-posets
+open import order-theory.precategory-of-total-orders
+```
+
+</details>
+
+## Idea
+
+The **(large) precategory of inhabited finite total orders** consists of
+[inhabited finite total orders](order-theory.inhabited-finite-total-orders.md)
+and [order preserving maps](order-theory.order-preserving-maps-posets.md) and is
+exhibited as a
+[full subprecategory](category-theory.full-large-subprecategories.md) of the
+[precategory of posets](order-theory.precategory-of-posets.md).
+
+## Definitions
+
+### The large precategory of inhabited finite total orders
+
+```agda
+parametric-Inhabited-Total-Order-𝔽-Full-Large-Subprecategory :
+  (α β : Level → Level) →
+  Full-Large-Subprecategory
+    ( λ l → α l ⊔ β l)
+    ( parametric-Poset-Large-Precategory α β)
+parametric-Inhabited-Total-Order-𝔽-Full-Large-Subprecategory α β =
+  is-inhabited-finite-total-order-Poset-Prop
+
+Inhabited-Total-Order-𝔽-Large-Precategory : Large-Precategory lsuc (_⊔_)
+Inhabited-Total-Order-𝔽-Large-Precategory =
+  large-precategory-Full-Large-Subprecategory
+    ( Poset-Large-Precategory)
+    ( parametric-Inhabited-Total-Order-𝔽-Full-Large-Subprecategory
+      ( λ l → l)
+      ( λ l → l))
+```
+
+### The precategory of finite total orders of universe level `l`
+
+```agda
+Inhabited-Total-Order-𝔽-Precategory : (l : Level) → Precategory (lsuc l) l
+Inhabited-Total-Order-𝔽-Precategory =
+  precategory-Large-Precategory Inhabited-Total-Order-𝔽-Large-Precategory
+```
diff --git a/src/order-theory/precategory-of-posets.lagda.md b/src/order-theory/precategory-of-posets.lagda.md
new file mode 100644
index 0000000000..2c9fc94979
--- /dev/null
+++ b/src/order-theory/precategory-of-posets.lagda.md
@@ -0,0 +1,59 @@
+# The precategory of posets
+
+```agda
+module order-theory.precategory-of-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-posets
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+The **(large) precategory of posets** consists of
+[posets](order-theory.posets.md) and
+[order preserving maps](order-theory.order-preserving-maps-posets.md).
+
+## Definitions
+
+### The large precategory of posets
+
+```agda
+parametric-Poset-Large-Precategory :
+  (α β : Level → Level) →
+  Large-Precategory
+    ( λ l → lsuc (α l) ⊔ lsuc (β l))
+    ( λ l1 l2 → α l1 ⊔ β l1 ⊔ α l2 ⊔ β l2)
+parametric-Poset-Large-Precategory α β =
+  λ where
+    .obj-Large-Precategory l → Poset (α l) (β l)
+    .hom-set-Large-Precategory → hom-set-Poset
+    .comp-hom-Large-Precategory {X = X} {Y} {Z} → comp-hom-Poset X Y Z
+    .id-hom-Large-Precategory {X = X} → id-hom-Poset X
+    .associative-comp-hom-Large-Precategory {X = X} {Y} {Z} {W} →
+      associative-comp-hom-Poset X Y Z W
+    .left-unit-law-comp-hom-Large-Precategory {X = X} {Y} →
+      left-unit-law-comp-hom-Poset X Y
+    .right-unit-law-comp-hom-Large-Precategory {X = X} {Y} →
+      right-unit-law-comp-hom-Poset X Y
+
+Poset-Large-Precategory : Large-Precategory lsuc (_⊔_)
+Poset-Large-Precategory = parametric-Poset-Large-Precategory (λ l → l) (λ l → l)
+```
+
+### The precategory or posets of universe level `l`
+
+```agda
+Poset-Precategory : (l : Level) → Precategory (lsuc l) l
+Poset-Precategory = precategory-Large-Precategory Poset-Large-Precategory
+```
diff --git a/src/order-theory/precategory-of-total-orders.lagda.md b/src/order-theory/precategory-of-total-orders.lagda.md
new file mode 100644
index 0000000000..8a9fc8c68a
--- /dev/null
+++ b/src/order-theory/precategory-of-total-orders.lagda.md
@@ -0,0 +1,57 @@
+# The precategory of total orders
+
+```agda
+module order-theory.precategory-of-total-orders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.full-large-subprecategories
+open import category-theory.large-precategories
+open import category-theory.precategories
+
+open import foundation.universe-levels
+
+open import order-theory.precategory-of-posets
+open import order-theory.total-orders
+```
+
+</details>
+
+## Idea
+
+The **(large) precategory of total orders** consists of
+[total orders](order-theory.total-orders.md) and
+[order preserving maps](order-theory.order-preserving-maps-posets.md) and is
+exhibited as a
+[full subprecategory](category-theory.full-large-subprecategories.md) of the
+[precategory of posets](order-theory.precategory-of-posets.md).
+
+## Definitions
+
+### The large precategory of total orders
+
+```agda
+parametric-Total-Order-Full-Large-Subprecategory :
+  (α β : Level → Level) →
+  Full-Large-Subprecategory
+    ( λ l → α l ⊔ β l)
+    ( parametric-Poset-Large-Precategory α β)
+parametric-Total-Order-Full-Large-Subprecategory α β = is-total-Poset-Prop
+
+Total-Order-Large-Precategory :
+  Large-Precategory lsuc (_⊔_)
+Total-Order-Large-Precategory =
+  large-precategory-Full-Large-Subprecategory
+    ( Poset-Large-Precategory)
+    ( parametric-Total-Order-Full-Large-Subprecategory (λ l → l) (λ l → l))
+```
+
+### The precategory or total orders of universe level `l`
+
+```agda
+Total-Order-Precategory : (l : Level) → Precategory (lsuc l) l
+Total-Order-Precategory =
+  precategory-Large-Precategory Total-Order-Large-Precategory
+```
diff --git a/src/order-theory/preorders.lagda.md b/src/order-theory/preorders.lagda.md
index 311f0b4a3a..b1bd20bc0c 100644
--- a/src/order-theory/preorders.lagda.md
+++ b/src/order-theory/preorders.lagda.md
@@ -151,8 +151,7 @@ module _
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
-  ( is-prop-hom-C :
-    (x y : obj-Precategory C) → is-prop (hom-Precategory C x y))
+  ( is-prop-hom-C : (x y : obj-Precategory C) → is-prop (hom-Precategory C x y))
   where
 
   preorder-is-prop-hom-Precategory : Preorder l1 l2
diff --git a/src/univalent-combinatorics/equivalences-standard-finite-types.lagda.md b/src/univalent-combinatorics/equivalences-standard-finite-types.lagda.md
index 4b83b2b2bd..9190619d09 100644
--- a/src/univalent-combinatorics/equivalences-standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/equivalences-standard-finite-types.lagda.md
@@ -27,7 +27,8 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-We construct equivalences between (types built out of) standard finite types.
+We construct **equivalences** between (types built out of)
+[standard finite types](univalent-combinatorics.standard-finite-types.md).
 
 ### The standard finite types are closed under function types
 
@@ -38,8 +39,8 @@ function-Fin zero-ℕ l =
   ( inv-left-unit-law-coprod unit) ∘e
   ( equiv-is-contr (universal-property-empty' (Fin l)) is-contr-unit)
 function-Fin (succ-ℕ k) l =
-  ( ( prod-Fin (exp-ℕ l k) l) ∘e
-    ( equiv-prod (function-Fin k l) (equiv-universal-property-unit (Fin l)))) ∘e
+  ( prod-Fin (exp-ℕ l k) l) ∘e
+  ( equiv-prod (function-Fin k l) (equiv-universal-property-unit (Fin l))) ∘e
   ( equiv-universal-property-coprod (Fin l))
 
 Fin-exp-ℕ : (k l : ℕ) → Fin (exp-ℕ l k) ≃ (Fin k → Fin l)
diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md
index 4fa2bac999..c8f0de3f89 100644
--- a/src/univalent-combinatorics/finite-types.lagda.md
+++ b/src/univalent-combinatorics/finite-types.lagda.md
@@ -47,7 +47,9 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-A type is finite if it is merely equivalent to a standard finite type.
+A type is **finite** if it is
+[merely equivalent](foundation.mere-equivalences.md) to a
+[standard finite type](univalent-combinatorics.standard-finite-types.md).
 
 ## Definition
 
@@ -99,7 +101,7 @@ has-cardinality :
 has-cardinality k X = mere-equiv (Fin k) X
 ```
 
-### The type of all types of cardinality k of a given universe leve l
+### The type of all types of cardinality `k` of a given universe level
 
 ```agda
 UU-Fin : (l : Level) → ℕ → UU (lsuc l)
diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md
index 265f072024..e6d995b007 100644
--- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md
+++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md
@@ -31,9 +31,11 @@ open import univalent-combinatorics.finite-types
 
 An **inhabited finite type** is a
 [finite type](univalent-combinatorics.finite-types.md) that is
-[inhabited](foundation.inhabited-types.md), meaning it is a type that is merely
-equivalent to a standard finite type, and that comes equipped with a term of its
-propositional truncation.
+[inhabited](foundation.inhabited-types.md), meaning it is a type that is
+[merely equivalent](foundation.mere-equivalences.md) to a
+[standard finite type](univalent-combinatorics.standard-finite-types.md), and
+that comes equipped with a term of its
+[propositional truncation](foundation.propositional-truncations.md).
 
 ## Definitions
 
@@ -123,7 +125,7 @@ compute-Fam-Inhabited-𝔽 :
   {l1 l2 : Level} → (X : 𝔽 l1) →
   Fam-Inhabited-Types-𝔽 l2 X ≃
     Σ ( Fam-Inhabited-Types l2 (type-𝔽 X))
-      ( λ Y → ((x : (type-𝔽 X)) → is-finite (type-Inhabited-Type (Y x))))
+      ( λ Y → (x : type-𝔽 X) → is-finite (type-Inhabited-Type (Y x)))
 compute-Fam-Inhabited-𝔽 X =
   ( distributive-Π-Σ) ∘e
   ( equiv-Π
@@ -149,7 +151,7 @@ eq-equiv-Inhabited-𝔽 X Y e =
       ( e))
 ```
 
-### Every type in `UU-Fin (succ-ℕ n)` is a inhabited finite type
+### Every type in `UU-Fin (succ-ℕ n)` is an inhabited finite type
 
 ```agda
 is-finite-and-inhabited-type-UU-Fin-succ-ℕ :
diff --git a/src/univalent-combinatorics/sequences-finite-types.lagda.md b/src/univalent-combinatorics/sequences-finite-types.lagda.md
index 699d6af9f5..b9d113365b 100644
--- a/src/univalent-combinatorics/sequences-finite-types.lagda.md
+++ b/src/univalent-combinatorics/sequences-finite-types.lagda.md
@@ -20,7 +20,6 @@ open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.negated-equality
-open import foundation.negation
 open import foundation.pairs-of-distinct-elements
 open import foundation.repetitions-of-values
 open import foundation.repetitions-sequences
diff --git a/tables/precategories.md b/tables/precategories.md
index 06b715ed2e..de35225da8 100644
--- a/tables/precategories.md
+++ b/tables/precategories.md
@@ -1,15 +1,18 @@
-| Precategory           | File                                                                                                                      |
-| --------------------- | ------------------------------------------------------------------------------------------------------------------------- |
-| Abelian groups        | [`group-theory.precategory-of-abelian-groups`](group-theory.precategory-of-abelian-groups.md)                             |
-| Commutative monoids   | [`group-theory.precategory-of-commutative-monoids`](group-theory.precategory-of-commutative-monoids.md)                   |
-| Commutative rings     | [`commutative-algebra.precategory-of-commutative-rings`](commutative-algebra.precategory-of-commutative-rings.md)         |
-| Commutative semirings | [`commutative-algebra.precategory-of-commutative-semirings`](commutative-algebra.precategory-of-commutative-semirings.md) |
-| Concrete groups       | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md)                           |
-| Finite species        | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md)                                       |
-| `G`-sets              | [`group-theory.precategory-of-group-actions`](group-theory.precategory-of-group-actions.md)                               |
-| Groups                | [`group-theory.precategory-of-groups`](group-theory.precategory-of-groups.md)                                             |
-| Monoids               | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md)                                           |
-| Rings                 | [`ring-theory.precategory-of-rings`](ring-theory.precategory-of-rings.md)                                                 |
-| Semigroups            | [`group-theory.precategory-of-semigroups`](group-theory.precategory-of-semigroups.md)                                     |
-| Semirings             | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md)                                         |
-| Sets                  | [`foundation.category-of-sets`](foundation.category-of-sets.md)                                                           |
+| Precategory            | File                                                                                                                      |
+| ---------------------- | ------------------------------------------------------------------------------------------------------------------------- |
+| Abelian groups         | [`group-theory.precategory-of-abelian-groups`](group-theory.precategory-of-abelian-groups.md)                             |
+| Commutative monoids    | [`group-theory.precategory-of-commutative-monoids`](group-theory.precategory-of-commutative-monoids.md)                   |
+| Commutative rings      | [`commutative-algebra.precategory-of-commutative-rings`](commutative-algebra.precategory-of-commutative-rings.md)         |
+| Commutative semirings  | [`commutative-algebra.precategory-of-commutative-semirings`](commutative-algebra.precategory-of-commutative-semirings.md) |
+| Concrete groups        | [`group-theory.precategory-of-concrete-groups`](group-theory.precategory-of-concrete-groups.md)                           |
+| Decidable total orders | [`order-theory.precategory-of-decidable-total-orders`](order-theory.precategory-of-decidable-total-orders.md)             |
+| Finite species         | [`species.precategory-of-finite-species`](species.precategory-of-finite-species.md)                                       |
+| `G`-sets               | [`group-theory.precategory-of-group-actions`](group-theory.precategory-of-group-actions.md)                               |
+| Groups                 | [`group-theory.precategory-of-groups`](group-theory.precategory-of-groups.md)                                             |
+| Monoids                | [`group-theory.precategory-of-monoids`](group-theory.precategory-of-monoids.md)                                           |
+| Posets                 | [`order-theory.precategory-of-posets`](order-theory.precategory-of-posets.md)                                             |
+| Rings                  | [`ring-theory.precategory-of-rings`](ring-theory.precategory-of-rings.md)                                                 |
+| Semigroups             | [`group-theory.precategory-of-semigroups`](group-theory.precategory-of-semigroups.md)                                     |
+| Semirings              | [`ring-theory.precategory-of-semirings`](ring-theory.precategory-of-semirings.md)                                         |
+| Sets                   | [`foundation.category-of-sets`](foundation.category-of-sets.md)                                                           |
+| Total orders           | [`order-theory.precategory-of-total-orders`](order-theory.precategory-of-total-orders.md)                                 |