From 97b0536d8c4be7556c64fc4efe028787b04a38ed Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 22:16:11 +0200 Subject: [PATCH 01/15] checkout `order-theory` --- src/order-theory.lagda.md | 4 + src/order-theory/chains-posets.lagda.md | 13 +++ src/order-theory/chains-preorders.lagda.md | 8 ++ src/order-theory/large-suplattices.lagda.md | 10 +- .../maximal-elements-posets.lagda.md | 46 ++++++++ ...ategory-of-decidable-total-orders.lagda.md | 2 +- .../precategory-of-posets.lagda.md | 12 +- .../precategory-of-total-orders.lagda.md | 2 +- src/order-theory/subtypes-leq-posets.lagda.md | 40 +++++++ .../upper-bounds-chains-posets.lagda.md | 48 ++++++++ src/order-theory/zorn.lagda.md | 103 ++++++++++++++++++ 11 files changed, 271 insertions(+), 17 deletions(-) create mode 100644 src/order-theory/maximal-elements-posets.lagda.md create mode 100644 src/order-theory/subtypes-leq-posets.lagda.md create mode 100644 src/order-theory/upper-bounds-chains-posets.lagda.md create mode 100644 src/order-theory/zorn.lagda.md diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index fdb7cae0eb..5e8a759c97 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -75,6 +75,7 @@ open import order-theory.lower-sets-large-posets public open import order-theory.lower-types-preorders public open import order-theory.maximal-chains-posets public open import order-theory.maximal-chains-preorders public +open import order-theory.maximal-elements-posets public open import order-theory.meet-semilattices public open import order-theory.meet-suplattices public open import order-theory.nuclei-large-locales public @@ -101,15 +102,18 @@ open import order-theory.similarity-of-order-preserving-maps-large-posets public open import order-theory.similarity-of-order-preserving-maps-large-preorders public open import order-theory.subposets public open import order-theory.subpreorders public +open import order-theory.subtypes-leq-posets public open import order-theory.suplattices public open import order-theory.top-elements-large-posets public 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.zorn public ``` diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md index 609bdfb03e..c3eaf21e1b 100644 --- a/src/order-theory/chains-posets.lagda.md +++ b/src/order-theory/chains-posets.lagda.md @@ -7,7 +7,11 @@ module order-theory.chains-posets where
Imports ```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 @@ -53,9 +57,18 @@ module _ sub-preorder-chain-Poset = sub-preorder-chain-Preorder (preorder-Poset X) C + is-chain-Subposet-chain-Poset : + is-chain-Subposet X sub-preorder-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 + type-Poset-type-chain-Poset : type-chain-Poset → type-Poset X + type-Poset-type-chain-Poset = + type-Preorder-type-chain-Preorder (preorder-Poset X) C + module _ {l1 l2 : Level} (X : Poset l1 l2) where diff --git a/src/order-theory/chains-preorders.lagda.md b/src/order-theory/chains-preorders.lagda.md index edcc516f32..c53a1bb8f1 100644 --- a/src/order-theory/chains-preorders.lagda.md +++ b/src/order-theory/chains-preorders.lagda.md @@ -58,9 +58,17 @@ module _ sub-preorder-chain-Preorder : type-Preorder X → Prop l3 sub-preorder-chain-Preorder = pr1 C + is-chain-Subpreorder-chain-Preorder : + is-chain-Subpreorder X sub-preorder-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-Preorder-type-chain-Preorder : type-chain-Preorder → type-Preorder X + type-Preorder-type-chain-Preorder = + inclusion-subtype sub-preorder-chain-Preorder + module _ {l1 l2 : Level} (X : Preorder l1 l2) where diff --git a/src/order-theory/large-suplattices.lagda.md b/src/order-theory/large-suplattices.lagda.md index 6f8bb90417..ac9782f0a4 100644 --- a/src/order-theory/large-suplattices.lagda.md +++ b/src/order-theory/large-suplattices.lagda.md @@ -4,22 +4,24 @@ module order-theory.large-suplattices where ``` -
Imports +Imports ```agda -open import foundation.binary-relations open import foundation.dependent-pair-types -open import foundation.identity-types open import foundation.large-binary-relations + +open import foundation.binary-relations + +open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.universe-levels open import order-theory.large-posets -open import order-theory.least-upper-bounds-large-posets open import order-theory.posets open import order-theory.suplattices +open import order-theory.least-upper-bounds-large-posets open import order-theory.upper-bounds-large-posets ``` diff --git a/src/order-theory/maximal-elements-posets.lagda.md b/src/order-theory/maximal-elements-posets.lagda.md new file mode 100644 index 0000000000..b807d310ab --- /dev/null +++ b/src/order-theory/maximal-elements-posets.lagda.md @@ -0,0 +1,46 @@ +# Maximal elements in posets + +```agda +module order-theory.maximal-elements-posets where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import foundation-core.identity-types +open import foundation-core.propositions + +open import order-theory.posets +``` + +
+ +## Idea + +TODO + +## Definition + +```agda +module _ + {l1 l2 : Level} (X : Poset l1 l2) + where + + is-maximal-element-Poset-Prop : type-Poset X → Prop (l1 ⊔ l2) + is-maximal-element-Poset-Prop x = + Π-Prop + ( type-Poset X) + ( λ y → + ( function-Prop (leq-Poset X x y) (y = x , is-set-type-Poset X y x))) + + is-maximal-element-Poset : type-Poset X → UU (l1 ⊔ l2) + is-maximal-element-Poset x = type-Prop (is-maximal-element-Poset-Prop x) + + is-prop-is-maximal-element-Poset : + (x : type-Poset X) → is-prop (is-maximal-element-Poset x) + is-prop-is-maximal-element-Poset x = + is-prop-type-Prop (is-maximal-element-Poset-Prop x) +``` 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 ee91924562..7632fb7f60 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 of total orders at a universe level +### The precategory or total orders of universe level `l` ```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 2d4708a629..29876db4bc 100644 --- a/src/order-theory/precategory-of-posets.lagda.md +++ b/src/order-theory/precategory-of-posets.lagda.md @@ -28,16 +28,6 @@ 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) → @@ -65,7 +55,7 @@ Poset-Large-Precategory : Large-Precategory lsuc (_⊔_) Poset-Large-Precategory = parametric-Poset-Large-Precategory (λ l → l) (λ l → l) ``` -### The precategory of posets at a universe level +### The precategory or posets of universe level `l` ```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 aeb5d9ffd2..8a9fc8c68a 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 of total orders at a universe level +### The precategory or total orders of universe level `l` ```agda Total-Order-Precategory : (l : Level) → Precategory (lsuc l) l diff --git a/src/order-theory/subtypes-leq-posets.lagda.md b/src/order-theory/subtypes-leq-posets.lagda.md new file mode 100644 index 0000000000..9a96cc9b6b --- /dev/null +++ b/src/order-theory/subtypes-leq-posets.lagda.md @@ -0,0 +1,40 @@ +# Subtypes leq Posets + +```agda +module order-theory.subtypes-leq-posets where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.posets +open import order-theory.preorders +``` + +
+ +## Idea + +TODO + +## Definition + +```agda +module _ + {l1 : Level} (l2 : Level) (A : UU l1) + where + + subtypes-leq-Preorder : Preorder (l1 ⊔ lsuc l2) (l1 ⊔ l2) + pr1 subtypes-leq-Preorder = subtype l2 A + pr1 (pr2 subtypes-leq-Preorder) = leq-prop-subtype + pr1 (pr2 (pr2 subtypes-leq-Preorder)) = refl-leq-subtype + pr2 (pr2 (pr2 subtypes-leq-Preorder)) = transitive-leq-subtype + + subtypes-leq-Poset : Poset (l1 ⊔ lsuc l2) (l1 ⊔ l2) + pr1 subtypes-leq-Poset = subtypes-leq-Preorder + pr2 subtypes-leq-Poset = antisymmetric-leq-subtype +``` 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..aba3dbbe68 --- /dev/null +++ b/src/order-theory/upper-bounds-chains-posets.lagda.md @@ -0,0 +1,48 @@ +# Upper bounds of chains in posets + +```agda +module order-theory.upper-bounds-chains-posets where +``` + +
Imports + +```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 +``` + +
+ +## Idea + +An **upper bound** of a chain `C` in a poset `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-chain-upper-bound-Prop : type-Poset X → Prop (l1 ⊔ l2 ⊔ l3) + is-chain-upper-bound-Prop = + is-upper-bound-family-of-elements-Poset-Prop X + ( type-Poset-type-chain-Poset X C) + + is-chain-upper-bound : type-Poset X → UU (l1 ⊔ l2 ⊔ l3) + is-chain-upper-bound = type-Prop ∘ is-chain-upper-bound-Prop + + has-chain-upper-bound-Prop : Prop (l1 ⊔ l2 ⊔ l3) + has-chain-upper-bound-Prop = ∃ (type-Poset X) is-chain-upper-bound-Prop + + has-chain-upper-bound : UU (l1 ⊔ l2 ⊔ l3) + has-chain-upper-bound = type-Prop has-chain-upper-bound-Prop +``` diff --git a/src/order-theory/zorn.lagda.md b/src/order-theory/zorn.lagda.md new file mode 100644 index 0000000000..ecc4021460 --- /dev/null +++ b/src/order-theory/zorn.lagda.md @@ -0,0 +1,103 @@ +# Zorn's lemma + +```agda +module order-theory.zorn where +``` + +
Imports + +```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.maximal-elements-posets +open import order-theory.posets +open import order-theory.upper-bounds-chains-posets +``` + +
+ +## Idea + +TODO + +## Definition + +```agda +module _ + (l1 l2 l3 : Level) + where + + Zorn-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) + Zorn-Prop = + Π-Prop + ( Poset l1 l2) + ( λ X → + ( function-Prop + ( (C : chain-Poset l3 X) → has-chain-upper-bound X C) + ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X)))) + + Zorn : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) + Zorn = type-Prop Zorn-Prop + + Zorn-non-empty-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) + Zorn-non-empty-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-chain-upper-bound X C) + ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X))))) + + Zorn-non-empty : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) + Zorn-non-empty = type-Prop Zorn-non-empty-Prop + + Zorn-Zorn-non-empty : Zorn-non-empty → Zorn + Zorn-Zorn-non-empty zorn X H = + zorn X + ( apply-universal-property-trunc-Prop + ( H + ( pair + ( λ _ → raise-empty-Prop l3) + ( λ (_ , f) → raise-ex-falso l3 f))) + ( is-inhabited-Prop (type-Poset X)) + ( λ (x , _) → unit-trunc-Prop x)) + ( λ C _ → H C) + + module _ + (lem : LEM (l1 ⊔ l3)) + where + + Zorn-non-empty-Zorn : Zorn → Zorn-non-empty + Zorn-non-empty-Zorn zorn X is-inhabited-X H = zorn X chain-upper-bound + where + chain-upper-bound : (C : chain-Poset l3 X) → has-chain-upper-bound 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-chain-upper-bound-Prop X C) + ( λ x → + ( intro-exists x + ( λ (y , y-in-C) → + ( ex-falso (is-empty-C (intro-exists y y-in-C)))))) + + iff-Zorn-non-empty-Zorn : type-iff-Prop Zorn-non-empty-Prop Zorn-Prop + pr1 (iff-Zorn-non-empty-Zorn) = Zorn-Zorn-non-empty + pr2 (iff-Zorn-non-empty-Zorn) = Zorn-non-empty-Zorn +``` From 84573311424027afecebab022e0358207ce05541 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 22:49:18 +0200 Subject: [PATCH 02/15] rename module `zorn` -> `zorns-lemma` --- src/order-theory.lagda.md | 2 +- src/order-theory/{zorn.lagda.md => zorns-lemma.lagda.md} | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename src/order-theory/{zorn.lagda.md => zorns-lemma.lagda.md} (98%) diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index 5e8a759c97..c1e09ba160 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -115,5 +115,5 @@ 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.zorn public +open import order-theory.zorns-lemma public ``` diff --git a/src/order-theory/zorn.lagda.md b/src/order-theory/zorns-lemma.lagda.md similarity index 98% rename from src/order-theory/zorn.lagda.md rename to src/order-theory/zorns-lemma.lagda.md index ecc4021460..a32191d09c 100644 --- a/src/order-theory/zorn.lagda.md +++ b/src/order-theory/zorns-lemma.lagda.md @@ -1,7 +1,7 @@ # Zorn's lemma ```agda -module order-theory.zorn where +module order-theory.zorns-lemma where ```
Imports From e4e21d691d5ef4bedaf37d8455bf9a22bab5984b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 22:50:33 +0200 Subject: [PATCH 03/15] prose zorn's lemma --- src/order-theory/zorns-lemma.lagda.md | 123 +++++++++++++++++--------- 1 file changed, 79 insertions(+), 44 deletions(-) diff --git a/src/order-theory/zorns-lemma.lagda.md b/src/order-theory/zorns-lemma.lagda.md index a32191d09c..aec0ca88aa 100644 --- a/src/order-theory/zorns-lemma.lagda.md +++ b/src/order-theory/zorns-lemma.lagda.md @@ -29,75 +29,110 @@ open import order-theory.upper-bounds-chains-posets ## Idea -TODO +{{#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 +[maximal element](order-theory.maximal-elements.md). -## Definition +## Statement + +### Zorn's lemma ```agda module _ (l1 l2 l3 : Level) where - Zorn-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) - Zorn-Prop = + zorns-lemma-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) + zorns-lemma-Prop = Π-Prop ( Poset l1 l2) ( λ X → - ( function-Prop + function-Prop ( (C : chain-Poset l3 X) → has-chain-upper-bound X C) - ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X)))) + ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X))) - Zorn : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) - Zorn = type-Prop Zorn-Prop + 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 - Zorn-non-empty-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) - Zorn-non-empty-Prop = + inhabited-zorns-lemma-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) + inhabited-zorns-lemma-Prop = Π-Prop ( Poset l1 l2) ( λ X → - ( function-Prop + function-Prop ( is-inhabited (type-Poset X)) ( function-Prop ( (C : chain-Poset l3 X) → - is-inhabited (type-chain-Poset X C) → - has-chain-upper-bound X C) - ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X))))) + is-inhabited (type-chain-Poset X C) → has-chain-upper-bound X C) + ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X)))) + + inhabited-zorns-lemma : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) + inhabited-zorns-lemma = type-Prop inhabited-zorns-lemma-Prop +``` + +## Properties - Zorn-non-empty : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) - Zorn-non-empty = type-Prop Zorn-non-empty-Prop +### Zorn's lemma for inhabited chains implies Zorn's lemma - Zorn-Zorn-non-empty : Zorn-non-empty → Zorn - Zorn-Zorn-non-empty zorn X H = +```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 - ( pair - ( λ _ → raise-empty-Prop l3) - ( λ (_ , f) → raise-ex-falso l3 f))) + ( H ((λ _ → raise-empty-Prop l3) , (λ p → raise-ex-falso l3 (pr2 p)))) ( is-inhabited-Prop (type-Poset X)) - ( λ (x , _) → unit-trunc-Prop x)) + ( λ p → unit-trunc-Prop (pr1 p))) ( λ C _ → H C) +``` - module _ - (lem : LEM (l1 ⊔ l3)) - where +### Assuming the law of excluded middle, Zorn's lemma implies Zorn's lemma for inhabited chains - Zorn-non-empty-Zorn : Zorn → Zorn-non-empty - Zorn-non-empty-Zorn zorn X is-inhabited-X H = zorn X chain-upper-bound - where - chain-upper-bound : (C : chain-Poset l3 X) → has-chain-upper-bound 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-chain-upper-bound-Prop X C) - ( λ x → - ( intro-exists x - ( λ (y , y-in-C) → - ( ex-falso (is-empty-C (intro-exists y y-in-C)))))) - - iff-Zorn-non-empty-Zorn : type-iff-Prop Zorn-non-empty-Prop Zorn-Prop - pr1 (iff-Zorn-non-empty-Zorn) = Zorn-Zorn-non-empty - pr2 (iff-Zorn-non-empty-Zorn) = Zorn-non-empty-Zorn +```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-chain-upper-bound 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-chain-upper-bound-Prop 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 From bd054b16a4eb7f479bc39c2e0cb0bb147488c7ec Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:09:36 +0200 Subject: [PATCH 04/15] edits --- src/order-theory/chains-posets.lagda.md | 11 +++++++-- src/order-theory/chains-preorders.lagda.md | 11 +++++++-- .../maximal-elements-posets.lagda.md | 23 +++++++++++++------ 3 files changed, 34 insertions(+), 11 deletions(-) diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md index c3eaf21e1b..e10ed18a47 100644 --- a/src/order-theory/chains-posets.lagda.md +++ b/src/order-theory/chains-posets.lagda.md @@ -22,8 +22,10 @@ open import order-theory.posets ## 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 @@ -88,3 +90,8 @@ module _ is-prop-inclusion-chain-Poset = is-prop-inclusion-chain-Preorder (preorder-Poset X) ``` + +## 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 c53a1bb8f1..412692b8bc 100644 --- a/src/order-theory/chains-preorders.lagda.md +++ b/src/order-theory/chains-preorders.lagda.md @@ -21,8 +21,10 @@ 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 @@ -92,3 +94,8 @@ module _ is-prop-inclusion-chain-Preorder C D = is-prop-type-Prop (inclusion-chain-Preorder-Prop 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/maximal-elements-posets.lagda.md b/src/order-theory/maximal-elements-posets.lagda.md index b807d310ab..6c1d02fcc8 100644 --- a/src/order-theory/maximal-elements-posets.lagda.md +++ b/src/order-theory/maximal-elements-posets.lagda.md @@ -20,7 +20,11 @@ open import order-theory.posets ## Idea -TODO +A +{{#concept "maximal" Disambiguation="element in a poset" WD="maximal and minimal elements" WDID=Q1475294 Agda=is-maximal-element-Poset}} +element in a [poset](order-theory.posets.md) is an element `y` such that every +other element `x` that is greater than it `y ≤ x` is +[equal](foundation-core.identity-types.md) to it `y = x`. ## Definition @@ -29,18 +33,23 @@ module _ {l1 l2 : Level} (X : Poset l1 l2) where - is-maximal-element-Poset-Prop : type-Poset X → Prop (l1 ⊔ l2) - is-maximal-element-Poset-Prop x = + is-maximal-element-prop-Poset : type-Poset X → Prop (l1 ⊔ l2) + is-maximal-element-prop-Poset x = Π-Prop ( type-Poset X) - ( λ y → - ( function-Prop (leq-Poset X x y) (y = x , is-set-type-Poset X y x))) + ( λ y → function-Prop (leq-Poset X x y) (y = x , is-set-type-Poset X y x)) is-maximal-element-Poset : type-Poset X → UU (l1 ⊔ l2) - is-maximal-element-Poset x = type-Prop (is-maximal-element-Poset-Prop x) + is-maximal-element-Poset x = type-Prop (is-maximal-element-prop-Poset x) is-prop-is-maximal-element-Poset : (x : type-Poset X) → is-prop (is-maximal-element-Poset x) is-prop-is-maximal-element-Poset x = - is-prop-type-Prop (is-maximal-element-Poset-Prop x) + is-prop-type-Prop (is-maximal-element-prop-Poset x) ``` + +## 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 From 238aaef31544dbf1650b600a0abb94ea4e36d243 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:18:37 +0200 Subject: [PATCH 05/15] delete `subtypes-leq-posets` --- src/order-theory.lagda.md | 1 - src/order-theory/subtypes-leq-posets.lagda.md | 40 ------------------- 2 files changed, 41 deletions(-) delete mode 100644 src/order-theory/subtypes-leq-posets.lagda.md diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index c1e09ba160..cf2daf8ccb 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -102,7 +102,6 @@ open import order-theory.similarity-of-order-preserving-maps-large-posets public open import order-theory.similarity-of-order-preserving-maps-large-preorders public open import order-theory.subposets public open import order-theory.subpreorders public -open import order-theory.subtypes-leq-posets public open import order-theory.suplattices public open import order-theory.top-elements-large-posets public open import order-theory.top-elements-posets public diff --git a/src/order-theory/subtypes-leq-posets.lagda.md b/src/order-theory/subtypes-leq-posets.lagda.md deleted file mode 100644 index 9a96cc9b6b..0000000000 --- a/src/order-theory/subtypes-leq-posets.lagda.md +++ /dev/null @@ -1,40 +0,0 @@ -# Subtypes leq Posets - -```agda -module order-theory.subtypes-leq-posets where -``` - -
Imports - -```agda -open import foundation.dependent-pair-types -open import foundation.subtypes -open import foundation.universe-levels - -open import order-theory.posets -open import order-theory.preorders -``` - -
- -## Idea - -TODO - -## Definition - -```agda -module _ - {l1 : Level} (l2 : Level) (A : UU l1) - where - - subtypes-leq-Preorder : Preorder (l1 ⊔ lsuc l2) (l1 ⊔ l2) - pr1 subtypes-leq-Preorder = subtype l2 A - pr1 (pr2 subtypes-leq-Preorder) = leq-prop-subtype - pr1 (pr2 (pr2 subtypes-leq-Preorder)) = refl-leq-subtype - pr2 (pr2 (pr2 subtypes-leq-Preorder)) = transitive-leq-subtype - - subtypes-leq-Poset : Poset (l1 ⊔ lsuc l2) (l1 ⊔ l2) - pr1 subtypes-leq-Poset = subtypes-leq-Preorder - pr2 subtypes-leq-Poset = antisymmetric-leq-subtype -``` From 8eec9b48d6e493ea016aa5487e2e14a94cb3d376 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:40:03 +0200 Subject: [PATCH 06/15] fixes --- src/order-theory/chains-posets.lagda.md | 60 ++++++++---------- src/order-theory/chains-preorders.lagda.md | 63 ++++++++----------- src/order-theory/finite-preorders.lagda.md | 2 +- .../maximal-chains-preorders.lagda.md | 2 +- src/order-theory/subposets.lagda.md | 17 ++--- .../upper-bounds-chains-posets.lagda.md | 2 +- src/order-theory/zorns-lemma.lagda.md | 4 +- 7 files changed, 68 insertions(+), 82 deletions(-) diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md index e10ed18a47..3647919bcb 100644 --- a/src/order-theory/chains-posets.lagda.md +++ b/src/order-theory/chains-posets.lagda.md @@ -16,6 +16,7 @@ open import foundation.universe-levels open import order-theory.chains-preorders open import order-theory.posets +open import order-theory.subposets ```
@@ -31,21 +32,17 @@ A {{#concept "chain" Disambiguation="in a poset" Agda=chain-Poset}} in a ```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 : - {l3 : Level} (S : type-Poset X → Prop l3) → UU (l1 ⊔ l2 ⊔ l3) - is-chain-Subposet = is-chain-Subpreorder (preorder-Poset X) + is-chain-Subposet : UU (l1 ⊔ l2 ⊔ l3) + is-chain-Subposet = 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) + is-prop-is-chain-Subposet : is-prop is-chain-Subposet + is-prop-is-chain-Subposet = is-prop-is-chain-Subpreorder (preorder-Poset X) S chain-Poset : {l1 l2 : Level} (l : Level) (X : Poset l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l) @@ -55,40 +52,37 @@ 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 sub-preorder-chain-Poset - is-chain-Subposet-chain-Poset = - is-chain-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 - type-Poset-type-chain-Poset : type-chain-Poset → type-Poset X - type-Poset-type-chain-Poset = - type-Preorder-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 diff --git a/src/order-theory/chains-preorders.lagda.md b/src/order-theory/chains-preorders.lagda.md index 412692b8bc..4aa05e3682 100644 --- a/src/order-theory/chains-preorders.lagda.md +++ b/src/order-theory/chains-preorders.lagda.md @@ -30,23 +30,18 @@ restricted to `S` is [linear](order-theory.total-preorders.md). ```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 : - {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) + is-prop-is-chain-Subpreorder : is-prop is-chain-Subpreorder + is-prop-is-chain-Subpreorder = is-prop-type-Prop is-chain-prop-Subpreorder chain-Preorder : {l1 l2 : Level} (l : Level) (X : Preorder l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l) @@ -57,42 +52,38 @@ 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 sub-preorder-chain-Preorder - is-chain-Subpreorder-chain-Preorder = pr2 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 - type-Preorder-type-chain-Preorder : type-chain-Preorder → type-Preorder X - type-Preorder-type-chain-Preorder = - inclusion-subtype sub-preorder-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-prop-chain-Preorder : Prop (l1 ⊔ l3 ⊔ l4) + inclusion-prop-chain-Preorder = inclusion-Subpreorder-Prop X - ( sub-preorder-chain-Preorder X C) - ( sub-preorder-chain-Preorder X D) + ( 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 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/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..b891dcc5e8 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) @@ -80,8 +84,7 @@ 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) @@ -96,14 +99,12 @@ 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 diff --git a/src/order-theory/upper-bounds-chains-posets.lagda.md b/src/order-theory/upper-bounds-chains-posets.lagda.md index aba3dbbe68..0ec5c25cc4 100644 --- a/src/order-theory/upper-bounds-chains-posets.lagda.md +++ b/src/order-theory/upper-bounds-chains-posets.lagda.md @@ -35,7 +35,7 @@ module _ is-chain-upper-bound-Prop : type-Poset X → Prop (l1 ⊔ l2 ⊔ l3) is-chain-upper-bound-Prop = is-upper-bound-family-of-elements-Poset-Prop X - ( type-Poset-type-chain-Poset X C) + ( inclusion-type-chain-Poset X C) is-chain-upper-bound : type-Poset X → UU (l1 ⊔ l2 ⊔ l3) is-chain-upper-bound = type-Prop ∘ is-chain-upper-bound-Prop diff --git a/src/order-theory/zorns-lemma.lagda.md b/src/order-theory/zorns-lemma.lagda.md index aec0ca88aa..8988165a53 100644 --- a/src/order-theory/zorns-lemma.lagda.md +++ b/src/order-theory/zorns-lemma.lagda.md @@ -51,7 +51,7 @@ module _ ( λ X → function-Prop ( (C : chain-Poset l3 X) → has-chain-upper-bound X C) - ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X))) + ( ∃ (type-Poset X) (is-maximal-element-prop-Poset X))) zorns-lemma : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) zorns-lemma = type-Prop zorns-lemma-Prop @@ -74,7 +74,7 @@ module _ ( function-Prop ( (C : chain-Poset l3 X) → is-inhabited (type-chain-Poset X C) → has-chain-upper-bound X C) - ( ∃ (type-Poset X) (is-maximal-element-Poset-Prop X)))) + ( ∃ (type-Poset X) (is-maximal-element-prop-Poset X)))) inhabited-zorns-lemma : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) inhabited-zorns-lemma = type-Prop inhabited-zorns-lemma-Prop From 169ba36a37ac8992d7636bf3bd6fc3358667524e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:44:44 +0200 Subject: [PATCH 07/15] 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 From abe6bcf55a65643633677401179d4b1040349532 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:45:50 +0200 Subject: [PATCH 08/15] revert some merge conflicts --- src/order-theory/large-suplattices.lagda.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/order-theory/large-suplattices.lagda.md b/src/order-theory/large-suplattices.lagda.md index ac9782f0a4..6f8bb90417 100644 --- a/src/order-theory/large-suplattices.lagda.md +++ b/src/order-theory/large-suplattices.lagda.md @@ -4,24 +4,22 @@ module order-theory.large-suplattices where ``` -Imports +
Imports ```agda -open import foundation.dependent-pair-types -open import foundation.large-binary-relations - open import foundation.binary-relations - +open import foundation.dependent-pair-types open import foundation.identity-types +open import foundation.large-binary-relations open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.universe-levels open import order-theory.large-posets +open import order-theory.least-upper-bounds-large-posets open import order-theory.posets open import order-theory.suplattices -open import order-theory.least-upper-bounds-large-posets open import order-theory.upper-bounds-large-posets ``` From 3658f69b3709d3f4cc4d30b0681d1ac39b7640df Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:50:45 +0200 Subject: [PATCH 09/15] naming upper bounds chains posets --- .../upper-bounds-chains-posets.lagda.md | 24 +++++++++++-------- src/order-theory/zorns-lemma.lagda.md | 9 +++---- 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/order-theory/upper-bounds-chains-posets.lagda.md b/src/order-theory/upper-bounds-chains-posets.lagda.md index 0ec5c25cc4..4326fd679f 100644 --- a/src/order-theory/upper-bounds-chains-posets.lagda.md +++ b/src/order-theory/upper-bounds-chains-posets.lagda.md @@ -22,8 +22,11 @@ open import order-theory.upper-bounds-posets ## Idea -An **upper bound** of a chain `C` in a poset `P` is an element `x` such that for -every element `y` in `C`, `y ≤ x` holds. +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 @@ -32,17 +35,18 @@ module _ {l1 l2 l3 : Level} (X : Poset l1 l2) (C : chain-Poset l3 X) where - is-chain-upper-bound-Prop : type-Poset X → Prop (l1 ⊔ l2 ⊔ l3) - is-chain-upper-bound-Prop = + 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-chain-upper-bound : type-Poset X → UU (l1 ⊔ l2 ⊔ l3) - is-chain-upper-bound = type-Prop ∘ is-chain-upper-bound-Prop + 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-chain-upper-bound-Prop : Prop (l1 ⊔ l2 ⊔ l3) - has-chain-upper-bound-Prop = ∃ (type-Poset X) is-chain-upper-bound-Prop + 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-chain-upper-bound : UU (l1 ⊔ l2 ⊔ l3) - has-chain-upper-bound = type-Prop has-chain-upper-bound-Prop + 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 index 8988165a53..9e39eff443 100644 --- a/src/order-theory/zorns-lemma.lagda.md +++ b/src/order-theory/zorns-lemma.lagda.md @@ -50,7 +50,7 @@ module _ ( Poset l1 l2) ( λ X → function-Prop - ( (C : chain-Poset l3 X) → has-chain-upper-bound X C) + ( (C : chain-Poset l3 X) → has-upper-bound-chain-Poset X C) ( ∃ (type-Poset X) (is-maximal-element-prop-Poset X))) zorns-lemma : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) @@ -73,7 +73,8 @@ module _ ( is-inhabited (type-Poset X)) ( function-Prop ( (C : chain-Poset l3 X) → - is-inhabited (type-chain-Poset X C) → has-chain-upper-bound X C) + is-inhabited (type-chain-Poset X C) → + has-upper-bound-chain-Poset X C) ( ∃ (type-Poset X) (is-maximal-element-prop-Poset X)))) inhabited-zorns-lemma : UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) @@ -112,13 +113,13 @@ module _ 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-chain-upper-bound X C + 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-chain-upper-bound-Prop X C) + ( has-upper-bound-chain-prop-Poset X C) ( λ x → intro-exists x (λ w → ex-falso (is-empty-C (unit-trunc-Prop w)))) From 4b8cc0482d57f2156c1010cb9f6d20c6458c7ab0 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 19 Oct 2024 23:52:34 +0200 Subject: [PATCH 10/15] more naming --- src/order-theory/chains-preorders.lagda.md | 2 +- src/order-theory/subposets.lagda.md | 18 +++++++++--------- src/order-theory/subpreorders.lagda.md | 10 +++++----- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/order-theory/chains-preorders.lagda.md b/src/order-theory/chains-preorders.lagda.md index 4aa05e3682..684985b98b 100644 --- a/src/order-theory/chains-preorders.lagda.md +++ b/src/order-theory/chains-preorders.lagda.md @@ -73,7 +73,7 @@ module _ inclusion-prop-chain-Preorder : Prop (l1 ⊔ l3 ⊔ l4) inclusion-prop-chain-Preorder = - inclusion-Subpreorder-Prop X + inclusion-prop-Subpreorder X ( subpreorder-chain-Preorder X C) ( subpreorder-chain-Preorder X D) diff --git a/src/order-theory/subposets.lagda.md b/src/order-theory/subposets.lagda.md index b891dcc5e8..d7cd52162e 100644 --- a/src/order-theory/subposets.lagda.md +++ b/src/order-theory/subposets.lagda.md @@ -76,7 +76,7 @@ module _ pr2 poset-Subposet = antisymmetric-leq-Subposet ``` -### Inclusion of sub-posets +### Inclusion of subposets ```agda module _ @@ -87,9 +87,9 @@ module _ {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 @@ -111,9 +111,9 @@ module _ 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 ``` From 0d89ecad3ea520a1464db9c7d104ee08bc56bc30 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 20 Oct 2024 00:08:46 +0200 Subject: [PATCH 11/15] remove duplicate maximal elements posets --- src/order-theory.lagda.md | 1 - .../finitely-graded-posets.lagda.md | 2 +- .../maximal-elements-posets.lagda.md | 55 ------------------- .../top-elements-large-posets.lagda.md | 7 ++- src/order-theory/top-elements-posets.lagda.md | 26 ++++++--- .../top-elements-preorders.lagda.md | 20 +++++-- src/order-theory/zorns-lemma.lagda.md | 6 +- 7 files changed, 39 insertions(+), 78 deletions(-) delete mode 100644 src/order-theory/maximal-elements-posets.lagda.md diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index cf2daf8ccb..1de24c0872 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -75,7 +75,6 @@ open import order-theory.lower-sets-large-posets public open import order-theory.lower-types-preorders public open import order-theory.maximal-chains-posets public open import order-theory.maximal-chains-preorders public -open import order-theory.maximal-elements-posets public open import order-theory.meet-semilattices public open import order-theory.meet-suplattices public open import order-theory.nuclei-large-locales public 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-elements-posets.lagda.md b/src/order-theory/maximal-elements-posets.lagda.md deleted file mode 100644 index 6c1d02fcc8..0000000000 --- a/src/order-theory/maximal-elements-posets.lagda.md +++ /dev/null @@ -1,55 +0,0 @@ -# Maximal elements in posets - -```agda -module order-theory.maximal-elements-posets where -``` - -
Imports - -```agda -open import foundation.dependent-pair-types -open import foundation.universe-levels - -open import foundation-core.identity-types -open import foundation-core.propositions - -open import order-theory.posets -``` - -
- -## Idea - -A -{{#concept "maximal" Disambiguation="element in a poset" WD="maximal and minimal elements" WDID=Q1475294 Agda=is-maximal-element-Poset}} -element in a [poset](order-theory.posets.md) is an element `y` such that every -other element `x` that is greater than it `y ≤ x` is -[equal](foundation-core.identity-types.md) to it `y = x`. - -## Definition - -```agda -module _ - {l1 l2 : Level} (X : Poset l1 l2) - where - - is-maximal-element-prop-Poset : type-Poset X → Prop (l1 ⊔ l2) - is-maximal-element-prop-Poset x = - Π-Prop - ( type-Poset X) - ( λ y → function-Prop (leq-Poset X x y) (y = x , is-set-type-Poset X y x)) - - is-maximal-element-Poset : type-Poset X → UU (l1 ⊔ l2) - is-maximal-element-Poset x = type-Prop (is-maximal-element-prop-Poset x) - - is-prop-is-maximal-element-Poset : - (x : type-Poset X) → is-prop (is-maximal-element-Poset x) - is-prop-is-maximal-element-Poset x = - is-prop-type-Prop (is-maximal-element-prop-Poset x) -``` - -## 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-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/zorns-lemma.lagda.md b/src/order-theory/zorns-lemma.lagda.md index 9e39eff443..c6cdb1d3dc 100644 --- a/src/order-theory/zorns-lemma.lagda.md +++ b/src/order-theory/zorns-lemma.lagda.md @@ -20,8 +20,8 @@ open import foundation-core.coproduct-types open import foundation-core.propositions open import order-theory.chains-posets -open import order-theory.maximal-elements-posets open import order-theory.posets +open import order-theory.top-elements-posets open import order-theory.upper-bounds-chains-posets ``` @@ -51,7 +51,7 @@ module _ ( λ X → function-Prop ( (C : chain-Poset l3 X) → has-upper-bound-chain-Poset X C) - ( ∃ (type-Poset X) (is-maximal-element-prop-Poset X))) + ( ∃ (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 @@ -75,7 +75,7 @@ module _ ( (C : chain-Poset l3 X) → is-inhabited (type-chain-Poset X C) → has-upper-bound-chain-Poset X C) - ( ∃ (type-Poset X) (is-maximal-element-prop-Poset X)))) + ( ∃ (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 From ef2600685633d0c39a8561ce946a42ed51c44146 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 20 Oct 2024 00:09:43 +0200 Subject: [PATCH 12/15] Update src/order-theory/chains-posets.lagda.md Co-authored-by: Egbert Rijke --- src/order-theory/chains-posets.lagda.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md index 3647919bcb..d40656dc10 100644 --- a/src/order-theory/chains-posets.lagda.md +++ b/src/order-theory/chains-posets.lagda.md @@ -43,7 +43,11 @@ module _ is-prop-is-chain-Subposet : is-prop is-chain-Subposet is-prop-is-chain-Subposet = is-prop-is-chain-Subpreorder (preorder-Poset X) S +``` + +### 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) From b7d5e58e68f865f8d629d9e22043c5f015b5da08 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 20 Oct 2024 00:12:56 +0200 Subject: [PATCH 13/15] Update src/order-theory/chains-posets.lagda.md Co-authored-by: Egbert Rijke --- src/order-theory/chains-posets.lagda.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md index d40656dc10..79e72f7cd7 100644 --- a/src/order-theory/chains-posets.lagda.md +++ b/src/order-theory/chains-posets.lagda.md @@ -30,6 +30,8 @@ A {{#concept "chain" Disambiguation="in a poset" Agda=chain-Poset}} in a ## Definition +### The predicate on subsets of posets to be a chain + ```agda module _ {l1 l2 l3 : Level} (X : Poset l1 l2) (S : Subposet l3 X) From a4212d86093c9c07ae9363103c78b91ab8d60358 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 20 Oct 2024 00:18:11 +0200 Subject: [PATCH 14/15] review chains --- src/order-theory/chains-posets.lagda.md | 4 ++-- src/order-theory/chains-preorders.lagda.md | 10 ++++++++-- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/order-theory/chains-posets.lagda.md b/src/order-theory/chains-posets.lagda.md index 79e72f7cd7..99d9811a4b 100644 --- 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 index 684985b98b..f620d50ff1 100644 --- 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 From 0bdbccaa9d03bda57ea3536a50335af9bad77f66 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 20 Oct 2024 00:42:51 +0200 Subject: [PATCH 15/15] fix link --- src/order-theory/zorns-lemma.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/order-theory/zorns-lemma.lagda.md b/src/order-theory/zorns-lemma.lagda.md index c6cdb1d3dc..a2e403817a 100644 --- a/src/order-theory/zorns-lemma.lagda.md +++ b/src/order-theory/zorns-lemma.lagda.md @@ -33,7 +33,7 @@ open import order-theory.upper-bounds-chains-posets 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 -[maximal element](order-theory.maximal-elements.md). +[top element](order-theory.top-elements-posets.md). ## Statement