From 9860ec74162b86ba7d8bd3ba79529961bfbc481c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Oct 2025 20:53:43 +0100 Subject: [PATCH 01/13] define material types --- docs/PROJECTS.md | 3 + references.bib | 9 + .../equivalence-relations.lagda.md | 4 +- src/foundation/binary-relations.lagda.md | 30 +-- src/foundation/decidable-relations.lagda.md | 6 +- .../exponents-set-quotients.lagda.md | 2 +- src/group-theory/grothendieck-groups.lagda.md | 2 +- ...y-of-elements-pseudometric-spaces.lagda.md | 4 +- src/order-theory.lagda.md | 1 + .../accessible-elements-relations.lagda.md | 2 +- ...ections-closed-intervals-lattices.lagda.md | 2 +- ...ons-closed-intervals-total-orders.lagda.md | 2 +- src/order-theory/ordinals.lagda.md | 8 +- .../poset-closed-intervals-posets.lagda.md | 2 +- src/order-theory/preorders.lagda.md | 4 +- src/order-theory/strict-preorders.lagda.md | 4 +- .../strictly-preordered-sets.lagda.md | 4 +- ...l-founded-propositional-relations.lagda.md | 163 ++++++++++++ .../well-founded-relations.lagda.md | 4 + src/set-theory.lagda.md | 3 + .../elementhood-structures.lagda.md | 217 +++++++++++++++ src/set-theory/material-types.lagda.md | 189 +++++++++++++ .../well-founded-material-types.lagda.md | 251 ++++++++++++++++++ 23 files changed, 878 insertions(+), 38 deletions(-) create mode 100644 src/order-theory/well-founded-propositional-relations.lagda.md create mode 100644 src/set-theory/elementhood-structures.lagda.md create mode 100644 src/set-theory/material-types.lagda.md create mode 100644 src/set-theory/well-founded-material-types.lagda.md diff --git a/docs/PROJECTS.md b/docs/PROJECTS.md index 58f6c901359..e0a12e68097 100644 --- a/docs/PROJECTS.md +++ b/docs/PROJECTS.md @@ -4,6 +4,9 @@ Here is a list of projects that use the agda-unimath library: - - +- +- +- If your project uses the agda-unimath library, let us know, so we can add your project to the list. diff --git a/references.bib b/references.bib index 52836201613..953eda4cd45 100644 --- a/references.bib +++ b/references.bib @@ -520,6 +520,15 @@ @article{GK12 issn = {1469-8064}, } +@misc{GS24, + title = {Univalent Material Set Theory}, + author = {Håkon Robbestad Gylterud and Elisabeth Stenholm}, + year = 2024, + eprint = {2312.13024}, + archiveprefix = {arXiv}, + primaryclass = {math.LO}, +} + @book{Johnstone02, title = {Sketches of an Elephant a Topos Theory Compendium}, author = {Johnstone, Peter T}, diff --git a/src/foundation-core/equivalence-relations.lagda.md b/src/foundation-core/equivalence-relations.lagda.md index 28396e95f5a..c226e0b21e7 100644 --- a/src/foundation-core/equivalence-relations.lagda.md +++ b/src/foundation-core/equivalence-relations.lagda.md @@ -51,14 +51,14 @@ prop-equivalence-relation = pr1 sim-equivalence-relation : {l1 l2 : Level} {A : UU l1} → equivalence-relation l2 A → A → A → UU l2 -sim-equivalence-relation R = type-Relation-Prop (prop-equivalence-relation R) +sim-equivalence-relation R = rel-Relation-Prop (prop-equivalence-relation R) abstract is-prop-sim-equivalence-relation : {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A) (x y : A) → is-prop (sim-equivalence-relation R x y) is-prop-sim-equivalence-relation R = - is-prop-type-Relation-Prop (prop-equivalence-relation R) + is-prop-rel-Relation-Prop (prop-equivalence-relation R) is-prop-is-equivalence-relation : {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) → diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md index 36815698f5c..2926407d013 100644 --- a/src/foundation/binary-relations.lagda.md +++ b/src/foundation/binary-relations.lagda.md @@ -56,19 +56,19 @@ Relation-Prop : (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1) Relation-Prop l A = A → A → Prop l -type-Relation-Prop : +rel-Relation-Prop : {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → Relation l2 A -type-Relation-Prop R x y = pr1 (R x y) +rel-Relation-Prop R x y = pr1 (R x y) -is-prop-type-Relation-Prop : +is-prop-rel-Relation-Prop : {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) → - (x y : A) → is-prop (type-Relation-Prop R x y) -is-prop-type-Relation-Prop R x y = pr2 (R x y) + (x y : A) → is-prop (rel-Relation-Prop R x y) +is-prop-rel-Relation-Prop R x y = pr2 (R x y) total-space-Relation-Prop : {l : Level} {l1 : Level} {A : UU l1} → Relation-Prop l A → UU (l ⊔ l1) total-space-Relation-Prop {A = A} R = - Σ (A × A) λ (a , a') → type-Relation-Prop R a a' + Σ (A × A) λ (a , a') → rel-Relation-Prop R a a' ``` ### The predicate of being a reflexive relation @@ -96,11 +96,11 @@ module _ where is-reflexive-Relation-Prop : UU (l1 ⊔ l2) - is-reflexive-Relation-Prop = is-reflexive (type-Relation-Prop R) + is-reflexive-Relation-Prop = is-reflexive (rel-Relation-Prop R) is-prop-is-reflexive-Relation-Prop : is-prop is-reflexive-Relation-Prop is-prop-is-reflexive-Relation-Prop = - is-prop-Π (λ x → is-prop-type-Relation-Prop R x x) + is-prop-Π (λ x → is-prop-rel-Relation-Prop R x x) is-reflexive-prop-Relation-Prop : Prop (l1 ⊔ l2) is-reflexive-prop-Relation-Prop = @@ -132,12 +132,12 @@ module _ where is-symmetric-Relation-Prop : UU (l1 ⊔ l2) - is-symmetric-Relation-Prop = is-symmetric (type-Relation-Prop R) + is-symmetric-Relation-Prop = is-symmetric (rel-Relation-Prop R) is-prop-is-symmetric-Relation-Prop : is-prop is-symmetric-Relation-Prop is-prop-is-symmetric-Relation-Prop = is-prop-iterated-Π 3 - ( λ x y r → is-prop-type-Relation-Prop R y x) + ( λ x y r → is-prop-rel-Relation-Prop R y x) is-symmetric-prop-Relation-Prop : Prop (l1 ⊔ l2) is-symmetric-prop-Relation-Prop = @@ -172,14 +172,14 @@ module _ where is-transitive-Relation-Prop : UU (l1 ⊔ l2) - is-transitive-Relation-Prop = is-transitive (type-Relation-Prop R) + is-transitive-Relation-Prop = is-transitive (rel-Relation-Prop R) is-prop-is-transitive-Relation-Prop : is-prop is-transitive-Relation-Prop is-prop-is-transitive-Relation-Prop = is-prop-iterated-Π 3 ( λ x y z → is-prop-function-type - ( is-prop-function-type (is-prop-type-Relation-Prop R x z))) + ( is-prop-function-type (is-prop-rel-Relation-Prop R x z))) ``` ### The predicate of being an irreflexive relation @@ -200,7 +200,7 @@ module _ where is-irreflexive-Relation-Prop : UU (l1 ⊔ l2) - is-irreflexive-Relation-Prop = is-irreflexive (type-Relation-Prop R) + is-irreflexive-Relation-Prop = is-irreflexive (rel-Relation-Prop R) ``` ### The predicate of being an asymmetric relation @@ -242,7 +242,7 @@ module _ where is-antisymmetric-Relation-Prop : UU (l1 ⊔ l2) - is-antisymmetric-Relation-Prop = is-antisymmetric (type-Relation-Prop R) + is-antisymmetric-Relation-Prop = is-antisymmetric (rel-Relation-Prop R) ``` ### The predicate of being an entire relation @@ -271,7 +271,7 @@ module _ where is-entire-Relation-Prop : UU (l1 ⊔ l2) - is-entire-Relation-Prop = is-entire-Relation (type-Relation-Prop R) + is-entire-Relation-Prop = is-entire-Relation (rel-Relation-Prop R) ``` ## Properties diff --git a/src/foundation/decidable-relations.lagda.md b/src/foundation/decidable-relations.lagda.md index 770d4b5f81a..9526fe0d401 100644 --- a/src/foundation/decidable-relations.lagda.md +++ b/src/foundation/decidable-relations.lagda.md @@ -33,7 +33,7 @@ that each `R x y` is a decidable proposition. is-decidable-Relation-Prop : {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → UU (l1 ⊔ l2) is-decidable-Relation-Prop {A = A} R = - (x y : A) → is-decidable ( type-Relation-Prop R x y) + (x y : A) → is-decidable ( rel-Relation-Prop R x y) Decidable-Relation : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) Decidable-Relation l2 X = X → X → Decidable-Prop l2 @@ -62,8 +62,8 @@ map-inv-equiv-relation-is-decidable-Decidable-Relation : Σ ( Relation-Prop l2 X) (λ R → is-decidable-Relation-Prop R) → Decidable-Relation l2 X map-inv-equiv-relation-is-decidable-Decidable-Relation (R , d) x y = - ( ( type-Relation-Prop R x y) , - ( is-prop-type-Relation-Prop R x y) , + ( ( rel-Relation-Prop R x y) , + ( is-prop-rel-Relation-Prop R x y) , ( d x y)) equiv-relation-is-decidable-Decidable-Relation : diff --git a/src/foundation/exponents-set-quotients.lagda.md b/src/foundation/exponents-set-quotients.lagda.md index bfc9888f3c2..a1591975622 100644 --- a/src/foundation/exponents-set-quotients.lagda.md +++ b/src/foundation/exponents-set-quotients.lagda.md @@ -66,7 +66,7 @@ module _ Π-Prop X (λ x → prop-equivalence-relation R (f x) (g x)) sim-function-type : (f g : X → A) → UU (l1 ⊔ l3) - sim-function-type = type-Relation-Prop rel-function-type + sim-function-type = rel-Relation-Prop rel-function-type refl-sim-function-type : is-reflexive sim-function-type refl-sim-function-type f x = refl-equivalence-relation R (f x) diff --git a/src/group-theory/grothendieck-groups.lagda.md b/src/group-theory/grothendieck-groups.lagda.md index 32f535427d8..973c5d05460 100644 --- a/src/group-theory/grothendieck-groups.lagda.md +++ b/src/group-theory/grothendieck-groups.lagda.md @@ -84,7 +84,7 @@ module _ grothendieck-relation-Commutative-Monoid : Relation l (type-product-Commutative-Monoid M M) grothendieck-relation-Commutative-Monoid = - type-Relation-Prop grothendieck-relation-prop-Commutative-Monoid + rel-Relation-Prop grothendieck-relation-prop-Commutative-Monoid refl-grothendieck-relation-Commutative-Monoid : is-reflexive-Relation-Prop grothendieck-relation-prop-Commutative-Monoid diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index f9caa041d21..218e9ae9d16 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -61,13 +61,13 @@ module _ sim-Pseudometric-Space : Relation l2 (type-Pseudometric-Space A) sim-Pseudometric-Space = - type-Relation-Prop sim-prop-Pseudometric-Space + rel-Relation-Prop sim-prop-Pseudometric-Space is-prop-sim-Pseudometric-Space : (x y : type-Pseudometric-Space A) → is-prop (sim-Pseudometric-Space x y) is-prop-sim-Pseudometric-Space = - is-prop-type-Relation-Prop sim-prop-Pseudometric-Space + is-prop-rel-Relation-Prop sim-prop-Pseudometric-Space ``` ## Properties diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index 538d9ef2590..645d6a00f3c 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -168,6 +168,7 @@ 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-propositional-relations public open import order-theory.well-founded-relations public open import order-theory.zorns-lemma public ``` diff --git a/src/order-theory/accessible-elements-relations.lagda.md b/src/order-theory/accessible-elements-relations.lagda.md index a6b6863dcaa..b15c5e6ccf5 100644 --- a/src/order-theory/accessible-elements-relations.lagda.md +++ b/src/order-theory/accessible-elements-relations.lagda.md @@ -142,7 +142,7 @@ module _ is-prop-is-accessible-element-Relation x ``` -### If `x` is an `<`-accessible element, then `<` is antisymmetric at `x` +### If `x` is an `<`-accessible element, then `<` is asymmetric at `x` ```agda module _ diff --git a/src/order-theory/intersections-closed-intervals-lattices.lagda.md b/src/order-theory/intersections-closed-intervals-lattices.lagda.md index cd2c982e45a..29248dfabca 100644 --- a/src/order-theory/intersections-closed-intervals-lattices.lagda.md +++ b/src/order-theory/intersections-closed-intervals-lattices.lagda.md @@ -51,7 +51,7 @@ module _ intersect-closed-interval-Lattice : Relation l2 (closed-interval-Lattice L) intersect-closed-interval-Lattice = - type-Relation-Prop intersect-prop-closed-interval-Lattice + rel-Relation-Prop intersect-prop-closed-interval-Lattice ``` ## Properties diff --git a/src/order-theory/intersections-closed-intervals-total-orders.lagda.md b/src/order-theory/intersections-closed-intervals-total-orders.lagda.md index 260d60218ed..198057b1271 100644 --- a/src/order-theory/intersections-closed-intervals-total-orders.lagda.md +++ b/src/order-theory/intersections-closed-intervals-total-orders.lagda.md @@ -51,7 +51,7 @@ module _ intersect-closed-interval-Total-Order : Relation l2 (closed-interval-Total-Order T) intersect-closed-interval-Total-Order = - type-Relation-Prop intersect-prop-closed-interval-Total-Order + rel-Relation-Prop intersect-prop-closed-interval-Total-Order ``` ## Properties diff --git a/src/order-theory/ordinals.lagda.md b/src/order-theory/ordinals.lagda.md index e805ff678ba..a5079d23b90 100644 --- a/src/order-theory/ordinals.lagda.md +++ b/src/order-theory/ordinals.lagda.md @@ -50,7 +50,7 @@ extensionality-principle-Ordinal : {l1 l2 : Level} {X : UU l1} → Relation-Prop l2 X → UU (l1 ⊔ l2) extensionality-principle-Ordinal {X = X} R = (x y : X) → - ((u : X) → type-Relation-Prop R u x ↔ type-Relation-Prop R u y) → x ＝ y + ((u : X) → rel-Relation-Prop R u x ↔ rel-Relation-Prop R u y) → x ＝ y ``` ### The predicate of being an ordinal @@ -62,7 +62,7 @@ module _ is-ordinal : UU (l1 ⊔ l2) is-ordinal = - ( is-transitive-well-founded-relation-Relation (type-Relation-Prop R)) × + ( is-transitive-well-founded-relation-Relation (rel-Relation-Prop R)) × ( extensionality-principle-Ordinal R) ``` @@ -83,7 +83,7 @@ module _ le-prop-Ordinal = pr1 (pr2 O) le-Ordinal : Relation l2 type-Ordinal - le-Ordinal = type-Relation-Prop le-prop-Ordinal + le-Ordinal = rel-Relation-Prop le-prop-Ordinal is-ordinal-Ordinal : is-ordinal le-prop-Ordinal is-ordinal-Ordinal = pr2 (pr2 O) @@ -138,7 +138,7 @@ The associated reflexive relation on an ordinal. is-prop-leq-Ordinal {y = y} = is-prop-Π ( λ u → - is-prop-function-type (is-prop-type-Relation-Prop le-prop-Ordinal u y)) + is-prop-function-type (is-prop-rel-Relation-Prop le-prop-Ordinal u y)) leq-prop-Ordinal : Relation-Prop (l1 ⊔ l2) type-Ordinal leq-prop-Ordinal x y = (leq-Ordinal x y , is-prop-leq-Ordinal) diff --git a/src/order-theory/poset-closed-intervals-posets.lagda.md b/src/order-theory/poset-closed-intervals-posets.lagda.md index e9eb0d5e6cf..528127255c9 100644 --- a/src/order-theory/poset-closed-intervals-posets.lagda.md +++ b/src/order-theory/poset-closed-intervals-posets.lagda.md @@ -41,7 +41,7 @@ module _ leq-prop-Poset P c a ∧ leq-prop-Poset P b d leq-closed-interval-Poset : Relation l2 (closed-interval-Poset P) - leq-closed-interval-Poset = type-Relation-Prop leq-prop-closed-interval-Poset + leq-closed-interval-Poset = rel-Relation-Prop leq-prop-closed-interval-Poset ``` ## Properties diff --git a/src/order-theory/preorders.lagda.md b/src/order-theory/preorders.lagda.md index 1601ec8858f..1dd65cde20c 100644 --- a/src/order-theory/preorders.lagda.md +++ b/src/order-theory/preorders.lagda.md @@ -63,7 +63,7 @@ module _ leq-Preorder x y = type-Prop (leq-prop-Preorder x y) is-prop-leq-Preorder : (x y : type-Preorder) → is-prop (leq-Preorder x y) - is-prop-leq-Preorder = is-prop-type-Relation-Prop leq-prop-Preorder + is-prop-leq-Preorder = is-prop-rel-Relation-Prop leq-prop-Preorder concatenate-eq-leq-Preorder' : {x y z : type-Preorder} → x ＝ y → leq-Preorder x z → leq-Preorder y z @@ -97,7 +97,7 @@ module _ le-Preorder x y = type-Prop (le-prop-Preorder x y) is-prop-le-Preorder : (x y : type-Preorder) → is-prop (le-Preorder x y) - is-prop-le-Preorder = is-prop-type-Relation-Prop le-prop-Preorder + is-prop-le-Preorder = is-prop-rel-Relation-Prop le-prop-Preorder refl-leq-Preorder : is-reflexive leq-Preorder refl-leq-Preorder = pr1 (pr2 (pr2 X)) diff --git a/src/order-theory/strict-preorders.lagda.md b/src/order-theory/strict-preorders.lagda.md index 6f1a4b4392e..b9bb6c9d469 100644 --- a/src/order-theory/strict-preorders.lagda.md +++ b/src/order-theory/strict-preorders.lagda.md @@ -61,13 +61,13 @@ module _ le-Strict-Preorder : Relation l2 type-Strict-Preorder le-Strict-Preorder = - type-Relation-Prop le-prop-Strict-Preorder + rel-Relation-Prop le-prop-Strict-Preorder is-prop-le-Strict-Preorder : (x y : type-Strict-Preorder) → is-prop (le-Strict-Preorder x y) is-prop-le-Strict-Preorder = - is-prop-type-Relation-Prop le-prop-Strict-Preorder + is-prop-rel-Relation-Prop le-prop-Strict-Preorder is-irreflexive-le-Strict-Preorder : is-irreflexive le-Strict-Preorder diff --git a/src/order-theory/strictly-preordered-sets.lagda.md b/src/order-theory/strictly-preordered-sets.lagda.md index a5a458b6d8f..9f7d58c9dd1 100644 --- a/src/order-theory/strictly-preordered-sets.lagda.md +++ b/src/order-theory/strictly-preordered-sets.lagda.md @@ -81,13 +81,13 @@ module _ le-Strictly-Preordered-Set : Relation l2 type-Strictly-Preordered-Set le-Strictly-Preordered-Set = - type-Relation-Prop le-prop-Strictly-Preordered-Set + rel-Relation-Prop le-prop-Strictly-Preordered-Set is-prop-le-Strictly-Preordered-Set : (x y : type-Strictly-Preordered-Set) → is-prop (le-Strictly-Preordered-Set x y) is-prop-le-Strictly-Preordered-Set = - is-prop-type-Relation-Prop le-prop-Strictly-Preordered-Set + is-prop-rel-Relation-Prop le-prop-Strictly-Preordered-Set is-irreflexive-le-Strictly-Preordered-Set : is-irreflexive le-Strictly-Preordered-Set diff --git a/src/order-theory/well-founded-propositional-relations.lagda.md b/src/order-theory/well-founded-propositional-relations.lagda.md new file mode 100644 index 00000000000..7081e72372d --- /dev/null +++ b/src/order-theory/well-founded-propositional-relations.lagda.md @@ -0,0 +1,163 @@ +# Well-founded propositional relations + +```agda +module order-theory.well-founded-propositional-relations where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.universal-quantification +open import foundation.universe-levels + +open import order-theory.accessible-elements-relations +open import order-theory.preorders +open import order-theory.well-founded-relations +``` + +
+ +## Idea + +Given a type `X` equipped with a +[binary propositional relation](foundation.binary-relations.md) +`_<_ : X → X → Prop` we say that the relation `_<_` is +{{#concept "well-founded" Disambiguation="binary propositional relation" WDID=Q338021 WD="well-founded relation" Agda=is-well-founded-Relation-Prop Agda=Well-Founded-Relation-Prop}} +if all elements of `X` are +[accessible](order-theory.accessible-elements-relations.md) with respect to +`_<_`. + +Well-founded propositional relations satisfy an induction principle: In order to +construct an element of `P x` for all `x : X` it suffices to construct an +element of `P y` for all elements `y < x`. More precisely, the +{{#concept "well-founded induction principle" WDID=Q14402036 WD="well-founded induction" Agda=ind-Well-Founded-Relation-Prop-Prop}} +is a function + +```text + (x : X) → ((u : X) → (u < x) → P u) → P x. +``` + +## Definitions + +### The predicate of being a well-founded propositional relation + +```agda +module _ + {l1 l2 : Level} {X : UU l1} (_<_ : Relation-Prop l2 X) + where + + is-well-founded-prop-Relation-Prop : Prop (l1 ⊔ l2) + is-well-founded-prop-Relation-Prop = + is-well-founded-prop-Relation (rel-Relation-Prop _<_) + + is-well-founded-Relation-Prop : UU (l1 ⊔ l2) + is-well-founded-Relation-Prop = type-Prop is-well-founded-prop-Relation-Prop + + is-prop-is-well-founded-Relation-Prop : is-prop is-well-founded-Relation-Prop + is-prop-is-well-founded-Relation-Prop = + is-prop-type-Prop is-well-founded-prop-Relation-Prop +``` + +### Well-founded propositional relations + +```agda +Well-Founded-Relation-Prop : + {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +Well-Founded-Relation-Prop l X = + Σ (Relation-Prop l X) is-well-founded-Relation-Prop + +module _ + {l1 l2 : Level} {X : UU l1} (R : Well-Founded-Relation-Prop l2 X) + where + + rel-prop-Well-Founded-Relation-Prop : Relation-Prop l2 X + rel-prop-Well-Founded-Relation-Prop = pr1 R + + rel-Well-Founded-Relation-Prop : Relation l2 X + rel-Well-Founded-Relation-Prop = + rel-Relation-Prop rel-prop-Well-Founded-Relation-Prop + + is-well-founded-Well-Founded-Relation-Prop : + is-well-founded-Relation-Prop rel-prop-Well-Founded-Relation-Prop + is-well-founded-Well-Founded-Relation-Prop = pr2 R +``` + +### Well-founded induction + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} + ((R , w) : Well-Founded-Relation-Prop l2 X) + (let _<_ = rel-Relation-Prop R) + (P : X → UU l3) + where + + ind-Well-Founded-Relation-Prop : + ({x : X} → ({y : X} → y < x → P y) → P x) → (x : X) → P x + ind-Well-Founded-Relation-Prop IH x = + ind-accessible-element-Relation _<_ P (λ _ → IH) (w x) +``` + +## Properties + +### A well-founded propositional relation is asymmetric, and thus irreflexive + +```agda +module _ + {l1 l2 : Level} {X : UU l1} ((R , w) : Well-Founded-Relation-Prop l2 X) + (let _<_ = rel-Relation-Prop R) + where + + is-asymmetric-le-Well-Founded-Relation-Prop : is-asymmetric _<_ + is-asymmetric-le-Well-Founded-Relation-Prop x y = + is-asymmetric-is-accessible-element-Relation _<_ (w x) + + is-irreflexive-le-Well-Founded-Relation-Prop : is-irreflexive _<_ + is-irreflexive-le-Well-Founded-Relation-Prop = + is-irreflexive-is-asymmetric _<_ is-asymmetric-le-Well-Founded-Relation-Prop +``` + +### The associated reflexive propositional relation of a well-founded propositional relation + +Given a well-founded relation $<$ on $X$ there is an associated reflexive +relation given by + +$$ + (x ≤ y) := ∀ (u : X), (u < x) ⇒ (u < y). +$$ + +```agda +module _ + {l1 l2 : Level} {X : UU l1} + ((_<_ , w) : Well-Founded-Relation-Prop l2 X) + where + + leq-prop-Well-Founded-Relation-Prop : Relation-Prop (l1 ⊔ l2) X + leq-prop-Well-Founded-Relation-Prop x y = ∀' X (λ u → u < x ⇒ u < y) + + leq-Well-Founded-Relation-Prop : Relation (l1 ⊔ l2) X + leq-Well-Founded-Relation-Prop = + rel-Relation-Prop leq-prop-Well-Founded-Relation-Prop + + refl-leq-Well-Founded-Relation-Prop : + is-reflexive leq-Well-Founded-Relation-Prop + refl-leq-Well-Founded-Relation-Prop x u = id + + leq-eq-Well-Founded-Relation-Prop : + {x y : X} → x ＝ y → leq-Well-Founded-Relation-Prop x y + leq-eq-Well-Founded-Relation-Prop {x} refl = + refl-leq-Well-Founded-Relation-Prop x + + transitive-leq-Well-Founded-Relation-Prop : + is-transitive leq-Well-Founded-Relation-Prop + transitive-leq-Well-Founded-Relation-Prop x y z f g t H = f t (g t H) +``` + +## See also + +- [Well-founded relations](order-theory.well-founded-relations.md). diff --git a/src/order-theory/well-founded-relations.lagda.md b/src/order-theory/well-founded-relations.lagda.md index 451de38ce55..8e6bc9df80e 100644 --- a/src/order-theory/well-founded-relations.lagda.md +++ b/src/order-theory/well-founded-relations.lagda.md @@ -55,6 +55,10 @@ module _ is-well-founded-Relation : UU (l1 ⊔ l2) is-well-founded-Relation = (x : X) → is-accessible-element-Relation _∈_ x + + is-prop-is-well-founded-Relation : is-prop is-well-founded-Relation + is-prop-is-well-founded-Relation = + is-prop-type-Prop is-well-founded-prop-Relation ``` ### Well-founded relations diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md index 6ce59643c86..4335c1c9989 100644 --- a/src/set-theory.lagda.md +++ b/src/set-theory.lagda.md @@ -55,15 +55,18 @@ open import set-theory.cantors-diagonal-argument public open import set-theory.cardinalities public open import set-theory.countable-sets public open import set-theory.cumulative-hierarchy public +open import set-theory.elementhood-structures public open import set-theory.finite-elements-increasing-binary-sequences public open import set-theory.inclusion-natural-numbers-increasing-binary-sequences public open import set-theory.increasing-binary-sequences public open import set-theory.inequality-increasing-binary-sequences public open import set-theory.infinite-sets public +open import set-theory.material-types public open import set-theory.positive-elements-increasing-binary-sequences public open import set-theory.russells-paradox public open import set-theory.strict-lower-bounds-increasing-binary-sequences public open import set-theory.uncountable-sets public +open import set-theory.well-founded-material-types public ``` ## See also diff --git a/src/set-theory/elementhood-structures.lagda.md b/src/set-theory/elementhood-structures.lagda.md new file mode 100644 index 00000000000..5565e3c9b36 --- /dev/null +++ b/src/set-theory/elementhood-structures.lagda.md @@ -0,0 +1,217 @@ +# Elementhood structures + +```agda +module set-theory.elementhood-structures where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.separated-types-subuniverses +open import foundation.subtypes +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.torsorial-type-families + +open import order-theory.accessible-elements-relations +open import order-theory.preorders + +open import orthogonal-factorization-systems.reflective-global-subuniverses +``` + +
+ +## Idea + +Given a type `A` and a [binary relation](foundation.binary-relations.md) +`_∈_ : A → A → Type` dubbed an _elementhood relation_, we say that the +elementhood relation is +{{#concept "extensional" Disambiguation="elementhood" Agda=is-extensional-elementhood-Relation}} +if the canonical map + +```text + (x = y) → (Π (u : A), (u ∈ x) ≃ (u ∈ y)) +``` + +is an [equivalence](foundation-core.equivalences.md). + +An extensional elementhood relation on `A` endows the type `A` with the +[structure](foundation.structure.md) of +{{#concept "elementhood" Disambiguation="on a type" Agda=Elementhood-Structure}}. + +## Definitions + +### The canonical comparison map + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (_∈_ : Relation l2 A) + where + + equiv-elementhood-eq-Relation : + (x y : A) → (x ＝ y) → (u : A) → (u ∈ x) ≃ (u ∈ y) + equiv-elementhood-eq-Relation x .x refl u = id-equiv +``` + +### The extensionality predicate on elementhood relations + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (_∈_ : Relation l2 A) + where + + is-extensional-elementhood-Relation : UU (l1 ⊔ l2) + is-extensional-elementhood-Relation = + (x y : A) → is-equiv (equiv-elementhood-eq-Relation _∈_ x y) + + abstract + is-prop-is-extensional-elementhood-Relation : + is-prop is-extensional-elementhood-Relation + is-prop-is-extensional-elementhood-Relation = + is-prop-Π + ( λ x → + is-prop-Π + ( λ y → + is-property-is-equiv (equiv-elementhood-eq-Relation _∈_ x y))) + + is-extensional-elementhood-prop-Relation : Prop (l1 ⊔ l2) + is-extensional-elementhood-prop-Relation = + ( is-extensional-elementhood-Relation , + is-prop-is-extensional-elementhood-Relation) +``` + +### The type of elementhood structures on a type + +```agda +Elementhood-Structure : + {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) +Elementhood-Structure l2 A = + type-subtype (is-extensional-elementhood-prop-Relation {l2 = l2} {A}) + +module _ + {l1 l2 : Level} {A : UU l1} (R@(_∈_ , _) : Elementhood-Structure l2 A) + where + + elementhood-Elementhood-Structure : Relation l2 A + elementhood-Elementhood-Structure = pr1 R + + is-extensional-Elementhood-Structure : + is-extensional-elementhood-Relation elementhood-Elementhood-Structure + is-extensional-Elementhood-Structure = pr2 R + + equiv-eq-Elementhood-Structure : + (x y : A) → (x ＝ y) → (u : A) → (u ∈ x) ≃ (u ∈ y) + equiv-eq-Elementhood-Structure = + equiv-elementhood-eq-Relation _∈_ + + extensionality-Elementhood-Structure : + (x y : A) → (x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y)) + extensionality-Elementhood-Structure x y = + ( equiv-eq-Elementhood-Structure x y , + is-extensional-Elementhood-Structure x y) + + inv-extensionality-Elementhood-Structure : + (x y : A) → ((u : A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) + inv-extensionality-Elementhood-Structure x y = + inv-equiv (extensionality-Elementhood-Structure x y) + + eq-equiv-Elementhood-Structure : + (x y : A) → ((u : A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + eq-equiv-Elementhood-Structure x y = + map-inv-equiv (extensionality-Elementhood-Structure x y) +``` + +### The type of elements of an element + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (R@(_∈_ , _) : Elementhood-Structure l2 A) + where + + element-Elementhood-Structure : A → UU (l1 ⊔ l2) + element-Elementhood-Structure x = Σ A (_∈ x) +``` + +## Properties + +### Elementhood relations valued in localizations + +If the elementhood relation `_∈_ : A → A → Type` is valued in a +[localization](orthogonal-factorization-systems.reflective-global-subuniverses.md) +`ℒ`, then `A` is `ℒ`-[separated](foundation.separated-types-subuniverses.md). + +This is a generalization of Proposition 1 of {{#cite GS24}}. + +**Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and +the right hand side is a dependent product of equivalence types between +`ℒ`-types, and so is itself an `ℒ`-type. ∎ + +```agda +module _ + {α β : Level → Level} {l1 l2 : Level} + (ℒ : reflective-global-subuniverse α β) + {A : UU l1} (R@(_∈_ , _) : Elementhood-Structure l2 A) + where + + abstract + is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure : + ((x y : A) → is-in-reflective-global-subuniverse ℒ (x ∈ y)) → + (x y : A) → is-in-reflective-global-subuniverse ℒ (x ＝ y) + is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure + H x y = + is-closed-under-equiv-reflective-global-subuniverse ℒ + ( (u : A) → (u ∈ x) ≃ (u ∈ y)) + ( x ＝ y) + ( inv-extensionality-Elementhood-Structure R x y) + ( is-in-reflective-global-subuniverse-Π ℒ + ( λ u → is-in-reflective-global-subuniverse-equiv ℒ (H u x) (H u y))) +``` + +### Uniqueness of comprehensions + +This is Proposition 4 of {{#cite GS24}}. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (R@(_∈_ , _) : Elementhood-Structure l2 A) + where + + abstract + uniqueness-comprehension-Elementhood-Structure' : + {l3 : Level} (ϕ : A → UU l3) → + is-proof-irrelevant (Σ A (λ x → (u : A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Elementhood-Structure' ϕ (x , α) = + is-contr-equiv' + ( Σ A (x ＝_)) + ( equiv-tot + ( λ y → + equiv-Π-equiv-family + ( λ u → equiv-precomp-equiv (α u) (u ∈ y)) ∘e + ( extensionality-Elementhood-Structure R x y))) + ( is-torsorial-Id x) + + abstract + uniqueness-comprehension-Elementhood-Structure : + {l3 : Level} (ϕ : A → UU l3) → + is-prop (Σ A (λ x → (u : A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Elementhood-Structure ϕ = + is-prop-is-proof-irrelevant + ( uniqueness-comprehension-Elementhood-Structure' ϕ) +``` + +## References + +{{#bibliography}} + +## External links + +- diff --git a/src/set-theory/material-types.lagda.md b/src/set-theory/material-types.lagda.md new file mode 100644 index 00000000000..31c6d85b44b --- /dev/null +++ b/src/set-theory/material-types.lagda.md @@ -0,0 +1,189 @@ +# Material types + +```agda +module set-theory.material-types where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.locally-small-types +open import foundation.propositions +open import foundation.separated-types-subuniverses +open import foundation.subtypes +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.torsorial-type-families + +open import order-theory.accessible-elements-relations +open import order-theory.preorders + +open import orthogonal-factorization-systems.reflective-global-subuniverses + +open import set-theory.elementhood-structures +``` + +
+ +## Idea + +A {{#concept "material type" Agda=Material-Type}} is a type `A` equipped with an +[elementhood structure](set-theory.elementhood-structures.md), i.e., a +type-valued relation `_∈_ : A → A → Type` such that +`(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))` for all `x y : A`. + +**Terminology.** Such structures are commonly referred to as _material sets_ +{{#cite GS24}}. However, we reserve this name for material +[0-types](foundation-core.sets.md). + +## Definitions + +### The type of material types + +```agda +Material-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Material-Type l1 l2 = Σ (UU l1) (Elementhood-Structure l2) + +module _ + {l1 l2 : Level} (A : Material-Type l1 l2) + where + + type-Material-Type : UU l1 + type-Material-Type = pr1 A + + elementhood-structure-Material-Type : + Elementhood-Structure l2 type-Material-Type + elementhood-structure-Material-Type = pr2 A + + elementhood-Material-Type : Relation l2 type-Material-Type + elementhood-Material-Type = + elementhood-Elementhood-Structure + ( elementhood-structure-Material-Type) + + is-extensional-elementhood-structure-Material-Type : + is-extensional-elementhood-Relation elementhood-Material-Type + is-extensional-elementhood-structure-Material-Type = + is-extensional-Elementhood-Structure + ( elementhood-structure-Material-Type) + +module _ + {l1 l2 : Level} (A : Material-Type l1 l2) + (let _∈_ = elementhood-Material-Type A) + where + + equiv-elementhood-eq-Material-Type : + (x y : type-Material-Type A) → + (x ＝ y) → (u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y) + equiv-elementhood-eq-Material-Type = + equiv-eq-Elementhood-Structure + ( elementhood-structure-Material-Type A) + + extensionality-Material-Type : + (x y : type-Material-Type A) → + (x ＝ y) ≃ ((u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) + extensionality-Material-Type = + extensionality-Elementhood-Structure + ( elementhood-structure-Material-Type A) + + inv-extensionality-Material-Type : + (x y : type-Material-Type A) → + ((u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) + inv-extensionality-Material-Type = + inv-extensionality-Elementhood-Structure + ( elementhood-structure-Material-Type A) + + eq-equiv-elementhood-Material-Type : + (x y : type-Material-Type A) → + ((u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + eq-equiv-elementhood-Material-Type = + eq-equiv-Elementhood-Structure + ( elementhood-structure-Material-Type A) +``` + +### The type of elements of an element + +```agda +module _ + {l1 l2 : Level} (A : Material-Type l1 l2) + where + + element-Material-Type : type-Material-Type A → UU (l1 ⊔ l2) + element-Material-Type = + element-Elementhood-Structure (elementhood-structure-Material-Type A) +``` + +## Properties + +### Elementhood relations valued in localizations + +If the elementhood relation `_∈_ : A → A → Type` is valued in a +[localization](orthogonal-factorization-systems.reflective-global-subuniverses.md) +`ℒ`, then `A` is `ℒ`-[separated](foundation.separated-types-subuniverses.md). + +This is a generalization of Proposition 1 of {{#cite GS24}}. + +**Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and +the right hand side is a dependent product of equivalence types between +`ℒ`-types, and so is itself an `ℒ`-type. ∎ + +```agda +module _ + {α β : Level → Level} {l1 l2 : Level} + (ℒ : reflective-global-subuniverse α β) + (A : Material-Type l1 l2) + (let _∈_ = elementhood-Material-Type A) + where + + abstract + is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Type : + ( (x y : type-Material-Type A) → + is-in-reflective-global-subuniverse ℒ (x ∈ y)) → + (x y : type-Material-Type A) → + is-in-reflective-global-subuniverse ℒ (x ＝ y) + is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Type = + is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure ℒ + ( elementhood-structure-Material-Type A) +``` + +### Uniqueness of comprehensions + +This is Proposition 4 of {{#cite GS24}}. + +```agda +module _ + {l1 l2 : Level} (A : Material-Type l1 l2) + (let _∈_ = elementhood-Material-Type A) + where + + abstract + uniqueness-comprehension-Material-Type' : + {l3 : Level} (ϕ : type-Material-Type A → UU l3) → + is-proof-irrelevant + ( Σ ( type-Material-Type A) + ( λ x → (u : type-Material-Type A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Material-Type' = + uniqueness-comprehension-Elementhood-Structure' + ( elementhood-structure-Material-Type A) + + abstract + uniqueness-comprehension-Material-Type : + {l3 : Level} (ϕ : type-Material-Type A → UU l3) → + is-prop + ( Σ ( type-Material-Type A) + ( λ x → (u : type-Material-Type A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Material-Type = + uniqueness-comprehension-Elementhood-Structure + ( elementhood-structure-Material-Type A) +``` + +## References + +{{#bibliography}} diff --git a/src/set-theory/well-founded-material-types.lagda.md b/src/set-theory/well-founded-material-types.lagda.md new file mode 100644 index 00000000000..893829c0ef8 --- /dev/null +++ b/src/set-theory/well-founded-material-types.lagda.md @@ -0,0 +1,251 @@ +# Well-founded material types + +```agda +module set-theory.well-founded-material-types where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.separated-types-subuniverses +open import foundation.subtypes +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.torsorial-type-families + +open import order-theory.accessible-elements-relations +open import order-theory.preorders +open import order-theory.well-founded-relations + +open import orthogonal-factorization-systems.reflective-global-subuniverses + +open import set-theory.elementhood-structures +open import set-theory.material-types +``` + +
+ +## Idea + +A [material type](set-theory.material-types.md) `A` is +{{#concept "well-founded" Disambiguation="material type" Agda=is-well-founded-Material-Type Agda=Well-Founded-Material-Type}} +if its underlying [elementhood relation](set-theory.elementhood-structures.md) +`∈` satisfies the [property](foundation-core.propositions.md) of being +[well-founded](order-theory.well-founded-relations.md). + +Well-founded material types satisfy an induction principle: given a type family +`P : A → Type` then in order to construct an element of `P x` for all `x : A` it +suffices to construct an element of `P u` for all elements `u ∈ x`. More +precisely, the +{{#concept "well-founded induction principle" WDID=Q14402036 WD="well-founded induction" Agda=ind-Well-Founded-Material-Type}} +is a function + +```text + (x : X) → ((u : A) → (u ∈ x) → P u) → P x. +``` + +In {{#cite GS24}}, such types are said to have elementhood structures that +satisfy _foundation_. + +## Definitions + +### The predicate on a material type of being well-founded + +```agda +module _ + {l1 l2 : Level} (A : Material-Type l1 l2) + (let _∈_ = elementhood-Material-Type A) + where + + is-well-founded-Material-Type : UU (l1 ⊔ l2) + is-well-founded-Material-Type = + is-well-founded-Relation _∈_ + + is-well-founded-prop-Material-Type : Prop (l1 ⊔ l2) + is-well-founded-prop-Material-Type = + is-well-founded-prop-Relation _∈_ + + is-prop-is-well-founded-Material-Type : + is-prop is-well-founded-Material-Type + is-prop-is-well-founded-Material-Type = + is-prop-is-well-founded-Relation _∈_ +``` + +### The type of well-founded material types + +```agda +Well-Founded-Material-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Well-Founded-Material-Type l1 l2 = + Σ (Material-Type l1 l2) is-well-founded-Material-Type + +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) + where + + material-type-Well-Founded-Material-Type : Material-Type l1 l2 + material-type-Well-Founded-Material-Type = pr1 A + + is-well-founded-Well-Founded-Material-Type : + is-well-founded-Material-Type material-type-Well-Founded-Material-Type + is-well-founded-Well-Founded-Material-Type = pr2 A + + type-Well-Founded-Material-Type : UU l1 + type-Well-Founded-Material-Type = + type-Material-Type material-type-Well-Founded-Material-Type + + elementhood-structure-Well-Founded-Material-Type : + Elementhood-Structure l2 type-Well-Founded-Material-Type + elementhood-structure-Well-Founded-Material-Type = + elementhood-structure-Material-Type + ( material-type-Well-Founded-Material-Type) + + elementhood-Well-Founded-Material-Type : + Relation l2 type-Well-Founded-Material-Type + elementhood-Well-Founded-Material-Type = + elementhood-Material-Type + ( material-type-Well-Founded-Material-Type) + + is-extensional-elementhood-structure-Well-Founded-Material-Type : + is-extensional-elementhood-Relation elementhood-Well-Founded-Material-Type + is-extensional-elementhood-structure-Well-Founded-Material-Type = + is-extensional-elementhood-structure-Material-Type + ( material-type-Well-Founded-Material-Type) + + well-founded-relation-Well-Founded-Material-Type : + Well-Founded-Relation l2 type-Well-Founded-Material-Type + well-founded-relation-Well-Founded-Material-Type = + ( elementhood-Well-Founded-Material-Type , + is-well-founded-Well-Founded-Material-Type) + +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) + (let _∈_ = elementhood-Well-Founded-Material-Type A) + where + + equiv-elementhood-eq-Well-Founded-Material-Type : + (x y : type-Well-Founded-Material-Type A) → + (x ＝ y) → (u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y) + equiv-elementhood-eq-Well-Founded-Material-Type = + equiv-elementhood-eq-Material-Type + ( material-type-Well-Founded-Material-Type A) + + extensionality-Well-Founded-Material-Type : + (x y : type-Well-Founded-Material-Type A) → + (x ＝ y) ≃ ((u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) + extensionality-Well-Founded-Material-Type = + extensionality-Material-Type + ( material-type-Well-Founded-Material-Type A) + + inv-extensionality-Well-Founded-Material-Type : + (x y : type-Well-Founded-Material-Type A) → + ((u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) + inv-extensionality-Well-Founded-Material-Type = + inv-extensionality-Material-Type + ( material-type-Well-Founded-Material-Type A) + + eq-equiv-elementhood-Well-Founded-Material-Type : + (x y : type-Well-Founded-Material-Type A) → + ((u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + eq-equiv-elementhood-Well-Founded-Material-Type = + eq-equiv-elementhood-Material-Type + ( material-type-Well-Founded-Material-Type A) +``` + +### Well-founded induction + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) + (let A' = type-Well-Founded-Material-Type A) + (let _∈_ = elementhood-Well-Founded-Material-Type A) + where + + ind-Well-Founded-Material-Type : + {l3 : Level} (P : A' → UU l3) → + ({x : A'} → ({u : A'} → u ∈ x → P u) → P x) → (x : A') → P x + ind-Well-Founded-Material-Type = + ind-Well-Founded-Relation + ( well-founded-relation-Well-Founded-Material-Type A) +``` + +### The type of elements of an element + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) + where + + element-Well-Founded-Material-Type : + type-Well-Founded-Material-Type A → UU (l1 ⊔ l2) + element-Well-Founded-Material-Type = + element-Material-Type (material-type-Well-Founded-Material-Type A) +``` + +## Properties + +### Uniqueness of comprehensions + +This is Proposition 4 of {{#cite GS24}}. + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) + (let _∈_ = elementhood-Well-Founded-Material-Type A) + where + + uniqueness-comprehension-Well-Founded-Material-Type' : + {l3 : Level} (ϕ : type-Well-Founded-Material-Type A → UU l3) → + is-proof-irrelevant + ( Σ ( type-Well-Founded-Material-Type A) + ( λ x → (u : type-Well-Founded-Material-Type A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Well-Founded-Material-Type' = + uniqueness-comprehension-Material-Type' + ( material-type-Well-Founded-Material-Type A) + + uniqueness-comprehension-Well-Founded-Material-Type : + {l3 : Level} (ϕ : type-Well-Founded-Material-Type A → UU l3) → + is-prop + ( Σ ( type-Well-Founded-Material-Type A) + ( λ x → (u : type-Well-Founded-Material-Type A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Well-Founded-Material-Type = + uniqueness-comprehension-Material-Type + ( material-type-Well-Founded-Material-Type A) +``` + +## Properties + +### Well-founded elementhood relations are asymmetric + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) + (let _∈_ = elementhood-Well-Founded-Material-Type A) + where + + asymmetric-elementhood-Well-Founded-Material-Type : is-asymmetric _∈_ + asymmetric-elementhood-Well-Founded-Material-Type = + is-asymmetric-le-Well-Founded-Relation + ( well-founded-relation-Well-Founded-Material-Type A) + + irreflexive-elementhood-Well-Founded-Material-Type : is-irreflexive _∈_ + irreflexive-elementhood-Well-Founded-Material-Type = + is-irreflexive-le-Well-Founded-Relation + ( well-founded-relation-Well-Founded-Material-Type A) +``` + +## References + +{{#bibliography}} + +## External links + +- From c98ae144fea2f7e3856d49f4688dc093d830879c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Oct 2025 23:10:46 +0100 Subject: [PATCH 02/13] remove unrelated additions and edits --- .../equivalence-relations.lagda.md | 4 +- src/foundation/binary-relations.lagda.md | 30 ++-- src/foundation/decidable-relations.lagda.md | 6 +- .../exponents-set-quotients.lagda.md | 2 +- src/group-theory/grothendieck-groups.lagda.md | 2 +- ...y-of-elements-pseudometric-spaces.lagda.md | 4 +- src/order-theory.lagda.md | 1 - ...ections-closed-intervals-lattices.lagda.md | 2 +- ...ons-closed-intervals-total-orders.lagda.md | 2 +- src/order-theory/ordinals.lagda.md | 8 +- .../poset-closed-intervals-posets.lagda.md | 2 +- src/order-theory/preorders.lagda.md | 4 +- src/order-theory/strict-preorders.lagda.md | 4 +- .../strictly-preordered-sets.lagda.md | 4 +- ...l-founded-propositional-relations.lagda.md | 163 ------------------ 15 files changed, 37 insertions(+), 201 deletions(-) delete mode 100644 src/order-theory/well-founded-propositional-relations.lagda.md diff --git a/src/foundation-core/equivalence-relations.lagda.md b/src/foundation-core/equivalence-relations.lagda.md index c226e0b21e7..28396e95f5a 100644 --- a/src/foundation-core/equivalence-relations.lagda.md +++ b/src/foundation-core/equivalence-relations.lagda.md @@ -51,14 +51,14 @@ prop-equivalence-relation = pr1 sim-equivalence-relation : {l1 l2 : Level} {A : UU l1} → equivalence-relation l2 A → A → A → UU l2 -sim-equivalence-relation R = rel-Relation-Prop (prop-equivalence-relation R) +sim-equivalence-relation R = type-Relation-Prop (prop-equivalence-relation R) abstract is-prop-sim-equivalence-relation : {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A) (x y : A) → is-prop (sim-equivalence-relation R x y) is-prop-sim-equivalence-relation R = - is-prop-rel-Relation-Prop (prop-equivalence-relation R) + is-prop-type-Relation-Prop (prop-equivalence-relation R) is-prop-is-equivalence-relation : {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) → diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md index 2926407d013..36815698f5c 100644 --- a/src/foundation/binary-relations.lagda.md +++ b/src/foundation/binary-relations.lagda.md @@ -56,19 +56,19 @@ Relation-Prop : (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1) Relation-Prop l A = A → A → Prop l -rel-Relation-Prop : +type-Relation-Prop : {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → Relation l2 A -rel-Relation-Prop R x y = pr1 (R x y) +type-Relation-Prop R x y = pr1 (R x y) -is-prop-rel-Relation-Prop : +is-prop-type-Relation-Prop : {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) → - (x y : A) → is-prop (rel-Relation-Prop R x y) -is-prop-rel-Relation-Prop R x y = pr2 (R x y) + (x y : A) → is-prop (type-Relation-Prop R x y) +is-prop-type-Relation-Prop R x y = pr2 (R x y) total-space-Relation-Prop : {l : Level} {l1 : Level} {A : UU l1} → Relation-Prop l A → UU (l ⊔ l1) total-space-Relation-Prop {A = A} R = - Σ (A × A) λ (a , a') → rel-Relation-Prop R a a' + Σ (A × A) λ (a , a') → type-Relation-Prop R a a' ``` ### The predicate of being a reflexive relation @@ -96,11 +96,11 @@ module _ where is-reflexive-Relation-Prop : UU (l1 ⊔ l2) - is-reflexive-Relation-Prop = is-reflexive (rel-Relation-Prop R) + is-reflexive-Relation-Prop = is-reflexive (type-Relation-Prop R) is-prop-is-reflexive-Relation-Prop : is-prop is-reflexive-Relation-Prop is-prop-is-reflexive-Relation-Prop = - is-prop-Π (λ x → is-prop-rel-Relation-Prop R x x) + is-prop-Π (λ x → is-prop-type-Relation-Prop R x x) is-reflexive-prop-Relation-Prop : Prop (l1 ⊔ l2) is-reflexive-prop-Relation-Prop = @@ -132,12 +132,12 @@ module _ where is-symmetric-Relation-Prop : UU (l1 ⊔ l2) - is-symmetric-Relation-Prop = is-symmetric (rel-Relation-Prop R) + is-symmetric-Relation-Prop = is-symmetric (type-Relation-Prop R) is-prop-is-symmetric-Relation-Prop : is-prop is-symmetric-Relation-Prop is-prop-is-symmetric-Relation-Prop = is-prop-iterated-Π 3 - ( λ x y r → is-prop-rel-Relation-Prop R y x) + ( λ x y r → is-prop-type-Relation-Prop R y x) is-symmetric-prop-Relation-Prop : Prop (l1 ⊔ l2) is-symmetric-prop-Relation-Prop = @@ -172,14 +172,14 @@ module _ where is-transitive-Relation-Prop : UU (l1 ⊔ l2) - is-transitive-Relation-Prop = is-transitive (rel-Relation-Prop R) + is-transitive-Relation-Prop = is-transitive (type-Relation-Prop R) is-prop-is-transitive-Relation-Prop : is-prop is-transitive-Relation-Prop is-prop-is-transitive-Relation-Prop = is-prop-iterated-Π 3 ( λ x y z → is-prop-function-type - ( is-prop-function-type (is-prop-rel-Relation-Prop R x z))) + ( is-prop-function-type (is-prop-type-Relation-Prop R x z))) ``` ### The predicate of being an irreflexive relation @@ -200,7 +200,7 @@ module _ where is-irreflexive-Relation-Prop : UU (l1 ⊔ l2) - is-irreflexive-Relation-Prop = is-irreflexive (rel-Relation-Prop R) + is-irreflexive-Relation-Prop = is-irreflexive (type-Relation-Prop R) ``` ### The predicate of being an asymmetric relation @@ -242,7 +242,7 @@ module _ where is-antisymmetric-Relation-Prop : UU (l1 ⊔ l2) - is-antisymmetric-Relation-Prop = is-antisymmetric (rel-Relation-Prop R) + is-antisymmetric-Relation-Prop = is-antisymmetric (type-Relation-Prop R) ``` ### The predicate of being an entire relation @@ -271,7 +271,7 @@ module _ where is-entire-Relation-Prop : UU (l1 ⊔ l2) - is-entire-Relation-Prop = is-entire-Relation (rel-Relation-Prop R) + is-entire-Relation-Prop = is-entire-Relation (type-Relation-Prop R) ``` ## Properties diff --git a/src/foundation/decidable-relations.lagda.md b/src/foundation/decidable-relations.lagda.md index 9526fe0d401..770d4b5f81a 100644 --- a/src/foundation/decidable-relations.lagda.md +++ b/src/foundation/decidable-relations.lagda.md @@ -33,7 +33,7 @@ that each `R x y` is a decidable proposition. is-decidable-Relation-Prop : {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → UU (l1 ⊔ l2) is-decidable-Relation-Prop {A = A} R = - (x y : A) → is-decidable ( rel-Relation-Prop R x y) + (x y : A) → is-decidable ( type-Relation-Prop R x y) Decidable-Relation : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) Decidable-Relation l2 X = X → X → Decidable-Prop l2 @@ -62,8 +62,8 @@ map-inv-equiv-relation-is-decidable-Decidable-Relation : Σ ( Relation-Prop l2 X) (λ R → is-decidable-Relation-Prop R) → Decidable-Relation l2 X map-inv-equiv-relation-is-decidable-Decidable-Relation (R , d) x y = - ( ( rel-Relation-Prop R x y) , - ( is-prop-rel-Relation-Prop R x y) , + ( ( type-Relation-Prop R x y) , + ( is-prop-type-Relation-Prop R x y) , ( d x y)) equiv-relation-is-decidable-Decidable-Relation : diff --git a/src/foundation/exponents-set-quotients.lagda.md b/src/foundation/exponents-set-quotients.lagda.md index a1591975622..bfc9888f3c2 100644 --- a/src/foundation/exponents-set-quotients.lagda.md +++ b/src/foundation/exponents-set-quotients.lagda.md @@ -66,7 +66,7 @@ module _ Π-Prop X (λ x → prop-equivalence-relation R (f x) (g x)) sim-function-type : (f g : X → A) → UU (l1 ⊔ l3) - sim-function-type = rel-Relation-Prop rel-function-type + sim-function-type = type-Relation-Prop rel-function-type refl-sim-function-type : is-reflexive sim-function-type refl-sim-function-type f x = refl-equivalence-relation R (f x) diff --git a/src/group-theory/grothendieck-groups.lagda.md b/src/group-theory/grothendieck-groups.lagda.md index 973c5d05460..32f535427d8 100644 --- a/src/group-theory/grothendieck-groups.lagda.md +++ b/src/group-theory/grothendieck-groups.lagda.md @@ -84,7 +84,7 @@ module _ grothendieck-relation-Commutative-Monoid : Relation l (type-product-Commutative-Monoid M M) grothendieck-relation-Commutative-Monoid = - rel-Relation-Prop grothendieck-relation-prop-Commutative-Monoid + type-Relation-Prop grothendieck-relation-prop-Commutative-Monoid refl-grothendieck-relation-Commutative-Monoid : is-reflexive-Relation-Prop grothendieck-relation-prop-Commutative-Monoid diff --git a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md index 218e9ae9d16..f9caa041d21 100644 --- a/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md +++ b/src/metric-spaces/similarity-of-elements-pseudometric-spaces.lagda.md @@ -61,13 +61,13 @@ module _ sim-Pseudometric-Space : Relation l2 (type-Pseudometric-Space A) sim-Pseudometric-Space = - rel-Relation-Prop sim-prop-Pseudometric-Space + type-Relation-Prop sim-prop-Pseudometric-Space is-prop-sim-Pseudometric-Space : (x y : type-Pseudometric-Space A) → is-prop (sim-Pseudometric-Space x y) is-prop-sim-Pseudometric-Space = - is-prop-rel-Relation-Prop sim-prop-Pseudometric-Space + is-prop-type-Relation-Prop sim-prop-Pseudometric-Space ``` ## Properties diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index 645d6a00f3c..538d9ef2590 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -168,7 +168,6 @@ 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-propositional-relations public open import order-theory.well-founded-relations public open import order-theory.zorns-lemma public ``` diff --git a/src/order-theory/intersections-closed-intervals-lattices.lagda.md b/src/order-theory/intersections-closed-intervals-lattices.lagda.md index 29248dfabca..cd2c982e45a 100644 --- a/src/order-theory/intersections-closed-intervals-lattices.lagda.md +++ b/src/order-theory/intersections-closed-intervals-lattices.lagda.md @@ -51,7 +51,7 @@ module _ intersect-closed-interval-Lattice : Relation l2 (closed-interval-Lattice L) intersect-closed-interval-Lattice = - rel-Relation-Prop intersect-prop-closed-interval-Lattice + type-Relation-Prop intersect-prop-closed-interval-Lattice ``` ## Properties diff --git a/src/order-theory/intersections-closed-intervals-total-orders.lagda.md b/src/order-theory/intersections-closed-intervals-total-orders.lagda.md index 198057b1271..260d60218ed 100644 --- a/src/order-theory/intersections-closed-intervals-total-orders.lagda.md +++ b/src/order-theory/intersections-closed-intervals-total-orders.lagda.md @@ -51,7 +51,7 @@ module _ intersect-closed-interval-Total-Order : Relation l2 (closed-interval-Total-Order T) intersect-closed-interval-Total-Order = - rel-Relation-Prop intersect-prop-closed-interval-Total-Order + type-Relation-Prop intersect-prop-closed-interval-Total-Order ``` ## Properties diff --git a/src/order-theory/ordinals.lagda.md b/src/order-theory/ordinals.lagda.md index a5079d23b90..e805ff678ba 100644 --- a/src/order-theory/ordinals.lagda.md +++ b/src/order-theory/ordinals.lagda.md @@ -50,7 +50,7 @@ extensionality-principle-Ordinal : {l1 l2 : Level} {X : UU l1} → Relation-Prop l2 X → UU (l1 ⊔ l2) extensionality-principle-Ordinal {X = X} R = (x y : X) → - ((u : X) → rel-Relation-Prop R u x ↔ rel-Relation-Prop R u y) → x ＝ y + ((u : X) → type-Relation-Prop R u x ↔ type-Relation-Prop R u y) → x ＝ y ``` ### The predicate of being an ordinal @@ -62,7 +62,7 @@ module _ is-ordinal : UU (l1 ⊔ l2) is-ordinal = - ( is-transitive-well-founded-relation-Relation (rel-Relation-Prop R)) × + ( is-transitive-well-founded-relation-Relation (type-Relation-Prop R)) × ( extensionality-principle-Ordinal R) ``` @@ -83,7 +83,7 @@ module _ le-prop-Ordinal = pr1 (pr2 O) le-Ordinal : Relation l2 type-Ordinal - le-Ordinal = rel-Relation-Prop le-prop-Ordinal + le-Ordinal = type-Relation-Prop le-prop-Ordinal is-ordinal-Ordinal : is-ordinal le-prop-Ordinal is-ordinal-Ordinal = pr2 (pr2 O) @@ -138,7 +138,7 @@ The associated reflexive relation on an ordinal. is-prop-leq-Ordinal {y = y} = is-prop-Π ( λ u → - is-prop-function-type (is-prop-rel-Relation-Prop le-prop-Ordinal u y)) + is-prop-function-type (is-prop-type-Relation-Prop le-prop-Ordinal u y)) leq-prop-Ordinal : Relation-Prop (l1 ⊔ l2) type-Ordinal leq-prop-Ordinal x y = (leq-Ordinal x y , is-prop-leq-Ordinal) diff --git a/src/order-theory/poset-closed-intervals-posets.lagda.md b/src/order-theory/poset-closed-intervals-posets.lagda.md index 528127255c9..e9eb0d5e6cf 100644 --- a/src/order-theory/poset-closed-intervals-posets.lagda.md +++ b/src/order-theory/poset-closed-intervals-posets.lagda.md @@ -41,7 +41,7 @@ module _ leq-prop-Poset P c a ∧ leq-prop-Poset P b d leq-closed-interval-Poset : Relation l2 (closed-interval-Poset P) - leq-closed-interval-Poset = rel-Relation-Prop leq-prop-closed-interval-Poset + leq-closed-interval-Poset = type-Relation-Prop leq-prop-closed-interval-Poset ``` ## Properties diff --git a/src/order-theory/preorders.lagda.md b/src/order-theory/preorders.lagda.md index 1dd65cde20c..1601ec8858f 100644 --- a/src/order-theory/preorders.lagda.md +++ b/src/order-theory/preorders.lagda.md @@ -63,7 +63,7 @@ module _ leq-Preorder x y = type-Prop (leq-prop-Preorder x y) is-prop-leq-Preorder : (x y : type-Preorder) → is-prop (leq-Preorder x y) - is-prop-leq-Preorder = is-prop-rel-Relation-Prop leq-prop-Preorder + is-prop-leq-Preorder = is-prop-type-Relation-Prop leq-prop-Preorder concatenate-eq-leq-Preorder' : {x y z : type-Preorder} → x ＝ y → leq-Preorder x z → leq-Preorder y z @@ -97,7 +97,7 @@ module _ le-Preorder x y = type-Prop (le-prop-Preorder x y) is-prop-le-Preorder : (x y : type-Preorder) → is-prop (le-Preorder x y) - is-prop-le-Preorder = is-prop-rel-Relation-Prop le-prop-Preorder + is-prop-le-Preorder = is-prop-type-Relation-Prop le-prop-Preorder refl-leq-Preorder : is-reflexive leq-Preorder refl-leq-Preorder = pr1 (pr2 (pr2 X)) diff --git a/src/order-theory/strict-preorders.lagda.md b/src/order-theory/strict-preorders.lagda.md index b9bb6c9d469..6f1a4b4392e 100644 --- a/src/order-theory/strict-preorders.lagda.md +++ b/src/order-theory/strict-preorders.lagda.md @@ -61,13 +61,13 @@ module _ le-Strict-Preorder : Relation l2 type-Strict-Preorder le-Strict-Preorder = - rel-Relation-Prop le-prop-Strict-Preorder + type-Relation-Prop le-prop-Strict-Preorder is-prop-le-Strict-Preorder : (x y : type-Strict-Preorder) → is-prop (le-Strict-Preorder x y) is-prop-le-Strict-Preorder = - is-prop-rel-Relation-Prop le-prop-Strict-Preorder + is-prop-type-Relation-Prop le-prop-Strict-Preorder is-irreflexive-le-Strict-Preorder : is-irreflexive le-Strict-Preorder diff --git a/src/order-theory/strictly-preordered-sets.lagda.md b/src/order-theory/strictly-preordered-sets.lagda.md index 9f7d58c9dd1..a5a458b6d8f 100644 --- a/src/order-theory/strictly-preordered-sets.lagda.md +++ b/src/order-theory/strictly-preordered-sets.lagda.md @@ -81,13 +81,13 @@ module _ le-Strictly-Preordered-Set : Relation l2 type-Strictly-Preordered-Set le-Strictly-Preordered-Set = - rel-Relation-Prop le-prop-Strictly-Preordered-Set + type-Relation-Prop le-prop-Strictly-Preordered-Set is-prop-le-Strictly-Preordered-Set : (x y : type-Strictly-Preordered-Set) → is-prop (le-Strictly-Preordered-Set x y) is-prop-le-Strictly-Preordered-Set = - is-prop-rel-Relation-Prop le-prop-Strictly-Preordered-Set + is-prop-type-Relation-Prop le-prop-Strictly-Preordered-Set is-irreflexive-le-Strictly-Preordered-Set : is-irreflexive le-Strictly-Preordered-Set diff --git a/src/order-theory/well-founded-propositional-relations.lagda.md b/src/order-theory/well-founded-propositional-relations.lagda.md deleted file mode 100644 index 7081e72372d..00000000000 --- a/src/order-theory/well-founded-propositional-relations.lagda.md +++ /dev/null @@ -1,163 +0,0 @@ -# Well-founded propositional relations - -```agda -module order-theory.well-founded-propositional-relations where -``` - -
Imports - -```agda -open import foundation.binary-relations -open import foundation.dependent-pair-types -open import foundation.function-types -open import foundation.identity-types -open import foundation.propositions -open import foundation.universal-quantification -open import foundation.universe-levels - -open import order-theory.accessible-elements-relations -open import order-theory.preorders -open import order-theory.well-founded-relations -``` - -
- -## Idea - -Given a type `X` equipped with a -[binary propositional relation](foundation.binary-relations.md) -`_<_ : X → X → Prop` we say that the relation `_<_` is -{{#concept "well-founded" Disambiguation="binary propositional relation" WDID=Q338021 WD="well-founded relation" Agda=is-well-founded-Relation-Prop Agda=Well-Founded-Relation-Prop}} -if all elements of `X` are -[accessible](order-theory.accessible-elements-relations.md) with respect to -`_<_`. - -Well-founded propositional relations satisfy an induction principle: In order to -construct an element of `P x` for all `x : X` it suffices to construct an -element of `P y` for all elements `y < x`. More precisely, the -{{#concept "well-founded induction principle" WDID=Q14402036 WD="well-founded induction" Agda=ind-Well-Founded-Relation-Prop-Prop}} -is a function - -```text - (x : X) → ((u : X) → (u < x) → P u) → P x. -``` - -## Definitions - -### The predicate of being a well-founded propositional relation - -```agda -module _ - {l1 l2 : Level} {X : UU l1} (_<_ : Relation-Prop l2 X) - where - - is-well-founded-prop-Relation-Prop : Prop (l1 ⊔ l2) - is-well-founded-prop-Relation-Prop = - is-well-founded-prop-Relation (rel-Relation-Prop _<_) - - is-well-founded-Relation-Prop : UU (l1 ⊔ l2) - is-well-founded-Relation-Prop = type-Prop is-well-founded-prop-Relation-Prop - - is-prop-is-well-founded-Relation-Prop : is-prop is-well-founded-Relation-Prop - is-prop-is-well-founded-Relation-Prop = - is-prop-type-Prop is-well-founded-prop-Relation-Prop -``` - -### Well-founded propositional relations - -```agda -Well-Founded-Relation-Prop : - {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) -Well-Founded-Relation-Prop l X = - Σ (Relation-Prop l X) is-well-founded-Relation-Prop - -module _ - {l1 l2 : Level} {X : UU l1} (R : Well-Founded-Relation-Prop l2 X) - where - - rel-prop-Well-Founded-Relation-Prop : Relation-Prop l2 X - rel-prop-Well-Founded-Relation-Prop = pr1 R - - rel-Well-Founded-Relation-Prop : Relation l2 X - rel-Well-Founded-Relation-Prop = - rel-Relation-Prop rel-prop-Well-Founded-Relation-Prop - - is-well-founded-Well-Founded-Relation-Prop : - is-well-founded-Relation-Prop rel-prop-Well-Founded-Relation-Prop - is-well-founded-Well-Founded-Relation-Prop = pr2 R -``` - -### Well-founded induction - -```agda -module _ - {l1 l2 l3 : Level} {X : UU l1} - ((R , w) : Well-Founded-Relation-Prop l2 X) - (let _<_ = rel-Relation-Prop R) - (P : X → UU l3) - where - - ind-Well-Founded-Relation-Prop : - ({x : X} → ({y : X} → y < x → P y) → P x) → (x : X) → P x - ind-Well-Founded-Relation-Prop IH x = - ind-accessible-element-Relation _<_ P (λ _ → IH) (w x) -``` - -## Properties - -### A well-founded propositional relation is asymmetric, and thus irreflexive - -```agda -module _ - {l1 l2 : Level} {X : UU l1} ((R , w) : Well-Founded-Relation-Prop l2 X) - (let _<_ = rel-Relation-Prop R) - where - - is-asymmetric-le-Well-Founded-Relation-Prop : is-asymmetric _<_ - is-asymmetric-le-Well-Founded-Relation-Prop x y = - is-asymmetric-is-accessible-element-Relation _<_ (w x) - - is-irreflexive-le-Well-Founded-Relation-Prop : is-irreflexive _<_ - is-irreflexive-le-Well-Founded-Relation-Prop = - is-irreflexive-is-asymmetric _<_ is-asymmetric-le-Well-Founded-Relation-Prop -``` - -### The associated reflexive propositional relation of a well-founded propositional relation - -Given a well-founded relation $<$ on $X$ there is an associated reflexive -relation given by - -$$ - (x ≤ y) := ∀ (u : X), (u < x) ⇒ (u < y). -$$ - -```agda -module _ - {l1 l2 : Level} {X : UU l1} - ((_<_ , w) : Well-Founded-Relation-Prop l2 X) - where - - leq-prop-Well-Founded-Relation-Prop : Relation-Prop (l1 ⊔ l2) X - leq-prop-Well-Founded-Relation-Prop x y = ∀' X (λ u → u < x ⇒ u < y) - - leq-Well-Founded-Relation-Prop : Relation (l1 ⊔ l2) X - leq-Well-Founded-Relation-Prop = - rel-Relation-Prop leq-prop-Well-Founded-Relation-Prop - - refl-leq-Well-Founded-Relation-Prop : - is-reflexive leq-Well-Founded-Relation-Prop - refl-leq-Well-Founded-Relation-Prop x u = id - - leq-eq-Well-Founded-Relation-Prop : - {x y : X} → x ＝ y → leq-Well-Founded-Relation-Prop x y - leq-eq-Well-Founded-Relation-Prop {x} refl = - refl-leq-Well-Founded-Relation-Prop x - - transitive-leq-Well-Founded-Relation-Prop : - is-transitive leq-Well-Founded-Relation-Prop - transitive-leq-Well-Founded-Relation-Prop x y z f g t H = f t (g t H) -``` - -## See also - -- [Well-founded relations](order-theory.well-founded-relations.md). From 2cda52fa135ce829825bcf06731210a1f6f5cc7e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 27 Oct 2025 23:25:29 +0100 Subject: [PATCH 03/13] fix name --- src/set-theory.lagda.md | 4 +- src/set-theory/material-sets.lagda.md | 190 +++++++++++++ src/set-theory/material-types.lagda.md | 189 ------------- .../well-founded-material-sets.lagda.md | 251 ++++++++++++++++++ .../well-founded-material-types.lagda.md | 251 ------------------ 5 files changed, 443 insertions(+), 442 deletions(-) create mode 100644 src/set-theory/material-sets.lagda.md delete mode 100644 src/set-theory/material-types.lagda.md create mode 100644 src/set-theory/well-founded-material-sets.lagda.md delete mode 100644 src/set-theory/well-founded-material-types.lagda.md diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md index 4335c1c9989..6b3bf0fcf7e 100644 --- a/src/set-theory.lagda.md +++ b/src/set-theory.lagda.md @@ -61,12 +61,12 @@ open import set-theory.inclusion-natural-numbers-increasing-binary-sequences pub open import set-theory.increasing-binary-sequences public open import set-theory.inequality-increasing-binary-sequences public open import set-theory.infinite-sets public -open import set-theory.material-types public +open import set-theory.material-sets public open import set-theory.positive-elements-increasing-binary-sequences public open import set-theory.russells-paradox public open import set-theory.strict-lower-bounds-increasing-binary-sequences public open import set-theory.uncountable-sets public -open import set-theory.well-founded-material-types public +open import set-theory.well-founded-material-sets public ``` ## See also diff --git a/src/set-theory/material-sets.lagda.md b/src/set-theory/material-sets.lagda.md new file mode 100644 index 00000000000..e1696827730 --- /dev/null +++ b/src/set-theory/material-sets.lagda.md @@ -0,0 +1,190 @@ +# Material sets + +```agda +module set-theory.material-sets where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.locally-small-types +open import foundation.propositions +open import foundation.separated-types-subuniverses +open import foundation.subtypes +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.torsorial-type-families + +open import order-theory.accessible-elements-relations +open import order-theory.preorders + +open import orthogonal-factorization-systems.reflective-global-subuniverses + +open import set-theory.elementhood-structures +``` + +
+ +## Idea + +A {{#concept "material set" Agda=Material-Set}} is a type `A` equipped with an +[elementhood structure](set-theory.elementhood-structures.md), i.e., a +type-valued relation `_∈_ : A → A → Type` such that +`(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))` for all `x y : A`. + +**Terminology.** Note that a material set does not generally define a homotopy +set in the sense of [0-types](foundation-core.sets.md). Here, by _set_ is is +instead meant that we have structure with an appropriate notion of +"elementhood". + +## Definitions + +### The type of material sets + +```agda +Material-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Material-Set l1 l2 = Σ (UU l1) (Elementhood-Structure l2) + +module _ + {l1 l2 : Level} (A : Material-Set l1 l2) + where + + type-Material-Set : UU l1 + type-Material-Set = pr1 A + + elementhood-structure-Material-Set : + Elementhood-Structure l2 type-Material-Set + elementhood-structure-Material-Set = pr2 A + + elementhood-Material-Set : Relation l2 type-Material-Set + elementhood-Material-Set = + elementhood-Elementhood-Structure + ( elementhood-structure-Material-Set) + + is-extensional-elementhood-structure-Material-Set : + is-extensional-elementhood-Relation elementhood-Material-Set + is-extensional-elementhood-structure-Material-Set = + is-extensional-Elementhood-Structure + ( elementhood-structure-Material-Set) + +module _ + {l1 l2 : Level} (A : Material-Set l1 l2) + (let _∈_ = elementhood-Material-Set A) + where + + equiv-elementhood-eq-Material-Set : + (x y : type-Material-Set A) → + (x ＝ y) → (u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y) + equiv-elementhood-eq-Material-Set = + equiv-eq-Elementhood-Structure + ( elementhood-structure-Material-Set A) + + extensionality-Material-Set : + (x y : type-Material-Set A) → + (x ＝ y) ≃ ((u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) + extensionality-Material-Set = + extensionality-Elementhood-Structure + ( elementhood-structure-Material-Set A) + + inv-extensionality-Material-Set : + (x y : type-Material-Set A) → + ((u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) + inv-extensionality-Material-Set = + inv-extensionality-Elementhood-Structure + ( elementhood-structure-Material-Set A) + + eq-equiv-elementhood-Material-Set : + (x y : type-Material-Set A) → + ((u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + eq-equiv-elementhood-Material-Set = + eq-equiv-Elementhood-Structure + ( elementhood-structure-Material-Set A) +``` + +### The type of elements of an element + +```agda +module _ + {l1 l2 : Level} (A : Material-Set l1 l2) + where + + element-Material-Set : type-Material-Set A → UU (l1 ⊔ l2) + element-Material-Set = + element-Elementhood-Structure (elementhood-structure-Material-Set A) +``` + +## Properties + +### Elementhood relations valued in localizations + +If the elementhood relation `_∈_ : A → A → Type` is valued in a +[localization](orthogonal-factorization-systems.reflective-global-subuniverses.md) +`ℒ`, then `A` is `ℒ`-[separated](foundation.separated-types-subuniverses.md). + +This is a generalization of Proposition 1 of {{#cite GS24}}. + +**Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and +the right hand side is a dependent product of equivalence types between +`ℒ`-types, and so is itself an `ℒ`-type. ∎ + +```agda +module _ + {α β : Level → Level} {l1 l2 : Level} + (ℒ : reflective-global-subuniverse α β) + (A : Material-Set l1 l2) + (let _∈_ = elementhood-Material-Set A) + where + + abstract + is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set : + ( (x y : type-Material-Set A) → + is-in-reflective-global-subuniverse ℒ (x ∈ y)) → + (x y : type-Material-Set A) → + is-in-reflective-global-subuniverse ℒ (x ＝ y) + is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set = + is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure ℒ + ( elementhood-structure-Material-Set A) +``` + +### Uniqueness of comprehensions + +This is Proposition 4 of {{#cite GS24}}. + +```agda +module _ + {l1 l2 : Level} (A : Material-Set l1 l2) + (let _∈_ = elementhood-Material-Set A) + where + + abstract + uniqueness-comprehension-Material-Set' : + {l3 : Level} (ϕ : type-Material-Set A → UU l3) → + is-proof-irrelevant + ( Σ ( type-Material-Set A) + ( λ x → (u : type-Material-Set A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Material-Set' = + uniqueness-comprehension-Elementhood-Structure' + ( elementhood-structure-Material-Set A) + + abstract + uniqueness-comprehension-Material-Set : + {l3 : Level} (ϕ : type-Material-Set A → UU l3) → + is-prop + ( Σ ( type-Material-Set A) + ( λ x → (u : type-Material-Set A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Material-Set = + uniqueness-comprehension-Elementhood-Structure + ( elementhood-structure-Material-Set A) +``` + +## References + +{{#bibliography}} diff --git a/src/set-theory/material-types.lagda.md b/src/set-theory/material-types.lagda.md deleted file mode 100644 index 31c6d85b44b..00000000000 --- a/src/set-theory/material-types.lagda.md +++ /dev/null @@ -1,189 +0,0 @@ -# Material types - -```agda -module set-theory.material-types where -``` - -
Imports - -```agda -open import foundation.binary-relations -open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.identity-types -open import foundation.locally-small-types -open import foundation.propositions -open import foundation.separated-types-subuniverses -open import foundation.subtypes -open import foundation.universe-levels - -open import foundation-core.contractible-types -open import foundation-core.torsorial-type-families - -open import order-theory.accessible-elements-relations -open import order-theory.preorders - -open import orthogonal-factorization-systems.reflective-global-subuniverses - -open import set-theory.elementhood-structures -``` - -
- -## Idea - -A {{#concept "material type" Agda=Material-Type}} is a type `A` equipped with an -[elementhood structure](set-theory.elementhood-structures.md), i.e., a -type-valued relation `_∈_ : A → A → Type` such that -`(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))` for all `x y : A`. - -**Terminology.** Such structures are commonly referred to as _material sets_ -{{#cite GS24}}. However, we reserve this name for material -[0-types](foundation-core.sets.md). - -## Definitions - -### The type of material types - -```agda -Material-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) -Material-Type l1 l2 = Σ (UU l1) (Elementhood-Structure l2) - -module _ - {l1 l2 : Level} (A : Material-Type l1 l2) - where - - type-Material-Type : UU l1 - type-Material-Type = pr1 A - - elementhood-structure-Material-Type : - Elementhood-Structure l2 type-Material-Type - elementhood-structure-Material-Type = pr2 A - - elementhood-Material-Type : Relation l2 type-Material-Type - elementhood-Material-Type = - elementhood-Elementhood-Structure - ( elementhood-structure-Material-Type) - - is-extensional-elementhood-structure-Material-Type : - is-extensional-elementhood-Relation elementhood-Material-Type - is-extensional-elementhood-structure-Material-Type = - is-extensional-Elementhood-Structure - ( elementhood-structure-Material-Type) - -module _ - {l1 l2 : Level} (A : Material-Type l1 l2) - (let _∈_ = elementhood-Material-Type A) - where - - equiv-elementhood-eq-Material-Type : - (x y : type-Material-Type A) → - (x ＝ y) → (u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y) - equiv-elementhood-eq-Material-Type = - equiv-eq-Elementhood-Structure - ( elementhood-structure-Material-Type A) - - extensionality-Material-Type : - (x y : type-Material-Type A) → - (x ＝ y) ≃ ((u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) - extensionality-Material-Type = - extensionality-Elementhood-Structure - ( elementhood-structure-Material-Type A) - - inv-extensionality-Material-Type : - (x y : type-Material-Type A) → - ((u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) - inv-extensionality-Material-Type = - inv-extensionality-Elementhood-Structure - ( elementhood-structure-Material-Type A) - - eq-equiv-elementhood-Material-Type : - (x y : type-Material-Type A) → - ((u : type-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) - eq-equiv-elementhood-Material-Type = - eq-equiv-Elementhood-Structure - ( elementhood-structure-Material-Type A) -``` - -### The type of elements of an element - -```agda -module _ - {l1 l2 : Level} (A : Material-Type l1 l2) - where - - element-Material-Type : type-Material-Type A → UU (l1 ⊔ l2) - element-Material-Type = - element-Elementhood-Structure (elementhood-structure-Material-Type A) -``` - -## Properties - -### Elementhood relations valued in localizations - -If the elementhood relation `_∈_ : A → A → Type` is valued in a -[localization](orthogonal-factorization-systems.reflective-global-subuniverses.md) -`ℒ`, then `A` is `ℒ`-[separated](foundation.separated-types-subuniverses.md). - -This is a generalization of Proposition 1 of {{#cite GS24}}. - -**Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and -the right hand side is a dependent product of equivalence types between -`ℒ`-types, and so is itself an `ℒ`-type. ∎ - -```agda -module _ - {α β : Level → Level} {l1 l2 : Level} - (ℒ : reflective-global-subuniverse α β) - (A : Material-Type l1 l2) - (let _∈_ = elementhood-Material-Type A) - where - - abstract - is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Type : - ( (x y : type-Material-Type A) → - is-in-reflective-global-subuniverse ℒ (x ∈ y)) → - (x y : type-Material-Type A) → - is-in-reflective-global-subuniverse ℒ (x ＝ y) - is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Type = - is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure ℒ - ( elementhood-structure-Material-Type A) -``` - -### Uniqueness of comprehensions - -This is Proposition 4 of {{#cite GS24}}. - -```agda -module _ - {l1 l2 : Level} (A : Material-Type l1 l2) - (let _∈_ = elementhood-Material-Type A) - where - - abstract - uniqueness-comprehension-Material-Type' : - {l3 : Level} (ϕ : type-Material-Type A → UU l3) → - is-proof-irrelevant - ( Σ ( type-Material-Type A) - ( λ x → (u : type-Material-Type A) → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Material-Type' = - uniqueness-comprehension-Elementhood-Structure' - ( elementhood-structure-Material-Type A) - - abstract - uniqueness-comprehension-Material-Type : - {l3 : Level} (ϕ : type-Material-Type A → UU l3) → - is-prop - ( Σ ( type-Material-Type A) - ( λ x → (u : type-Material-Type A) → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Material-Type = - uniqueness-comprehension-Elementhood-Structure - ( elementhood-structure-Material-Type A) -``` - -## References - -{{#bibliography}} diff --git a/src/set-theory/well-founded-material-sets.lagda.md b/src/set-theory/well-founded-material-sets.lagda.md new file mode 100644 index 00000000000..40d26cdb889 --- /dev/null +++ b/src/set-theory/well-founded-material-sets.lagda.md @@ -0,0 +1,251 @@ +# Well-founded material sets + +```agda +module set-theory.well-founded-material-sets where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.separated-types-subuniverses +open import foundation.subtypes +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.torsorial-type-families + +open import order-theory.accessible-elements-relations +open import order-theory.preorders +open import order-theory.well-founded-relations + +open import orthogonal-factorization-systems.reflective-global-subuniverses + +open import set-theory.elementhood-structures +open import set-theory.material-sets +``` + +
+ +## Idea + +A [material set](set-theory.material-sets.md) `A` is +{{#concept "well-founded" Disambiguation="material set" Agda=is-well-founded-Material-Set Agda=Well-Founded-Material-Set}} +if its underlying [elementhood relation](set-theory.elementhood-structures.md) +`∈` satisfies the [property](foundation-core.propositions.md) of being +[well-founded](order-theory.well-founded-relations.md). + +Well-founded material sets satisfy an induction principle: given a type family +`P : A → Type` then in order to construct an element of `P x` for all `x : A` it +suffices to construct an element of `P u` for all elements `u ∈ x`. More +precisely, the +{{#concept "well-founded induction principle" WDID=Q14402036 WD="well-founded induction" Agda=ind-Well-Founded-Material-Set}} +is a function + +```text + (x : X) → ((u : A) → (u ∈ x) → P u) → P x. +``` + +In {{#cite GS24}}, such types are said to have elementhood structures that +satisfy _foundation_. + +## Definitions + +### The predicate on a material set of being well-founded + +```agda +module _ + {l1 l2 : Level} (A : Material-Set l1 l2) + (let _∈_ = elementhood-Material-Set A) + where + + is-well-founded-Material-Set : UU (l1 ⊔ l2) + is-well-founded-Material-Set = + is-well-founded-Relation _∈_ + + is-well-founded-prop-Material-Set : Prop (l1 ⊔ l2) + is-well-founded-prop-Material-Set = + is-well-founded-prop-Relation _∈_ + + is-prop-is-well-founded-Material-Set : + is-prop is-well-founded-Material-Set + is-prop-is-well-founded-Material-Set = + is-prop-is-well-founded-Relation _∈_ +``` + +### The type of well-founded material sets + +```agda +Well-Founded-Material-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Well-Founded-Material-Set l1 l2 = + Σ (Material-Set l1 l2) is-well-founded-Material-Set + +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + where + + material-set-Well-Founded-Material-Set : Material-Set l1 l2 + material-set-Well-Founded-Material-Set = pr1 A + + is-well-founded-Well-Founded-Material-Set : + is-well-founded-Material-Set material-set-Well-Founded-Material-Set + is-well-founded-Well-Founded-Material-Set = pr2 A + + type-Well-Founded-Material-Set : UU l1 + type-Well-Founded-Material-Set = + type-Material-Set material-set-Well-Founded-Material-Set + + elementhood-structure-Well-Founded-Material-Set : + Elementhood-Structure l2 type-Well-Founded-Material-Set + elementhood-structure-Well-Founded-Material-Set = + elementhood-structure-Material-Set + ( material-set-Well-Founded-Material-Set) + + elementhood-Well-Founded-Material-Set : + Relation l2 type-Well-Founded-Material-Set + elementhood-Well-Founded-Material-Set = + elementhood-Material-Set + ( material-set-Well-Founded-Material-Set) + + is-extensional-elementhood-structure-Well-Founded-Material-Set : + is-extensional-elementhood-Relation elementhood-Well-Founded-Material-Set + is-extensional-elementhood-structure-Well-Founded-Material-Set = + is-extensional-elementhood-structure-Material-Set + ( material-set-Well-Founded-Material-Set) + + well-founded-relation-Well-Founded-Material-Set : + Well-Founded-Relation l2 type-Well-Founded-Material-Set + well-founded-relation-Well-Founded-Material-Set = + ( elementhood-Well-Founded-Material-Set , + is-well-founded-Well-Founded-Material-Set) + +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + (let _∈_ = elementhood-Well-Founded-Material-Set A) + where + + equiv-elementhood-eq-Well-Founded-Material-Set : + (x y : type-Well-Founded-Material-Set A) → + (x ＝ y) → (u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y) + equiv-elementhood-eq-Well-Founded-Material-Set = + equiv-elementhood-eq-Material-Set + ( material-set-Well-Founded-Material-Set A) + + extensionality-Well-Founded-Material-Set : + (x y : type-Well-Founded-Material-Set A) → + (x ＝ y) ≃ ((u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) + extensionality-Well-Founded-Material-Set = + extensionality-Material-Set + ( material-set-Well-Founded-Material-Set A) + + inv-extensionality-Well-Founded-Material-Set : + (x y : type-Well-Founded-Material-Set A) → + ((u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) + inv-extensionality-Well-Founded-Material-Set = + inv-extensionality-Material-Set + ( material-set-Well-Founded-Material-Set A) + + eq-equiv-elementhood-Well-Founded-Material-Set : + (x y : type-Well-Founded-Material-Set A) → + ((u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + eq-equiv-elementhood-Well-Founded-Material-Set = + eq-equiv-elementhood-Material-Set + ( material-set-Well-Founded-Material-Set A) +``` + +### Well-founded induction + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + (let A' = type-Well-Founded-Material-Set A) + (let _∈_ = elementhood-Well-Founded-Material-Set A) + where + + ind-Well-Founded-Material-Set : + {l3 : Level} (P : A' → UU l3) → + ({x : A'} → ({u : A'} → u ∈ x → P u) → P x) → (x : A') → P x + ind-Well-Founded-Material-Set = + ind-Well-Founded-Relation + ( well-founded-relation-Well-Founded-Material-Set A) +``` + +### The type of elements of an element + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + where + + element-Well-Founded-Material-Set : + type-Well-Founded-Material-Set A → UU (l1 ⊔ l2) + element-Well-Founded-Material-Set = + element-Material-Set (material-set-Well-Founded-Material-Set A) +``` + +## Properties + +### Uniqueness of comprehensions + +This is Proposition 4 of {{#cite GS24}}. + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + (let _∈_ = elementhood-Well-Founded-Material-Set A) + where + + uniqueness-comprehension-Well-Founded-Material-Set' : + {l3 : Level} (ϕ : type-Well-Founded-Material-Set A → UU l3) → + is-proof-irrelevant + ( Σ ( type-Well-Founded-Material-Set A) + ( λ x → (u : type-Well-Founded-Material-Set A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Well-Founded-Material-Set' = + uniqueness-comprehension-Material-Set' + ( material-set-Well-Founded-Material-Set A) + + uniqueness-comprehension-Well-Founded-Material-Set : + {l3 : Level} (ϕ : type-Well-Founded-Material-Set A → UU l3) → + is-prop + ( Σ ( type-Well-Founded-Material-Set A) + ( λ x → (u : type-Well-Founded-Material-Set A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Well-Founded-Material-Set = + uniqueness-comprehension-Material-Set + ( material-set-Well-Founded-Material-Set A) +``` + +## Properties + +### Well-founded elementhood relations are asymmetric + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + (let _∈_ = elementhood-Well-Founded-Material-Set A) + where + + asymmetric-elementhood-Well-Founded-Material-Set : is-asymmetric _∈_ + asymmetric-elementhood-Well-Founded-Material-Set = + is-asymmetric-le-Well-Founded-Relation + ( well-founded-relation-Well-Founded-Material-Set A) + + irreflexive-elementhood-Well-Founded-Material-Set : is-irreflexive _∈_ + irreflexive-elementhood-Well-Founded-Material-Set = + is-irreflexive-le-Well-Founded-Relation + ( well-founded-relation-Well-Founded-Material-Set A) +``` + +## References + +{{#bibliography}} + +## External links + +- diff --git a/src/set-theory/well-founded-material-types.lagda.md b/src/set-theory/well-founded-material-types.lagda.md deleted file mode 100644 index 893829c0ef8..00000000000 --- a/src/set-theory/well-founded-material-types.lagda.md +++ /dev/null @@ -1,251 +0,0 @@ -# Well-founded material types - -```agda -module set-theory.well-founded-material-types where -``` - -
Imports - -```agda -open import foundation.binary-relations -open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types -open import foundation.identity-types -open import foundation.propositions -open import foundation.separated-types-subuniverses -open import foundation.subtypes -open import foundation.universe-levels - -open import foundation-core.contractible-types -open import foundation-core.torsorial-type-families - -open import order-theory.accessible-elements-relations -open import order-theory.preorders -open import order-theory.well-founded-relations - -open import orthogonal-factorization-systems.reflective-global-subuniverses - -open import set-theory.elementhood-structures -open import set-theory.material-types -``` - -
- -## Idea - -A [material type](set-theory.material-types.md) `A` is -{{#concept "well-founded" Disambiguation="material type" Agda=is-well-founded-Material-Type Agda=Well-Founded-Material-Type}} -if its underlying [elementhood relation](set-theory.elementhood-structures.md) -`∈` satisfies the [property](foundation-core.propositions.md) of being -[well-founded](order-theory.well-founded-relations.md). - -Well-founded material types satisfy an induction principle: given a type family -`P : A → Type` then in order to construct an element of `P x` for all `x : A` it -suffices to construct an element of `P u` for all elements `u ∈ x`. More -precisely, the -{{#concept "well-founded induction principle" WDID=Q14402036 WD="well-founded induction" Agda=ind-Well-Founded-Material-Type}} -is a function - -```text - (x : X) → ((u : A) → (u ∈ x) → P u) → P x. -``` - -In {{#cite GS24}}, such types are said to have elementhood structures that -satisfy _foundation_. - -## Definitions - -### The predicate on a material type of being well-founded - -```agda -module _ - {l1 l2 : Level} (A : Material-Type l1 l2) - (let _∈_ = elementhood-Material-Type A) - where - - is-well-founded-Material-Type : UU (l1 ⊔ l2) - is-well-founded-Material-Type = - is-well-founded-Relation _∈_ - - is-well-founded-prop-Material-Type : Prop (l1 ⊔ l2) - is-well-founded-prop-Material-Type = - is-well-founded-prop-Relation _∈_ - - is-prop-is-well-founded-Material-Type : - is-prop is-well-founded-Material-Type - is-prop-is-well-founded-Material-Type = - is-prop-is-well-founded-Relation _∈_ -``` - -### The type of well-founded material types - -```agda -Well-Founded-Material-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) -Well-Founded-Material-Type l1 l2 = - Σ (Material-Type l1 l2) is-well-founded-Material-Type - -module _ - {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) - where - - material-type-Well-Founded-Material-Type : Material-Type l1 l2 - material-type-Well-Founded-Material-Type = pr1 A - - is-well-founded-Well-Founded-Material-Type : - is-well-founded-Material-Type material-type-Well-Founded-Material-Type - is-well-founded-Well-Founded-Material-Type = pr2 A - - type-Well-Founded-Material-Type : UU l1 - type-Well-Founded-Material-Type = - type-Material-Type material-type-Well-Founded-Material-Type - - elementhood-structure-Well-Founded-Material-Type : - Elementhood-Structure l2 type-Well-Founded-Material-Type - elementhood-structure-Well-Founded-Material-Type = - elementhood-structure-Material-Type - ( material-type-Well-Founded-Material-Type) - - elementhood-Well-Founded-Material-Type : - Relation l2 type-Well-Founded-Material-Type - elementhood-Well-Founded-Material-Type = - elementhood-Material-Type - ( material-type-Well-Founded-Material-Type) - - is-extensional-elementhood-structure-Well-Founded-Material-Type : - is-extensional-elementhood-Relation elementhood-Well-Founded-Material-Type - is-extensional-elementhood-structure-Well-Founded-Material-Type = - is-extensional-elementhood-structure-Material-Type - ( material-type-Well-Founded-Material-Type) - - well-founded-relation-Well-Founded-Material-Type : - Well-Founded-Relation l2 type-Well-Founded-Material-Type - well-founded-relation-Well-Founded-Material-Type = - ( elementhood-Well-Founded-Material-Type , - is-well-founded-Well-Founded-Material-Type) - -module _ - {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) - (let _∈_ = elementhood-Well-Founded-Material-Type A) - where - - equiv-elementhood-eq-Well-Founded-Material-Type : - (x y : type-Well-Founded-Material-Type A) → - (x ＝ y) → (u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y) - equiv-elementhood-eq-Well-Founded-Material-Type = - equiv-elementhood-eq-Material-Type - ( material-type-Well-Founded-Material-Type A) - - extensionality-Well-Founded-Material-Type : - (x y : type-Well-Founded-Material-Type A) → - (x ＝ y) ≃ ((u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) - extensionality-Well-Founded-Material-Type = - extensionality-Material-Type - ( material-type-Well-Founded-Material-Type A) - - inv-extensionality-Well-Founded-Material-Type : - (x y : type-Well-Founded-Material-Type A) → - ((u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) - inv-extensionality-Well-Founded-Material-Type = - inv-extensionality-Material-Type - ( material-type-Well-Founded-Material-Type A) - - eq-equiv-elementhood-Well-Founded-Material-Type : - (x y : type-Well-Founded-Material-Type A) → - ((u : type-Well-Founded-Material-Type A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) - eq-equiv-elementhood-Well-Founded-Material-Type = - eq-equiv-elementhood-Material-Type - ( material-type-Well-Founded-Material-Type A) -``` - -### Well-founded induction - -```agda -module _ - {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) - (let A' = type-Well-Founded-Material-Type A) - (let _∈_ = elementhood-Well-Founded-Material-Type A) - where - - ind-Well-Founded-Material-Type : - {l3 : Level} (P : A' → UU l3) → - ({x : A'} → ({u : A'} → u ∈ x → P u) → P x) → (x : A') → P x - ind-Well-Founded-Material-Type = - ind-Well-Founded-Relation - ( well-founded-relation-Well-Founded-Material-Type A) -``` - -### The type of elements of an element - -```agda -module _ - {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) - where - - element-Well-Founded-Material-Type : - type-Well-Founded-Material-Type A → UU (l1 ⊔ l2) - element-Well-Founded-Material-Type = - element-Material-Type (material-type-Well-Founded-Material-Type A) -``` - -## Properties - -### Uniqueness of comprehensions - -This is Proposition 4 of {{#cite GS24}}. - -```agda -module _ - {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) - (let _∈_ = elementhood-Well-Founded-Material-Type A) - where - - uniqueness-comprehension-Well-Founded-Material-Type' : - {l3 : Level} (ϕ : type-Well-Founded-Material-Type A → UU l3) → - is-proof-irrelevant - ( Σ ( type-Well-Founded-Material-Type A) - ( λ x → (u : type-Well-Founded-Material-Type A) → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Well-Founded-Material-Type' = - uniqueness-comprehension-Material-Type' - ( material-type-Well-Founded-Material-Type A) - - uniqueness-comprehension-Well-Founded-Material-Type : - {l3 : Level} (ϕ : type-Well-Founded-Material-Type A → UU l3) → - is-prop - ( Σ ( type-Well-Founded-Material-Type A) - ( λ x → (u : type-Well-Founded-Material-Type A) → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Well-Founded-Material-Type = - uniqueness-comprehension-Material-Type - ( material-type-Well-Founded-Material-Type A) -``` - -## Properties - -### Well-founded elementhood relations are asymmetric - -```agda -module _ - {l1 l2 : Level} (A : Well-Founded-Material-Type l1 l2) - (let _∈_ = elementhood-Well-Founded-Material-Type A) - where - - asymmetric-elementhood-Well-Founded-Material-Type : is-asymmetric _∈_ - asymmetric-elementhood-Well-Founded-Material-Type = - is-asymmetric-le-Well-Founded-Relation - ( well-founded-relation-Well-Founded-Material-Type A) - - irreflexive-elementhood-Well-Founded-Material-Type : is-irreflexive _∈_ - irreflexive-elementhood-Well-Founded-Material-Type = - is-irreflexive-le-Well-Founded-Relation - ( well-founded-relation-Well-Founded-Material-Type A) -``` - -## References - -{{#bibliography}} - -## External links - -- From 007234433a23d6dd4f1fbc8722dfda35c047be91 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 28 Oct 2025 12:44:15 +0100 Subject: [PATCH 04/13] remove additional projects --- docs/PROJECTS.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/docs/PROJECTS.md b/docs/PROJECTS.md index e0a12e68097..6bde141651e 100644 --- a/docs/PROJECTS.md +++ b/docs/PROJECTS.md @@ -5,8 +5,6 @@ Here is a list of projects that use the agda-unimath library: - - - -- -- If your project uses the agda-unimath library, let us know, so we can add your project to the list. From 5883035f556ea580b6968325e5ad0ab7bfad1d8b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 10:52:06 +0100 Subject: [PATCH 05/13] Update src/set-theory/elementhood-structures.lagda.md Co-authored-by: Elisabeth Stenholm <55891497+elisabethstenholm@users.noreply.github.com> --- src/set-theory/elementhood-structures.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/set-theory/elementhood-structures.lagda.md b/src/set-theory/elementhood-structures.lagda.md index 5565e3c9b36..8e131956330 100644 --- a/src/set-theory/elementhood-structures.lagda.md +++ b/src/set-theory/elementhood-structures.lagda.md @@ -214,4 +214,4 @@ module _ ## External links -- +- From 202c2e6aab9a2dc4a96be93c910ad7a3fba06680 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 10:52:18 +0100 Subject: [PATCH 06/13] Update src/set-theory/well-founded-material-sets.lagda.md Co-authored-by: Elisabeth Stenholm <55891497+elisabethstenholm@users.noreply.github.com> --- src/set-theory/well-founded-material-sets.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/set-theory/well-founded-material-sets.lagda.md b/src/set-theory/well-founded-material-sets.lagda.md index 40d26cdb889..d25e2b2df87 100644 --- a/src/set-theory/well-founded-material-sets.lagda.md +++ b/src/set-theory/well-founded-material-sets.lagda.md @@ -248,4 +248,4 @@ module _ ## External links -- +- From b839cd7c73980bb5edbfa0d8deb981e5d4979a7a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 10:53:01 +0100 Subject: [PATCH 07/13] review --- docs/PROJECTS.md | 1 - references.bib | 15 ++++++++++++--- src/set-theory/elementhood-structures.lagda.md | 4 ++-- src/set-theory/material-sets.lagda.md | 4 ++-- .../well-founded-material-sets.lagda.md | 4 ++-- 5 files changed, 18 insertions(+), 10 deletions(-) diff --git a/docs/PROJECTS.md b/docs/PROJECTS.md index 6bde141651e..58f6c901359 100644 --- a/docs/PROJECTS.md +++ b/docs/PROJECTS.md @@ -4,7 +4,6 @@ Here is a list of projects that use the agda-unimath library: - - -- If your project uses the agda-unimath library, let us know, so we can add your project to the list. diff --git a/references.bib b/references.bib index 953eda4cd45..26bfe9f10bc 100644 --- a/references.bib +++ b/references.bib @@ -520,13 +520,22 @@ @article{GK12 issn = {1469-8064}, } -@misc{GS24, - title = {Univalent Material Set Theory}, +@article{GS26, + title = {Univalent material set theory}, author = {Håkon Robbestad Gylterud and Elisabeth Stenholm}, - year = 2024, + year = 2026, + journal = {Annals of Pure and Applied Logic}, + volume = 177, + number = 2, + pages = 103662, + doi = {https://doi.org/10.1016/j.apal.2025.103662}, + issn = {0168-0072}, eprint = {2312.13024}, archiveprefix = {arXiv}, primaryclass = {math.LO}, + url = {https://www.sciencedirect.com/science/article/pii/S0168007225001113}, + keywords = {Type theory, Homotopy type theory, Constructive set theory, Material set theory}, + abstract = {Homotopy type theory (HoTT) can be seen as a generalisation of structural set theory, in the sense that 0-types represent structural sets within the more general notion of types. For material set theory, we also have concrete models as 0-types in HoTT, but this does not currently have any generalisation to higher types. The aim of this paper is to give such a generalisation of material set theory to higher type levels within homotopy type theory. This is achieved by generalising the construction of the type of iterative sets to obtain an n-type universe of n-types. At level 1, this gives a connection between groupoids and multisets. More specifically, we define the notion of an ∈-structure as a type with an extensional binary type family and generalise the axioms of constructive set theory to higher type levels. There is a tight connection between the univalence axiom and the extensionality axiom of ∈-structures. Once an ∈-structure is given, its elements can be seen as representing types in the ambient type theory. A useful property of these structures is that an ∈-structure of n-types is itself an n-type, as opposed to univalent universes, which have higher type levels than the types in the universe. The theory has an alternative, coalgebraic formulation, in terms of coalgebras for a certain hierarchy of functors, Pn, which generalises the powerset functor from sub-types to covering spaces and n-connected maps in general. The coalgebras which furthermore are fixed-points of their respective functors in the hierarchy are shown to model the axioms given in the first part. As concrete examples of models for the theory developed we construct the initial algebras of the Pn functors. In addition to being an example of initial algebras of non-polynomial functors, this construction allows one to start with a univalent universe and get a hierarchy of ∈-structures which gives a stratified ∈-structure representation of that universe. These types are moreover n-type universes of n-types which contain all the usual types an type formers. The universes are cumulative both with respect to universe levels and with respect to type levels. The results are formalised in the proof-assistant Agda.}, } @book{Johnstone02, diff --git a/src/set-theory/elementhood-structures.lagda.md b/src/set-theory/elementhood-structures.lagda.md index 8e131956330..b7d82382af3 100644 --- a/src/set-theory/elementhood-structures.lagda.md +++ b/src/set-theory/elementhood-structures.lagda.md @@ -149,7 +149,7 @@ If the elementhood relation `_∈_ : A → A → Type` is valued in a [localization](orthogonal-factorization-systems.reflective-global-subuniverses.md) `ℒ`, then `A` is `ℒ`-[separated](foundation.separated-types-subuniverses.md). -This is a generalization of Proposition 1 of {{#cite GS24}}. +This is a generalization of Proposition 1 of {{#cite GS26}}. **Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and the right hand side is a dependent product of equivalence types between @@ -178,7 +178,7 @@ module _ ### Uniqueness of comprehensions -This is Proposition 4 of {{#cite GS24}}. +This is Proposition 4 of {{#cite GS26}}. ```agda module _ diff --git a/src/set-theory/material-sets.lagda.md b/src/set-theory/material-sets.lagda.md index e1696827730..9f37da9eb1e 100644 --- a/src/set-theory/material-sets.lagda.md +++ b/src/set-theory/material-sets.lagda.md @@ -129,7 +129,7 @@ If the elementhood relation `_∈_ : A → A → Type` is valued in a [localization](orthogonal-factorization-systems.reflective-global-subuniverses.md) `ℒ`, then `A` is `ℒ`-[separated](foundation.separated-types-subuniverses.md). -This is a generalization of Proposition 1 of {{#cite GS24}}. +This is a generalization of Proposition 1 of {{#cite GS26}}. **Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and the right hand side is a dependent product of equivalence types between @@ -156,7 +156,7 @@ module _ ### Uniqueness of comprehensions -This is Proposition 4 of {{#cite GS24}}. +This is Proposition 4 of {{#cite GS26}}. ```agda module _ diff --git a/src/set-theory/well-founded-material-sets.lagda.md b/src/set-theory/well-founded-material-sets.lagda.md index d25e2b2df87..d3780682447 100644 --- a/src/set-theory/well-founded-material-sets.lagda.md +++ b/src/set-theory/well-founded-material-sets.lagda.md @@ -53,7 +53,7 @@ is a function (x : X) → ((u : A) → (u ∈ x) → P u) → P x. ``` -In {{#cite GS24}}, such types are said to have elementhood structures that +In {{#cite GS26}}, such types are said to have elementhood structures that satisfy _foundation_. ## Definitions @@ -194,7 +194,7 @@ module _ ### Uniqueness of comprehensions -This is Proposition 4 of {{#cite GS24}}. +This is Proposition 4 of {{#cite GS26}}. ```agda module _ From 4815b3b6f4d8973558b3d99fbe0d673d9be07d84 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 11:07:20 +0100 Subject: [PATCH 08/13] edits --- .../elementhood-structures.lagda.md | 15 ++---- src/set-theory/material-sets.lagda.md | 45 +++++------------ .../well-founded-material-sets.lagda.md | 49 ++++++++----------- 3 files changed, 38 insertions(+), 71 deletions(-) diff --git a/src/set-theory/elementhood-structures.lagda.md b/src/set-theory/elementhood-structures.lagda.md index b7d82382af3..a699ebf278c 100644 --- a/src/set-theory/elementhood-structures.lagda.md +++ b/src/set-theory/elementhood-structures.lagda.md @@ -10,21 +10,16 @@ module set-theory.elementhood-structures where open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositions -open import foundation.separated-types-subuniverses open import foundation.subtypes open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.torsorial-type-families -open import order-theory.accessible-elements-relations -open import order-theory.preorders - open import orthogonal-factorization-systems.reflective-global-subuniverses ``` @@ -109,14 +104,14 @@ module _ is-extensional-Elementhood-Structure = pr2 R equiv-eq-Elementhood-Structure : - (x y : A) → (x ＝ y) → (u : A) → (u ∈ x) ≃ (u ∈ y) + {x y : A} → (x ＝ y) → (u : A) → (u ∈ x) ≃ (u ∈ y) equiv-eq-Elementhood-Structure = - equiv-elementhood-eq-Relation _∈_ + equiv-elementhood-eq-Relation _∈_ _ _ extensionality-Elementhood-Structure : (x y : A) → (x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y)) extensionality-Elementhood-Structure x y = - ( equiv-eq-Elementhood-Structure x y , + ( equiv-eq-Elementhood-Structure , is-extensional-Elementhood-Structure x y) inv-extensionality-Elementhood-Structure : @@ -125,8 +120,8 @@ module _ inv-equiv (extensionality-Elementhood-Structure x y) eq-equiv-Elementhood-Structure : - (x y : A) → ((u : A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) - eq-equiv-Elementhood-Structure x y = + {x y : A} → ((u : A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + eq-equiv-Elementhood-Structure {x} {y} = map-inv-equiv (extensionality-Elementhood-Structure x y) ``` diff --git a/src/set-theory/material-sets.lagda.md b/src/set-theory/material-sets.lagda.md index 9f37da9eb1e..81607459404 100644 --- a/src/set-theory/material-sets.lagda.md +++ b/src/set-theory/material-sets.lagda.md @@ -10,22 +10,10 @@ module set-theory.material-sets where open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types open import foundation.identity-types -open import foundation.locally-small-types open import foundation.propositions -open import foundation.separated-types-subuniverses -open import foundation.subtypes open import foundation.universe-levels -open import foundation-core.contractible-types -open import foundation-core.torsorial-type-families - -open import order-theory.accessible-elements-relations -open import order-theory.preorders - open import orthogonal-factorization-systems.reflective-global-subuniverses open import set-theory.elementhood-structures @@ -77,33 +65,30 @@ module _ module _ {l1 l2 : Level} (A : Material-Set l1 l2) + (let A' = type-Material-Set A) (let _∈_ = elementhood-Material-Set A) where equiv-elementhood-eq-Material-Set : - (x y : type-Material-Set A) → - (x ＝ y) → (u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y) + {x y : A'} → (x ＝ y) → (u : A') → (u ∈ x) ≃ (u ∈ y) equiv-elementhood-eq-Material-Set = equiv-eq-Elementhood-Structure ( elementhood-structure-Material-Set A) extensionality-Material-Set : - (x y : type-Material-Set A) → - (x ＝ y) ≃ ((u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) + (x y : A') → (x ＝ y) ≃ ((u : A') → (u ∈ x) ≃ (u ∈ y)) extensionality-Material-Set = extensionality-Elementhood-Structure ( elementhood-structure-Material-Set A) inv-extensionality-Material-Set : - (x y : type-Material-Set A) → - ((u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) + (x y : A') → ((u : A') → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) inv-extensionality-Material-Set = inv-extensionality-Elementhood-Structure ( elementhood-structure-Material-Set A) eq-equiv-elementhood-Material-Set : - (x y : type-Material-Set A) → - ((u : type-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + {x y : A'} → ((u : A') → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) eq-equiv-elementhood-Material-Set = eq-equiv-Elementhood-Structure ( elementhood-structure-Material-Set A) @@ -140,15 +125,14 @@ module _ {α β : Level → Level} {l1 l2 : Level} (ℒ : reflective-global-subuniverse α β) (A : Material-Set l1 l2) + (let A' = type-Material-Set A) (let _∈_ = elementhood-Material-Set A) where abstract is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set : - ( (x y : type-Material-Set A) → - is-in-reflective-global-subuniverse ℒ (x ∈ y)) → - (x y : type-Material-Set A) → - is-in-reflective-global-subuniverse ℒ (x ＝ y) + ( (x y : A') → is-in-reflective-global-subuniverse ℒ (x ∈ y)) → + (x y : A') → is-in-reflective-global-subuniverse ℒ (x ＝ y) is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set = is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure ℒ ( elementhood-structure-Material-Set A) @@ -161,25 +145,22 @@ This is Proposition 4 of {{#cite GS26}}. ```agda module _ {l1 l2 : Level} (A : Material-Set l1 l2) + (let A' = type-Material-Set A) (let _∈_ = elementhood-Material-Set A) where abstract uniqueness-comprehension-Material-Set' : - {l3 : Level} (ϕ : type-Material-Set A → UU l3) → - is-proof-irrelevant - ( Σ ( type-Material-Set A) - ( λ x → (u : type-Material-Set A) → ϕ u ≃ (u ∈ x))) + {l3 : Level} (ϕ : A' → UU l3) → + is-proof-irrelevant (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) uniqueness-comprehension-Material-Set' = uniqueness-comprehension-Elementhood-Structure' ( elementhood-structure-Material-Set A) abstract uniqueness-comprehension-Material-Set : - {l3 : Level} (ϕ : type-Material-Set A → UU l3) → - is-prop - ( Σ ( type-Material-Set A) - ( λ x → (u : type-Material-Set A) → ϕ u ≃ (u ∈ x))) + {l3 : Level} (ϕ : A' → UU l3) → + is-prop (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) uniqueness-comprehension-Material-Set = uniqueness-comprehension-Elementhood-Structure ( elementhood-structure-Material-Set A) diff --git a/src/set-theory/well-founded-material-sets.lagda.md b/src/set-theory/well-founded-material-sets.lagda.md index d3780682447..363f692b4cc 100644 --- a/src/set-theory/well-founded-material-sets.lagda.md +++ b/src/set-theory/well-founded-material-sets.lagda.md @@ -10,24 +10,12 @@ module set-theory.well-founded-material-sets where open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.function-types -open import foundation.functoriality-dependent-function-types -open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositions -open import foundation.separated-types-subuniverses -open import foundation.subtypes open import foundation.universe-levels -open import foundation-core.contractible-types -open import foundation-core.torsorial-type-families - -open import order-theory.accessible-elements-relations -open import order-theory.preorders open import order-theory.well-founded-relations -open import orthogonal-factorization-systems.reflective-global-subuniverses - open import set-theory.elementhood-structures open import set-theory.material-sets ``` @@ -128,33 +116,30 @@ module _ module _ {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + (let A' = type-Well-Founded-Material-Set A) (let _∈_ = elementhood-Well-Founded-Material-Set A) where equiv-elementhood-eq-Well-Founded-Material-Set : - (x y : type-Well-Founded-Material-Set A) → - (x ＝ y) → (u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y) + {x y : A'} → (x ＝ y) → (u : A') → (u ∈ x) ≃ (u ∈ y) equiv-elementhood-eq-Well-Founded-Material-Set = equiv-elementhood-eq-Material-Set ( material-set-Well-Founded-Material-Set A) extensionality-Well-Founded-Material-Set : - (x y : type-Well-Founded-Material-Set A) → - (x ＝ y) ≃ ((u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) + (x y : A') → (x ＝ y) ≃ ((u : A') → (u ∈ x) ≃ (u ∈ y)) extensionality-Well-Founded-Material-Set = extensionality-Material-Set ( material-set-Well-Founded-Material-Set A) inv-extensionality-Well-Founded-Material-Set : - (x y : type-Well-Founded-Material-Set A) → - ((u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) + (x y : A') → ((u : A') → (u ∈ x) ≃ (u ∈ y)) ≃ (x ＝ y) inv-extensionality-Well-Founded-Material-Set = inv-extensionality-Material-Set ( material-set-Well-Founded-Material-Set A) eq-equiv-elementhood-Well-Founded-Material-Set : - (x y : type-Well-Founded-Material-Set A) → - ((u : type-Well-Founded-Material-Set A) → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) + {x y : A'} → ((u : A') → (u ∈ x) ≃ (u ∈ y)) → (x ＝ y) eq-equiv-elementhood-Well-Founded-Material-Set = eq-equiv-elementhood-Material-Set ( material-set-Well-Founded-Material-Set A) @@ -199,23 +184,20 @@ This is Proposition 4 of {{#cite GS26}}. ```agda module _ {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + (let A' = type-Well-Founded-Material-Set A) (let _∈_ = elementhood-Well-Founded-Material-Set A) where uniqueness-comprehension-Well-Founded-Material-Set' : - {l3 : Level} (ϕ : type-Well-Founded-Material-Set A → UU l3) → - is-proof-irrelevant - ( Σ ( type-Well-Founded-Material-Set A) - ( λ x → (u : type-Well-Founded-Material-Set A) → ϕ u ≃ (u ∈ x))) + {l3 : Level} (ϕ : A' → UU l3) → + is-proof-irrelevant (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) uniqueness-comprehension-Well-Founded-Material-Set' = uniqueness-comprehension-Material-Set' ( material-set-Well-Founded-Material-Set A) uniqueness-comprehension-Well-Founded-Material-Set : - {l3 : Level} (ϕ : type-Well-Founded-Material-Set A → UU l3) → - is-prop - ( Σ ( type-Well-Founded-Material-Set A) - ( λ x → (u : type-Well-Founded-Material-Set A) → ϕ u ≃ (u ∈ x))) + {l3 : Level} (ϕ : A' → UU l3) → + is-prop (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) uniqueness-comprehension-Well-Founded-Material-Set = uniqueness-comprehension-Material-Set ( material-set-Well-Founded-Material-Set A) @@ -235,6 +217,15 @@ module _ asymmetric-elementhood-Well-Founded-Material-Set = is-asymmetric-le-Well-Founded-Relation ( well-founded-relation-Well-Founded-Material-Set A) +``` + +### Well-founded elementhood relations are irreflexive + +```agda +module _ + {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) + (let _∈_ = elementhood-Well-Founded-Material-Set A) + where irreflexive-elementhood-Well-Founded-Material-Set : is-irreflexive _∈_ irreflexive-elementhood-Well-Founded-Material-Set = @@ -248,4 +239,4 @@ module _ ## External links -- +- From 13c34977677ec519006116574487d85fd73954dc Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 11:08:36 +0100 Subject: [PATCH 09/13] edit --- src/set-theory/well-founded-material-sets.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/set-theory/well-founded-material-sets.lagda.md b/src/set-theory/well-founded-material-sets.lagda.md index 363f692b4cc..3cd33d645ba 100644 --- a/src/set-theory/well-founded-material-sets.lagda.md +++ b/src/set-theory/well-founded-material-sets.lagda.md @@ -34,7 +34,7 @@ Well-founded material sets satisfy an induction principle: given a type family `P : A → Type` then in order to construct an element of `P x` for all `x : A` it suffices to construct an element of `P u` for all elements `u ∈ x`. More precisely, the -{{#concept "well-founded induction principle" WDID=Q14402036 WD="well-founded induction" Agda=ind-Well-Founded-Material-Set}} +{{#concept "well-founded induction principle" Disambiguation="of a well-founded material set" WDID=Q14402036 WD="well-founded induction" Agda=ind-Well-Founded-Material-Set}} is a function ```text From b72444c95e523c3407c2d98aa61c40e2fb61161d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 11:30:24 +0100 Subject: [PATCH 10/13] edit --- references.bib | 1 - 1 file changed, 1 deletion(-) diff --git a/references.bib b/references.bib index 26bfe9f10bc..56d024317d0 100644 --- a/references.bib +++ b/references.bib @@ -533,7 +533,6 @@ @article{GS26 eprint = {2312.13024}, archiveprefix = {arXiv}, primaryclass = {math.LO}, - url = {https://www.sciencedirect.com/science/article/pii/S0168007225001113}, keywords = {Type theory, Homotopy type theory, Constructive set theory, Material set theory}, abstract = {Homotopy type theory (HoTT) can be seen as a generalisation of structural set theory, in the sense that 0-types represent structural sets within the more general notion of types. For material set theory, we also have concrete models as 0-types in HoTT, but this does not currently have any generalisation to higher types. The aim of this paper is to give such a generalisation of material set theory to higher type levels within homotopy type theory. This is achieved by generalising the construction of the type of iterative sets to obtain an n-type universe of n-types. At level 1, this gives a connection between groupoids and multisets. More specifically, we define the notion of an ∈-structure as a type with an extensional binary type family and generalise the axioms of constructive set theory to higher type levels. There is a tight connection between the univalence axiom and the extensionality axiom of ∈-structures. Once an ∈-structure is given, its elements can be seen as representing types in the ambient type theory. A useful property of these structures is that an ∈-structure of n-types is itself an n-type, as opposed to univalent universes, which have higher type levels than the types in the universe. The theory has an alternative, coalgebraic formulation, in terms of coalgebras for a certain hierarchy of functors, Pn, which generalises the powerset functor from sub-types to covering spaces and n-connected maps in general. The coalgebras which furthermore are fixed-points of their respective functors in the hierarchy are shown to model the axioms given in the first part. As concrete examples of models for the theory developed we construct the initial algebras of the Pn functors. In addition to being an example of initial algebras of non-polynomial functors, this construction allows one to start with a univalent universe and get a hierarchy of ∈-structures which gives a stratified ∈-structure representation of that universe. These types are moreover n-type universes of n-types which contain all the usual types an type formers. The universes are cumulative both with respect to universe levels and with respect to type levels. The results are formalised in the proof-assistant Agda.}, } From 0ce2212139853f54b487b7c8176486ca7360a200 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 11:37:27 +0100 Subject: [PATCH 11/13] more edits --- .../elementhood-structures.lagda.md | 71 +++++++++---------- src/set-theory/material-sets.lagda.md | 49 ++++++------- .../well-founded-material-sets.lagda.md | 8 +-- 3 files changed, 60 insertions(+), 68 deletions(-) diff --git a/src/set-theory/elementhood-structures.lagda.md b/src/set-theory/elementhood-structures.lagda.md index a699ebf278c..c8ef2823269 100644 --- a/src/set-theory/elementhood-structures.lagda.md +++ b/src/set-theory/elementhood-structures.lagda.md @@ -155,20 +155,19 @@ module _ {α β : Level → Level} {l1 l2 : Level} (ℒ : reflective-global-subuniverse α β) {A : UU l1} (R@(_∈_ , _) : Elementhood-Structure l2 A) - where - - abstract - is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure : - ((x y : A) → is-in-reflective-global-subuniverse ℒ (x ∈ y)) → - (x y : A) → is-in-reflective-global-subuniverse ℒ (x ＝ y) - is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure - H x y = - is-closed-under-equiv-reflective-global-subuniverse ℒ - ( (u : A) → (u ∈ x) ≃ (u ∈ y)) - ( x ＝ y) - ( inv-extensionality-Elementhood-Structure R x y) - ( is-in-reflective-global-subuniverse-Π ℒ - ( λ u → is-in-reflective-global-subuniverse-equiv ℒ (H u x) (H u y))) + where abstract + + is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure : + ((x y : A) → is-in-reflective-global-subuniverse ℒ (x ∈ y)) → + (x y : A) → is-in-reflective-global-subuniverse ℒ (x ＝ y) + is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure + H x y = + is-closed-under-equiv-reflective-global-subuniverse ℒ + ( (u : A) → (u ∈ x) ≃ (u ∈ y)) + ( x ＝ y) + ( inv-extensionality-Elementhood-Structure R x y) + ( is-in-reflective-global-subuniverse-Π ℒ + ( λ u → is-in-reflective-global-subuniverse-equiv ℒ (H u x) (H u y))) ``` ### Uniqueness of comprehensions @@ -178,29 +177,27 @@ This is Proposition 4 of {{#cite GS26}}. ```agda module _ {l1 l2 : Level} {A : UU l1} (R@(_∈_ , _) : Elementhood-Structure l2 A) - where - - abstract - uniqueness-comprehension-Elementhood-Structure' : - {l3 : Level} (ϕ : A → UU l3) → - is-proof-irrelevant (Σ A (λ x → (u : A) → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Elementhood-Structure' ϕ (x , α) = - is-contr-equiv' - ( Σ A (x ＝_)) - ( equiv-tot - ( λ y → - equiv-Π-equiv-family - ( λ u → equiv-precomp-equiv (α u) (u ∈ y)) ∘e - ( extensionality-Elementhood-Structure R x y))) - ( is-torsorial-Id x) - - abstract - uniqueness-comprehension-Elementhood-Structure : - {l3 : Level} (ϕ : A → UU l3) → - is-prop (Σ A (λ x → (u : A) → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Elementhood-Structure ϕ = - is-prop-is-proof-irrelevant - ( uniqueness-comprehension-Elementhood-Structure' ϕ) + where abstract + + uniqueness-comprehension-Elementhood-Structure' : + {l3 : Level} (ϕ : A → UU l3) → + is-proof-irrelevant (Σ A (λ x → (u : A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Elementhood-Structure' ϕ (x , α) = + is-contr-equiv' + ( Σ A (x ＝_)) + ( equiv-tot + ( λ y → + equiv-Π-equiv-family + ( λ u → equiv-precomp-equiv (α u) (u ∈ y)) ∘e + ( extensionality-Elementhood-Structure R x y))) + ( is-torsorial-Id x) + + uniqueness-comprehension-Elementhood-Structure : + {l3 : Level} (ϕ : A → UU l3) → + is-prop (Σ A (λ x → (u : A) → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Elementhood-Structure ϕ = + is-prop-is-proof-irrelevant + ( uniqueness-comprehension-Elementhood-Structure' ϕ) ``` ## References diff --git a/src/set-theory/material-sets.lagda.md b/src/set-theory/material-sets.lagda.md index 81607459404..4ac80a4a0b4 100644 --- a/src/set-theory/material-sets.lagda.md +++ b/src/set-theory/material-sets.lagda.md @@ -108,7 +108,7 @@ module _ ## Properties -### Elementhood relations valued in localizations +### Separation of material sets at localizations If the elementhood relation `_∈_ : A → A → Type` is valued in a [localization](orthogonal-factorization-systems.reflective-global-subuniverses.md) @@ -127,15 +127,14 @@ module _ (A : Material-Set l1 l2) (let A' = type-Material-Set A) (let _∈_ = elementhood-Material-Set A) - where - - abstract - is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set : - ( (x y : A') → is-in-reflective-global-subuniverse ℒ (x ∈ y)) → - (x y : A') → is-in-reflective-global-subuniverse ℒ (x ＝ y) - is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set = - is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure ℒ - ( elementhood-structure-Material-Set A) + where abstract + + is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set : + ( (x y : A') → is-in-reflective-global-subuniverse ℒ (x ∈ y)) → + (x y : A') → is-in-reflective-global-subuniverse ℒ (x ＝ y) + is-separated-type-is-in-global-reflective-subuniverse-elementhood-Material-Set = + is-separated-is-in-global-reflective-subuniverse-Elementhood-Structure ℒ + ( elementhood-structure-Material-Set A) ``` ### Uniqueness of comprehensions @@ -147,23 +146,21 @@ module _ {l1 l2 : Level} (A : Material-Set l1 l2) (let A' = type-Material-Set A) (let _∈_ = elementhood-Material-Set A) - where + where abstract - abstract - uniqueness-comprehension-Material-Set' : - {l3 : Level} (ϕ : A' → UU l3) → - is-proof-irrelevant (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Material-Set' = - uniqueness-comprehension-Elementhood-Structure' - ( elementhood-structure-Material-Set A) - - abstract - uniqueness-comprehension-Material-Set : - {l3 : Level} (ϕ : A' → UU l3) → - is-prop (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) - uniqueness-comprehension-Material-Set = - uniqueness-comprehension-Elementhood-Structure - ( elementhood-structure-Material-Set A) + uniqueness-comprehension-Material-Set' : + {l3 : Level} (ϕ : A' → UU l3) → + is-proof-irrelevant (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Material-Set' = + uniqueness-comprehension-Elementhood-Structure' + ( elementhood-structure-Material-Set A) + + uniqueness-comprehension-Material-Set : + {l3 : Level} (ϕ : A' → UU l3) → + is-prop (Σ A' (λ x → (u : A') → ϕ u ≃ (u ∈ x))) + uniqueness-comprehension-Material-Set = + uniqueness-comprehension-Elementhood-Structure + ( elementhood-structure-Material-Set A) ``` ## References diff --git a/src/set-theory/well-founded-material-sets.lagda.md b/src/set-theory/well-founded-material-sets.lagda.md index 3cd33d645ba..456bc0c6721 100644 --- a/src/set-theory/well-founded-material-sets.lagda.md +++ b/src/set-theory/well-founded-material-sets.lagda.md @@ -186,7 +186,7 @@ module _ {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) (let A' = type-Well-Founded-Material-Set A) (let _∈_ = elementhood-Well-Founded-Material-Set A) - where + where abstract uniqueness-comprehension-Well-Founded-Material-Set' : {l3 : Level} (ϕ : A' → UU l3) → @@ -203,15 +203,13 @@ module _ ( material-set-Well-Founded-Material-Set A) ``` -## Properties - ### Well-founded elementhood relations are asymmetric ```agda module _ {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) (let _∈_ = elementhood-Well-Founded-Material-Set A) - where + where abstract asymmetric-elementhood-Well-Founded-Material-Set : is-asymmetric _∈_ asymmetric-elementhood-Well-Founded-Material-Set = @@ -225,7 +223,7 @@ module _ module _ {l1 l2 : Level} (A : Well-Founded-Material-Set l1 l2) (let _∈_ = elementhood-Well-Founded-Material-Set A) - where + where abstract irreflexive-elementhood-Well-Founded-Material-Set : is-irreflexive _∈_ irreflexive-elementhood-Well-Founded-Material-Set = From 62f46adcb88104d24d2dc56c128cbfd947f7da4f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 13:28:23 +0100 Subject: [PATCH 12/13] typos --- src/set-theory/elementhood-structures.lagda.md | 2 +- src/set-theory/material-sets.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/set-theory/elementhood-structures.lagda.md b/src/set-theory/elementhood-structures.lagda.md index c8ef2823269..bd39f531eba 100644 --- a/src/set-theory/elementhood-structures.lagda.md +++ b/src/set-theory/elementhood-structures.lagda.md @@ -148,7 +148,7 @@ This is a generalization of Proposition 1 of {{#cite GS26}}. **Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and the right hand side is a dependent product of equivalence types between -`ℒ`-types, and so is itself an `ℒ`-type. ∎ +`ℒ`-types and so is itself an `ℒ`-type. ∎ ```agda module _ diff --git a/src/set-theory/material-sets.lagda.md b/src/set-theory/material-sets.lagda.md index 4ac80a4a0b4..b3e536f303f 100644 --- a/src/set-theory/material-sets.lagda.md +++ b/src/set-theory/material-sets.lagda.md @@ -29,7 +29,7 @@ type-valued relation `_∈_ : A → A → Type` such that `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))` for all `x y : A`. **Terminology.** Note that a material set does not generally define a homotopy -set in the sense of [0-types](foundation-core.sets.md). Here, by _set_ is is +set in the sense of [0-types](foundation-core.sets.md). Here, by _set_ it is instead meant that we have structure with an appropriate notion of "elementhood". @@ -118,7 +118,7 @@ This is a generalization of Proposition 1 of {{#cite GS26}}. **Proof.** By extensionality, `(x ＝ y) ≃ ((u : A) → (u ∈ x) ≃ (u ∈ y))`, and the right hand side is a dependent product of equivalence types between -`ℒ`-types, and so is itself an `ℒ`-type. ∎ +`ℒ`-types and so is itself an `ℒ`-type. ∎ ```agda module _ From 63e5f7fdf15e295cab90b75947e2d0838d4e2b29 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 29 Oct 2025 13:42:25 +0100 Subject: [PATCH 13/13] wikidata "is an element of" --- src/set-theory/elementhood-structures.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/set-theory/elementhood-structures.lagda.md b/src/set-theory/elementhood-structures.lagda.md index bd39f531eba..38fde1291a6 100644 --- a/src/set-theory/elementhood-structures.lagda.md +++ b/src/set-theory/elementhood-structures.lagda.md @@ -41,7 +41,7 @@ is an [equivalence](foundation-core.equivalences.md). An extensional elementhood relation on `A` endows the type `A` with the [structure](foundation.structure.md) of -{{#concept "elementhood" Disambiguation="on a type" Agda=Elementhood-Structure}}. +{{#concept "elementhood" Disambiguation="on a type" Agda=Elementhood-Structure WD="is an element of" WDID=Q655288}}. ## Definitions