revert some merge conflicts

src/order-theory/precategory-of-decidable-total-orders.lagda.md

@@ -51,7 +51,7 @@ Decidable-Total-Order-Large-Precategory =
       ( λ l → l))
 ```
 
-### The precategory or total orders of universe level `l`
+### The precategory of total orders at a universe level
 
 ```agda
 Decidable-Total-Order-Precategory : (l : Level) → Precategory (lsuc l) l

src/order-theory/precategory-of-posets.lagda.md

@@ -28,6 +28,16 @@ consists of [posets](order-theory.posets.md) and
 
 ### The large precategory of posets
 
+**Remark.** In this formalization we see a clear limit to our approach using
+[large precategories](category-theory.large-precategories.md). Large
+precategories are only designed to encapsulate structures that are universe
+polymorphic in a single universe level variable. However, posets are polymorphic
+in two universe level variables, leading to a shortcoming in the below
+formalization. Namely, we cannot capture the structure of all posets and
+morphisms between them. For instance, we can only capture morphisms between two
+posets of the form `A : Poset (α l1) (β l1)` and `B : Poset (α l2) (β l2)`, and
+not arbitrary ones of the form `A : Poset l1 l2` and `B : Poset l3 l4`.
+
 ```agda
 parametric-Poset-Large-Precategory :
   (α β : Level → Level) →
@@ -55,7 +65,7 @@ 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`
+### The precategory of posets at a universe level
 
 ```agda
 Poset-Precategory : (l : Level) → Precategory (lsuc l) l

src/order-theory/precategory-of-total-orders.lagda.md

@@ -48,7 +48,7 @@ Total-Order-Large-Precategory =
     ( parametric-Total-Order-Full-Large-Subprecategory (λ l → l) (λ l → l))
 ```
 
-### The precategory or total orders of universe level `l`
+### The precategory of total orders at a universe level
 
 ```agda
 Total-Order-Precategory : (l : Level) → Precategory (lsuc l) l