From 169ba36a37ac8992d7636bf3bd6fc3358667524e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:44:44 +0200 Subject: [PATCH] revert some merge conflicts --- .../precategory-of-decidable-total-orders.lagda.md | 2 +- src/order-theory/precategory-of-posets.lagda.md | 12 +++++++++++- .../precategory-of-total-orders.lagda.md | 2 +- 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/order-theory/precategory-of-decidable-total-orders.lagda.md b/src/order-theory/precategory-of-decidable-total-orders.lagda.md index 7632fb7f60..ee91924562 100644 --- a/src/order-theory/precategory-of-decidable-total-orders.lagda.md +++ b/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 diff --git a/src/order-theory/precategory-of-posets.lagda.md b/src/order-theory/precategory-of-posets.lagda.md index 29876db4bc..2d4708a629 100644 --- a/src/order-theory/precategory-of-posets.lagda.md +++ b/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 diff --git a/src/order-theory/precategory-of-total-orders.lagda.md b/src/order-theory/precategory-of-total-orders.lagda.md index 8a9fc8c68a..aeb5d9ffd2 100644 --- a/src/order-theory/precategory-of-total-orders.lagda.md +++ b/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