diff --git a/src/finite-group-theory/transpositions.lagda.md b/src/finite-group-theory/transpositions.lagda.md index a38bb0720cb..2b61f3fe91b 100644 --- a/src/finite-group-theory/transpositions.lagda.md +++ b/src/finite-group-theory/transpositions.lagda.md @@ -446,11 +446,11 @@ module _ apply-universal-property-trunc-Prop (pr2 Y) ( coproduct-Prop ( Id-Prop - ( pair X (is-set-count eX)) + ( set-type-count eX) ( pr1 two-elements-transposition) ( x)) ( Id-Prop - ( pair X (is-set-count eX)) + ( set-type-count eX) ( pr1 (pr2 two-elements-transposition)) ( x)) ( λ q r → diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md index 053a1e296cb..5a6c6683f34 100644 --- a/src/foundation-core/fibers-of-maps.lagda.md +++ b/src/foundation-core/fibers-of-maps.lagda.md @@ -63,6 +63,24 @@ module _ ## Properties +### Fibers of compositions + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + (g : B → X) (h : A → B) {x : X} + where + + inclusion-fiber-comp : (t : fiber g x) → fiber h (pr1 t) → fiber (g ∘ h) x + inclusion-fiber-comp (b , q) (a , p) = (a , ap g p ∙ q) + + left-fiber-comp : fiber (g ∘ h) x → fiber g x + left-fiber-comp (a , r) = (h a , r) + + right-fiber-comp : (q : fiber (g ∘ h) x) → fiber h (pr1 (left-fiber-comp q)) + right-fiber-comp (a , r) = (a , refl) +``` + ### Characterization of the identity types of the fibers of a map #### The case of `fiber` @@ -376,15 +394,11 @@ module _ map-compute-fiber-comp : fiber (g ∘ h) x → Σ (fiber g x) (λ t → fiber h (pr1 t)) - pr1 (pr1 (map-compute-fiber-comp (a , p))) = h a - pr2 (pr1 (map-compute-fiber-comp (a , p))) = p - pr1 (pr2 (map-compute-fiber-comp (a , p))) = a - pr2 (pr2 (map-compute-fiber-comp (a , p))) = refl + map-compute-fiber-comp t = (left-fiber-comp g h t , right-fiber-comp g h t) map-inv-compute-fiber-comp : Σ (fiber g x) (λ t → fiber h (pr1 t)) → fiber (g ∘ h) x - pr1 (map-inv-compute-fiber-comp t) = pr1 (pr2 t) - pr2 (map-inv-compute-fiber-comp t) = ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t) + map-inv-compute-fiber-comp (t , s) = inclusion-fiber-comp g h t s is-section-map-inv-compute-fiber-comp : is-section map-compute-fiber-comp map-inv-compute-fiber-comp diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 931de9244e3..09a93b80408 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -308,6 +308,7 @@ open import foundation.maps-in-global-subuniverses public open import foundation.maps-in-subuniverses public open import foundation.maximum-truncation-levels public open import foundation.maybe public +open import foundation.mere-decidable-embeddings public open import foundation.mere-embeddings public open import foundation.mere-equality public open import foundation.mere-equivalences public @@ -338,6 +339,7 @@ open import foundation.negated-equality public open import foundation.negation public open import foundation.noncontractible-types public open import foundation.noninjective-maps public +open import foundation.nonsurjective-maps public open import foundation.null-homotopic-maps public open import foundation.operations-span-diagrams public open import foundation.operations-spans public diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md index a9f50ba0fe6..a156f9b0180 100644 --- a/src/foundation/0-connected-types.lagda.md +++ b/src/foundation/0-connected-types.lagda.md @@ -159,22 +159,24 @@ is-trunc-map-ev-is-connected k {A} {B} a H K = ### The dependent universal property of 0-connected types ```agda -equiv-dependent-universal-property-is-0-connected : - {l1 : Level} {A : UU l1} (a : A) → is-0-connected A → - ( {l : Level} (P : A → Prop l) → - ((x : A) → type-Prop (P x)) ≃ type-Prop (P a)) -equiv-dependent-universal-property-is-0-connected a H P = - ( equiv-universal-property-unit (type-Prop (P a))) ∘e - ( equiv-dependent-universal-property-surjection-is-surjective - ( point a) - ( is-surjective-point-is-0-connected a H) - ( P)) - -apply-dependent-universal-property-is-0-connected : - {l1 : Level} {A : UU l1} (a : A) → is-0-connected A → - {l : Level} (P : A → Prop l) → type-Prop (P a) → (x : A) → type-Prop (P x) -apply-dependent-universal-property-is-0-connected a H P = - map-inv-equiv (equiv-dependent-universal-property-is-0-connected a H P) +module _ + {l1 : Level} {A : UU l1} (a : A) (H : is-0-connected A) + {l : Level} (P : A → Prop l) + where + + equiv-dependent-universal-property-is-0-connected : + ((x : A) → type-Prop (P x)) ≃ type-Prop (P a) + equiv-dependent-universal-property-is-0-connected = + ( equiv-universal-property-unit (type-Prop (P a))) ∘e + ( equiv-dependent-universal-property-surjection-is-surjective + ( point a) + ( is-surjective-point-is-0-connected a H) + ( P)) + + apply-dependent-universal-property-is-0-connected : + type-Prop (P a) → (x : A) → type-Prop (P x) + apply-dependent-universal-property-is-0-connected = + map-inv-equiv equiv-dependent-universal-property-is-0-connected ``` ### A type `A` is 0-connected if and only if every fiber inclusion `B a → Σ A B` is surjective diff --git a/src/foundation/axiom-of-choice.lagda.md b/src/foundation/axiom-of-choice.lagda.md index ac46b18ce62..61c0164da46 100644 --- a/src/foundation/axiom-of-choice.lagda.md +++ b/src/foundation/axiom-of-choice.lagda.md @@ -102,7 +102,7 @@ is-set-projective-AC0 : is-set-projective-AC0 ac X A B f h = map-trunc-Prop ( ( map-Σ - ( λ g → ((map-surjection f) ∘ g) ＝ h) + ( λ g → map-surjection f ∘ g ＝ h) ( precomp h A) ( λ s H → htpy-postcomp X H h)) ∘ ( section-is-split-surjective (map-surjection f))) diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md index e5e25491a8b..abe291dd5bc 100644 --- a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md +++ b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md @@ -43,7 +43,7 @@ Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for ```agda module _ - {l1 l2 : Level} (lem : LEM (l1 ⊔ l2)) + {l1 l2 : Level} (lem : level-LEM (l1 ⊔ l2)) {A : UU l1} {B : UU l2} where abstract @@ -68,7 +68,7 @@ module _ ```agda module _ - {l1 l2 : Level} (lem : LEM (l1 ⊔ l2)) + {l1 l2 : Level} (lem : level-LEM (l1 ⊔ l2)) (A : Set l1) (B : Set l2) where abstract diff --git a/src/foundation/connected-maps.lagda.md b/src/foundation/connected-maps.lagda.md index 76139721187..3afb570f379 100644 --- a/src/foundation/connected-maps.lagda.md +++ b/src/foundation/connected-maps.lagda.md @@ -54,19 +54,19 @@ if its [fibers](foundation-core.fibers-of-maps.md) are ### Connected maps ```agda -is-connected-map-Prop : - {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} → (A → B) → Prop (l1 ⊔ l2) -is-connected-map-Prop k {B = B} f = - Π-Prop B (λ b → is-connected-Prop k (fiber f b)) - -is-connected-map : - {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) -is-connected-map k f = type-Prop (is-connected-map-Prop k f) - -is-prop-is-connected-map : - {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) → - is-prop (is-connected-map k f) -is-prop-is-connected-map k f = is-prop-type-Prop (is-connected-map-Prop k f) +module _ + {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) + where + + is-connected-map-Prop : Prop (l1 ⊔ l2) + is-connected-map-Prop = + Π-Prop B (λ b → is-connected-Prop k (fiber f b)) + + is-connected-map : UU (l1 ⊔ l2) + is-connected-map = type-Prop is-connected-map-Prop + + is-prop-is-connected-map : is-prop is-connected-map + is-prop-is-connected-map = is-prop-type-Prop is-connected-map-Prop ``` ### The type of connected maps between two types @@ -325,6 +325,34 @@ is-connected-map-left-factor k {g = g} {h} H GH z = ( is-connected-equiv' (compute-fiber-comp g h z) (GH z)) ``` +### Composition and cancellation in commuting triangles + +```agda +module _ + {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (g : B → X) (h : A → B) (K : f ~ g ∘ h) + where + + abstract + is-connected-map-left-map-triangle : + is-connected-map k h → + is-connected-map k g → + is-connected-map k f + is-connected-map-left-map-triangle H G = + is-connected-map-htpy k K + ( is-connected-map-comp k G H) + + abstract + is-connected-map-right-map-triangle : + is-connected-map k f → + is-connected-map k h → + is-connected-map k g + is-connected-map-right-map-triangle F H = + is-connected-map-left-factor k + ( H) + ( is-connected-map-htpy' k K F) +``` + ### The total map induced by a family of maps is `k`-connected if and only if all maps in the family are `k`-connected ```agda @@ -377,14 +405,26 @@ module _ is-equiv (precomp-Π f (λ b → type-Truncated-Type (P b))) module _ - {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f : A → B} + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B} + (H : is-connected-map k f) where - dependent-universal-property-is-connected-map : - is-connected-map k f → dependent-universal-property-connected-map k f - dependent-universal-property-is-connected-map H P = - is-equiv-precomp-Π-fiber-condition - ( λ b → is-equiv-diagonal-exponential-is-connected (P b) (H b)) + abstract + dependent-universal-property-is-connected-map : + dependent-universal-property-connected-map k f + dependent-universal-property-is-connected-map P = + is-equiv-precomp-Π-fiber-condition + ( λ b → is-equiv-diagonal-exponential-is-connected (P b) (H b)) + +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : connected-map k A B) + where + + dup-connected-map : + dependent-universal-property-connected-map k (map-connected-map f) + dup-connected-map = + dependent-universal-property-is-connected-map + ( is-connected-map-connected-map f) module _ {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : connected-map k A B) @@ -397,11 +437,54 @@ module _ pr1 (equiv-dependent-universal-property-is-connected-map P) = precomp-Π (map-connected-map f) (λ b → type-Truncated-Type (P b)) pr2 (equiv-dependent-universal-property-is-connected-map P) = - dependent-universal-property-is-connected-map k + dependent-universal-property-is-connected-map ( is-connected-map-connected-map f) ( P) ``` +### The induction principle for connected maps + +```agda +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B} + (H : is-connected-map k f) + where + + ind-is-connected-map : + {l3 : Level} (P : B → Truncated-Type l3 k) → + ((a : A) → type-Truncated-Type (P (f a))) → + (b : B) → type-Truncated-Type (P b) + ind-is-connected-map P = + map-inv-is-equiv (dependent-universal-property-is-connected-map H P) + + compute-ind-is-connected-map : + {l3 : Level} (P : B → Truncated-Type l3 k) → + (g : (a : A) → type-Truncated-Type (P (f a))) → + (x : A) → ind-is-connected-map P g (f x) ＝ g x + compute-ind-is-connected-map P f = + htpy-eq + ( is-section-map-inv-is-equiv + ( dependent-universal-property-is-connected-map H P) + ( f)) + +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : connected-map k A B) + where + + ind-connected-map : + {l3 : Level} (P : B → Truncated-Type l3 k) → + ((a : A) → type-Truncated-Type (P (map-connected-map f a))) → + (b : B) → type-Truncated-Type (P b) + ind-connected-map = ind-is-connected-map (is-connected-map-connected-map f) + + compute-ind-connected-map : + {l3 : Level} (P : B → Truncated-Type l3 k) → + (g : (a : A) → type-Truncated-Type (P (map-connected-map f a))) → + (x : A) → ind-connected-map P g (map-connected-map f x) ＝ g x + compute-ind-connected-map = + compute-ind-is-connected-map (is-connected-map-connected-map f) +``` + ### A map that satisfies the dependent universal property for connected maps is a connected map **Proof:** Consider a map `f : A → B` such that the precomposition function @@ -510,7 +593,7 @@ abstract ( precomp-Π f (λ b → type-Truncated-Type (P b))) is-trunc-map-precomp-Π-is-connected-map k neg-two-𝕋 H P = is-contr-map-is-equiv - ( dependent-universal-property-is-connected-map k H + ( dependent-universal-property-is-connected-map H ( λ b → pair ( type-Truncated-Type (P b)) diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md index 70856d62e23..631d14a8f48 100644 --- a/src/foundation/decidable-embeddings.lagda.md +++ b/src/foundation/decidable-embeddings.lagda.md @@ -219,8 +219,8 @@ is-decidable-emb-id : {l : Level} {A : UU l} → is-decidable-emb (id {A = A}) is-decidable-emb-id = (is-emb-id , is-decidable-map-id) -decidable-emb-id : {l : Level} {A : UU l} → A ↪ᵈ A -decidable-emb-id = (id , is-decidable-emb-id) +id-decidable-emb : {l : Level} {A : UU l} → A ↪ᵈ A +id-decidable-emb = (id , is-decidable-emb-id) is-decidable-prop-map-id : {l : Level} {A : UU l} → is-decidable-prop-map (id {A = A}) diff --git a/src/foundation/diaconescus-theorem.lagda.md b/src/foundation/diaconescus-theorem.lagda.md index adcacce8ccd..f0141f93666 100644 --- a/src/foundation/diaconescus-theorem.lagda.md +++ b/src/foundation/diaconescus-theorem.lagda.md @@ -80,7 +80,7 @@ instance-theorem-Diaconescu P ac-P = ( ac-P is-surjective-map-surjection-bool-suspension) theorem-Diaconescu : - {l : Level} → level-AC0 l l → LEM l + {l : Level} → level-AC0 l l → level-LEM l theorem-Diaconescu ac P = instance-theorem-Diaconescu P ( ac (suspension-set-Prop P) (fiber map-surjection-bool-suspension)) diff --git a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md index bec1d7a0cf4..1e4127dda22 100644 --- a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md +++ b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md @@ -95,7 +95,7 @@ is-epimorphism-is-truncation-equivalence-Truncated-Type : is-truncation-equivalence k f → is-epimorphism-Truncated-Type k f is-epimorphism-is-truncation-equivalence-Truncated-Type k f H X = - is-emb-is-equiv (is-equiv-precomp-is-truncation-equivalence k f H X) + is-emb-is-equiv (is-equiv-precomp-is-truncation-equivalence H X) ``` ### A map is a `k`-epimorphism if and only if its `k`-truncation is a `k`-epimorphism @@ -283,8 +283,7 @@ module _ is-epimorphism-Truncated-Type k f → is-truncation-equivalence k (codiagonal-map f) is-truncation-equivalence-codiagonal-map-is-epimorphism-Truncated-Type e = - is-truncation-equivalence-is-equiv-precomp k - ( codiagonal-map f) + is-truncation-equivalence-is-equiv-precomp ( λ l X → is-equiv-right-factor ( ( horizontal-map-cocone f f) ∘ @@ -330,7 +329,7 @@ module _ ( is-equiv-comp ( map-equiv (equiv-up-pushout f f (type-Truncated-Type X))) ( precomp (codiagonal-map f) (type-Truncated-Type X)) - ( is-equiv-precomp-is-truncation-equivalence k (codiagonal-map f) e X) + (is-equiv-precomp-is-truncation-equivalence e X) ( is-equiv-map-equiv (equiv-up-pushout f f (type-Truncated-Type X)))) is-epimorphism-is-truncation-equivalence-codiagonal-map-Truncated-Type : diff --git a/src/foundation/functoriality-truncation.lagda.md b/src/foundation/functoriality-truncation.lagda.md index 3708abf21b5..f3df0ea2027 100644 --- a/src/foundation/functoriality-truncation.lagda.md +++ b/src/foundation/functoriality-truncation.lagda.md @@ -9,6 +9,7 @@ module foundation.functoriality-truncation where ```agda open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types +open import foundation.evaluation-functions open import foundation.function-extensionality open import foundation.truncations open import foundation.universe-levels @@ -19,6 +20,7 @@ open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies +open import foundation-core.identity-types open import foundation-core.retractions open import foundation-core.retracts-of-types open import foundation-core.sections @@ -180,3 +182,53 @@ module _ ( inclusion-retract R) ( retraction-retract R) ``` + +### The truncation of the evaluation map + +```agda +module _ + {l1 l2 : Level} (k : 𝕋) + where + + map-trunc-ev : + {X : UU l1} {Y : X → UU l2} → + (x : X) → type-trunc k ((x : X) → Y x) → type-trunc k (Y x) + map-trunc-ev x = map-trunc k (ev x) + + compute-map-trunc-ev : + {X : UU l1} {Y : X → UU l2} → + (x : X) (f : (x : X) → Y x) → + map-trunc-ev x (unit-trunc f) ＝ unit-trunc (f x) + compute-map-trunc-ev x f = coherence-square-map-trunc k (ev x) f +``` + +### Distributivity of truncations over dependent products + +```agda +module _ + {l1 l2 : Level} (k : 𝕋) + where + + map-distributive-trunc-Π : + {X : UU l1} (Y : X → UU l2) → + type-trunc k ((x : X) → Y x) → (x : X) → type-trunc k (Y x) + map-distributive-trunc-Π Y f x = map-trunc-ev k x f + + compute-distributive-trunc-Π : + {X : UU l1} {Y : X → UU l2} → + (f : (x : X) → Y x) (x : X) → + map-distributive-trunc-Π Y (unit-trunc f) x ＝ unit-trunc (f x) + compute-distributive-trunc-Π f x = compute-map-trunc-ev k x f + + map-distributive-trunc-function-type : + (X : UU l1) (Y : UU l2) → type-trunc k (X → Y) → X → type-trunc k Y + map-distributive-trunc-function-type X Y = + map-distributive-trunc-Π (λ _ → Y) + + compute-distributive-trunc-function-type : + {X : UU l1} {Y : UU l2} → + (f : X → Y) (x : X) → + map-distributive-trunc-function-type X Y (unit-trunc f) x ＝ + unit-trunc (f x) + compute-distributive-trunc-function-type = compute-distributive-trunc-Π +``` diff --git a/src/foundation/law-of-excluded-middle.lagda.md b/src/foundation/law-of-excluded-middle.lagda.md index a633ea32d6a..5c74fd8ce29 100644 --- a/src/foundation/law-of-excluded-middle.lagda.md +++ b/src/foundation/law-of-excluded-middle.lagda.md @@ -30,11 +30,14 @@ asserts that any [proposition](foundation-core.propositions.md) `P` is ## Definition ```agda -LEM : (l : Level) → UU (lsuc l) -LEM l = (P : Prop l) → is-decidable (type-Prop P) +level-LEM : (l : Level) → UU (lsuc l) +level-LEM l = (P : Prop l) → is-decidable (type-Prop P) -prop-LEM : (l : Level) → Prop (lsuc l) -prop-LEM l = Π-Prop (Prop l) (is-decidable-Prop) +LEM : UUω +LEM = {l : Level} → level-LEM l + +prop-level-LEM : (l : Level) → Prop (lsuc l) +prop-level-LEM l = Π-Prop (Prop l) (is-decidable-Prop) ``` ## Properties @@ -43,7 +46,7 @@ prop-LEM l = Π-Prop (Prop l) (is-decidable-Prop) ```agda decidable-prop-Prop : - {l : Level} → LEM l → Prop l → Decidable-Prop l + {l : Level} → level-LEM l → Prop l → Decidable-Prop l pr1 (decidable-prop-Prop lem P) = type-Prop P pr1 (pr2 (decidable-prop-Prop lem P)) = is-prop-type-Prop P pr2 (pr2 (decidable-prop-Prop lem P)) = lem P diff --git a/src/foundation/mere-decidable-embeddings.lagda.md b/src/foundation/mere-decidable-embeddings.lagda.md new file mode 100644 index 00000000000..7153fe862d8 --- /dev/null +++ b/src/foundation/mere-decidable-embeddings.lagda.md @@ -0,0 +1,75 @@ +# Mere decidable embeddings + +```agda +module foundation.mere-decidable-embeddings where +``` + +
Imports + +```agda +open import foundation.cantor-schroder-bernstein-decidable-embeddings +open import foundation.decidable-embeddings +open import foundation.functoriality-propositional-truncation +open import foundation.mere-equivalences +open import foundation.propositional-truncations +open import foundation.universe-levels +open import foundation.weak-limited-principle-of-omniscience + +open import foundation-core.propositions + +open import order-theory.large-preorders +``` + +
+ +## Idea + +A type `A` {{#concept "merely decidably embeds" Agda=mere-decidable-emb}} into a +type `B` if there [merely exists](foundation.propositional-truncations.md) a +[decidable embedding](foundation.decidable-embeddings.md) of `A` into `B`. + +## Definition + +```agda +mere-decidable-emb-Prop : {l1 l2 : Level} → UU l1 → UU l2 → Prop (l1 ⊔ l2) +mere-decidable-emb-Prop X Y = trunc-Prop (X ↪ᵈ Y) + +mere-decidable-emb : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +mere-decidable-emb X Y = type-Prop (mere-decidable-emb-Prop X Y) + +is-prop-mere-decidable-emb : + {l1 l2 : Level} (X : UU l1) (Y : UU l2) → is-prop (mere-decidable-emb X Y) +is-prop-mere-decidable-emb X Y = is-prop-type-Prop (mere-decidable-emb-Prop X Y) +``` + +## Properties + +### Types equipped with mere decidable embeddings form a preordering + +```agda +refl-mere-decidable-emb : {l1 : Level} (X : UU l1) → mere-decidable-emb X X +refl-mere-decidable-emb X = unit-trunc-Prop id-decidable-emb + +transitive-mere-decidable-emb : + {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3} → + mere-decidable-emb Y Z → mere-decidable-emb X Y → mere-decidable-emb X Z +transitive-mere-decidable-emb = map-binary-trunc-Prop comp-decidable-emb + +mere-decidable-emb-Large-Preorder : Large-Preorder lsuc (_⊔_) +mere-decidable-emb-Large-Preorder = + λ where + .type-Large-Preorder l → UU l + .leq-prop-Large-Preorder → mere-decidable-emb-Prop + .refl-leq-Large-Preorder → refl-mere-decidable-emb + .transitive-leq-Large-Preorder X Y Z → transitive-mere-decidable-emb +``` + +### Assuming WLPO, then types equipped with mere decidable embeddings form a partial ordering + +```agda +antisymmetric-mere-decidable-emb : + {l1 l2 : Level} {X : UU l1} {Y : UU l2} → level-WLPO (l1 ⊔ l2) → + mere-decidable-emb X Y → mere-decidable-emb Y X → mere-equiv X Y +antisymmetric-mere-decidable-emb wlpo = + map-binary-trunc-Prop (Cantor-Schröder-Bernstein-WLPO wlpo) +``` diff --git a/src/foundation/mere-embeddings.lagda.md b/src/foundation/mere-embeddings.lagda.md index 4fbccc13d40..2cb411aae49 100644 --- a/src/foundation/mere-embeddings.lagda.md +++ b/src/foundation/mere-embeddings.lagda.md @@ -8,9 +8,13 @@ module foundation.mere-embeddings where ```agda open import foundation.cantor-schroder-bernstein-escardo +open import foundation.dependent-pair-types open import foundation.embeddings +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-propositional-truncation open import foundation.law-of-excluded-middle open import foundation.mere-equivalences +open import foundation.projective-types open import foundation.propositional-truncations open import foundation.universe-levels @@ -21,6 +25,12 @@ open import order-theory.large-preorders +## Idea + +A type `A` {{#concept "merely embeds" Agda=mere-emb}} into a type `B` if there +[merely exists](foundation.propositional-truncations.md) an +[embedding](foundation-core.embeddings.md) of `A` into `B`. + ## Definition ```agda @@ -46,20 +56,15 @@ refl-mere-emb X = unit-trunc-Prop id-emb transitive-mere-emb : {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3} → mere-emb Y Z → mere-emb X Y → mere-emb X Z -transitive-mere-emb g f = - apply-universal-property-trunc-Prop g - ( mere-emb-Prop _ _) - ( λ g' → - apply-universal-property-trunc-Prop f - ( mere-emb-Prop _ _) - ( λ f' → unit-trunc-Prop (comp-emb g' f'))) +transitive-mere-emb = map-binary-trunc-Prop comp-emb mere-emb-Large-Preorder : Large-Preorder lsuc (_⊔_) -type-Large-Preorder mere-emb-Large-Preorder l = UU l -leq-prop-Large-Preorder mere-emb-Large-Preorder = mere-emb-Prop -refl-leq-Large-Preorder mere-emb-Large-Preorder = refl-mere-emb -transitive-leq-Large-Preorder mere-emb-Large-Preorder X Y Z = - transitive-mere-emb +mere-emb-Large-Preorder = + λ where + .type-Large-Preorder l → UU l + .leq-prop-Large-Preorder → mere-emb-Prop + .refl-leq-Large-Preorder → refl-mere-emb + .transitive-leq-Large-Preorder X Y Z → transitive-mere-emb ``` ### Assuming excluded middle, if there are mere embeddings between `A` and `B` in both directions, then there is a mere equivalence between them @@ -67,12 +72,35 @@ transitive-leq-Large-Preorder mere-emb-Large-Preorder X Y Z = ```agda antisymmetric-mere-emb : {l1 l2 : Level} {X : UU l1} {Y : UU l2} → - LEM (l1 ⊔ l2) → mere-emb X Y → mere-emb Y X → mere-equiv X Y -antisymmetric-mere-emb lem f g = - apply-universal-property-trunc-Prop f - ( mere-equiv-Prop _ _) - ( λ f' → - apply-universal-property-trunc-Prop g - ( mere-equiv-Prop _ _) - ( λ g' → unit-trunc-Prop (Cantor-Schröder-Bernstein-Escardó lem f' g'))) + level-LEM (l1 ⊔ l2) → mere-emb X Y → mere-emb Y X → mere-equiv X Y +antisymmetric-mere-emb lem = + map-binary-trunc-Prop (Cantor-Schröder-Bernstein-Escardó lem) +``` + +### Dependent sums over projective types preserve mere embeddings + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : X → UU l2} {Z : X → UU l3} + where + + mere-emb-tot : + is-projective-Level' (l2 ⊔ l3) X → + ((x : X) → mere-emb (Y x) (Z x)) → + mere-emb (Σ X Y) (Σ X Z) + mere-emb-tot H e = map-trunc-Prop emb-tot (H _ e) +``` + +### Dependent products over projective types preserve mere embeddings + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : X → UU l2} {Z : X → UU l3} + where + + mere-emb-Π : + is-projective-Level' (l2 ⊔ l3) X → + ((x : X) → mere-emb (Y x) (Z x)) → + mere-emb ((x : X) → Y x) ((x : X) → Z x) + mere-emb-Π H e = map-trunc-Prop emb-Π (H _ e) ``` diff --git a/src/foundation/nonsurjective-maps.lagda.md b/src/foundation/nonsurjective-maps.lagda.md new file mode 100644 index 00000000000..66c93e20a2a --- /dev/null +++ b/src/foundation/nonsurjective-maps.lagda.md @@ -0,0 +1,221 @@ +# Nonsurjective maps + +```agda +module foundation.nonsurjective-maps where +``` + +
Imports + +```agda +open import foundation.coproduct-types +open import foundation.decidable-maps +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.double-negation +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.functoriality-coproduct-types +open import foundation.functoriality-dependent-pair-types +open import foundation.functoriality-propositional-truncation +open import foundation.fundamental-theorem-of-identity-types +open import foundation.injective-maps +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.split-surjective-maps +open import foundation.structure-identity-principle +open import foundation.surjective-maps +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.contractible-maps +open import foundation-core.fibers-of-maps +open import foundation-core.function-types +open import foundation-core.functoriality-dependent-function-types +open import foundation-core.propositions + +open import logic.propositionally-decidable-maps +``` + +
+ +## Idea + +A map `f : A → B` is {{#concept "nonsurjective"}} if there +[exists](foundation.existential-quantification.md) a +[fiber](foundation-core.fibers-of-maps.md) that is [not](foundation.negation.md) +inhabited. + +## Definitions + +### The nonimage of a map + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + nonim : UU (l1 ⊔ l2) + nonim = Σ B (λ y → ¬ fiber f y) +``` + +### Nonsurjectivity of a map + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + is-nonsurjective : UU (l1 ⊔ l2) + is-nonsurjective = ║ nonim f ║₋₁ + + is-prop-is-nonsurjective : is-prop is-nonsurjective + is-prop-is-nonsurjective = is-prop-exists-structure B (λ y → ¬ fiber f y) + + is-nonsurjective-Prop : Prop (l1 ⊔ l2) + is-nonsurjective-Prop = exists-structure-Prop B (λ y → ¬ fiber f y) +``` + +### Nonsurjective maps between types + +```agda +nonsurjective-map : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +nonsurjective-map A B = Σ (A → B) is-nonsurjective + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : nonsurjective-map A B) + where + + map-nonsurjective-map : A → B + map-nonsurjective-map = pr1 f + + is-nonsurjective-map-nonsurjective-map : + is-nonsurjective map-nonsurjective-map + is-nonsurjective-map-nonsurjective-map = pr2 f +``` + +## Properties + +### Nonsurjective maps are not surjective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + is-not-surjective-is-nonsurjective' : ¬¬ nonim f → ¬ is-surjective f + is-not-surjective-is-nonsurjective' F H = + F (λ (x , np) → rec-trunc-Prop empty-Prop np (H x)) + + is-not-surjective-is-nonsurjective : is-nonsurjective f → ¬ is-surjective f + is-not-surjective-is-nonsurjective F = + is-not-surjective-is-nonsurjective' + ( intro-double-negation-type-trunc-Prop F) +``` + +### If `g ∘ f` is nonsurjective and `g` is surjective then `f` is nonsurjective + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : A → B} {g : B → C} + where + + is-nonsurjective-right-nonim-comp-is-surjective-left : + is-surjective g → nonim (g ∘ f) → is-nonsurjective f + is-nonsurjective-right-nonim-comp-is-surjective-left G (c , np) = + map-trunc-Prop + ( λ (y , q) → (y , map-neg (inclusion-fiber-comp g f (y , q)) np)) + ( G c) + + is-nonsurjective-right-is-surjective-left : + is-surjective g → is-nonsurjective (g ∘ f) → is-nonsurjective f + is-nonsurjective-right-is-surjective-left G = + rec-trunc-Prop + ( is-nonsurjective-Prop f) + ( is-nonsurjective-right-nonim-comp-is-surjective-left G) +``` + +### If `g ∘ f` is nonsurjective and `g` is decidable then `g` or `f` is nonsurjective + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : A → B} {g : B → C} + where + + decide-nonim-comp : + is-decidable-map g → + nonim (g ∘ f) → nonim f + nonim g + decide-nonim-comp H (c , np) = + map-coproduct + ( λ (y , q) → y , map-neg (inclusion-fiber-comp g f (y , q)) np) + ( c ,_) + ( H c) + + decide-is-nonsurjective-nonim-comp' : + is-decidable-map g → + nonim (g ∘ f) → is-nonsurjective f + is-nonsurjective g + decide-is-nonsurjective-nonim-comp' H (c , np) = + map-coproduct + ( λ (y , q) → + unit-trunc-Prop (y , map-neg (inclusion-fiber-comp g f (y , q)) np)) + (λ p → unit-trunc-Prop (c , p)) + ( H c) + + is-nonsurjective-is-nonsurjective-comp' : + is-decidable-map g → + is-nonsurjective (g ∘ f) → + disjunction-type (is-nonsurjective f) (is-nonsurjective g) + is-nonsurjective-is-nonsurjective-comp' H = + map-trunc-Prop (decide-is-nonsurjective-nonim-comp' H) +``` + +In fact, it suffices that `g` is propositionally decidable. + +```agda + decide-is-nonsurjective-nonim-comp : + is-inhabited-or-empty-map g → + nonim (g ∘ f) → is-nonsurjective f + is-nonsurjective g + decide-is-nonsurjective-nonim-comp H (c , np) = + map-coproduct + ( map-trunc-Prop + ( λ (y , q) → y , map-neg (inclusion-fiber-comp g f (y , q)) np)) + ( λ p → unit-trunc-Prop (c , p)) + ( H c) + + is-nonsurjective-is-nonsurjective-comp : + is-inhabited-or-empty-map g → + is-nonsurjective (g ∘ f) → + disjunction-type (is-nonsurjective f) (is-nonsurjective g) + is-nonsurjective-is-nonsurjective-comp H = + map-trunc-Prop (decide-is-nonsurjective-nonim-comp H) +``` + +### If `g` is nonsurjective then so is `g ∘ f` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : A → B} {g : B → C} + where + + nonim-comp : nonim g → nonim (g ∘ f) + nonim-comp (c , np) = (c , map-neg (left-fiber-comp g f) np) + + is-nonsurjective-comp : is-nonsurjective g → is-nonsurjective (g ∘ f) + is-nonsurjective-comp = map-trunc-Prop nonim-comp +``` + +### If `g` is injective and `f` is nonsurjective then so is `g ∘ f` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : A → B} {g : B → C} + where + + nonim-comp-is-injective-left : is-injective g → nonim f → nonim (g ∘ f) + nonim-comp-is-injective-left G (c , np) = + ( g c , map-neg (tot (λ _ → G)) np) + + is-nonsurjective-comp-is-injective-left : + is-injective g → is-nonsurjective f → is-nonsurjective (g ∘ f) + is-nonsurjective-comp-is-injective-left G = + map-trunc-Prop (nonim-comp-is-injective-left G) +``` diff --git a/src/foundation/projective-types.lagda.md b/src/foundation/projective-types.lagda.md index 7e0578ef970..5a2fd4906d2 100644 --- a/src/foundation/projective-types.lagda.md +++ b/src/foundation/projective-types.lagda.md @@ -10,12 +10,14 @@ module foundation.projective-types where open import elementary-number-theory.natural-numbers open import foundation.connected-maps +open import foundation.dependent-pair-types open import foundation.inhabited-types open import foundation.postcomposition-functions open import foundation.surjective-maps open import foundation.truncation-levels open import foundation.universe-levels +open import foundation-core.propositions open import foundation-core.sets open import foundation-core.truncated-types ``` @@ -90,11 +92,27 @@ is-trunc-projective k X = {l2 l3 : Level} → is-trunc-projective-Level l2 l3 k ### Alternative statement of set-projectivity ```agda -is-projective-Level' : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) -is-projective-Level' l2 X = - (P : X → UU l2) → - ((x : X) → is-inhabited (P x)) → - is-inhabited ((x : X) → (P x)) +module _ + {l1 : Level} (l2 : Level) (X : UU l1) + where + + is-projective-Level' : UU (l1 ⊔ lsuc l2) + is-projective-Level' = + (P : X → UU l2) → + ((x : X) → is-inhabited (P x)) → + is-inhabited ((x : X) → (P x)) + + abstract + is-prop-is-projective-Level' : is-prop is-projective-Level' + is-prop-is-projective-Level' = + is-prop-Π + ( λ P → + is-prop-function-type + ( is-property-is-inhabited ((x : X) → P x))) + + is-projective-prop-Level' : Prop (l1 ⊔ lsuc l2) + is-projective-prop-Level' = + ( is-projective-Level' , is-prop-is-projective-Level') is-projective' : {l1 : Level} → UU l1 → UUω is-projective' X = {l2 : Level} → is-projective-Level' l2 X diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index f38f2062b38..185b30b2985 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -68,8 +68,7 @@ trunc-Prop = trunc neg-one-𝕋 **Notation.** The [box drawings double vertical](https://codepoints.net/U+2551) symbol `║` in the propositional truncation notation `║_║₋₁` can be inserted with -`agda-input` using the escape sequence `\--=` and selecting the second item in -the list. +`agda-input` using the escape sequence `\--=2`. ## Properties diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md index 154cc2d2b55..5326e8c1ffb 100644 --- a/src/foundation/set-truncations.lagda.md +++ b/src/foundation/set-truncations.lagda.md @@ -68,6 +68,9 @@ is-set-type-trunc-Set = is-trunc-type-trunc unit-trunc-Set : {l : Level} {A : UU l} → A → type-trunc-Set A unit-trunc-Set = unit-trunc +unit-trunc-Set' : {l : Level} (A : UU l) → A → type-trunc-Set A +unit-trunc-Set' A = unit-trunc-Set + is-set-truncation-trunc-Set : {l1 : Level} (A : UU l1) → is-set-truncation (trunc-Set A) unit-trunc-Set is-set-truncation-trunc-Set A = is-truncation-trunc @@ -78,8 +81,7 @@ is-set-truncation-trunc-Set A = is-truncation-trunc **Notation.** The [box drawings double vertical](https://codepoints.net/U+2551) symbol `║` in the set truncation notation `║_║₀` can be inserted with -`agda-input` using the escape sequence `\--=` and selecting the second item in -the list. +`agda-input` using the escape sequence `\--=2`. ## Properties @@ -122,6 +124,50 @@ module _ (x : type-trunc-Set A) → type-Set (B x) apply-dependent-universal-property-trunc-Set' = map-inv-equiv (equiv-dependent-universal-property-trunc-Set B) f + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : type-trunc-Set A → UU l2} + (C : (a : type-trunc-Set A) → type-trunc-Set (B a) → Set l3) + (f : + (x : A) (y : B (unit-trunc-Set x)) → + type-Set (C (unit-trunc-Set x) (unit-trunc-Set y))) + where + + apply-twice-dependent-universal-property-trunc-Set' : + (a : type-trunc-Set A) (b : type-trunc-Set (B a)) → type-Set (C a b) + apply-twice-dependent-universal-property-trunc-Set' = + apply-dependent-universal-property-trunc-Set' + ( λ x → Π-Set (trunc-Set (B x)) (C x)) + ( λ x → + apply-dependent-universal-property-trunc-Set' + ( C (unit-trunc-Set x)) + ( f x)) + +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : type-trunc-Set A → UU l2} + {C : (a : type-trunc-Set A) → type-trunc-Set (B a) → UU l3} + (D : + (a : type-trunc-Set A) (b : type-trunc-Set (B a)) → type-trunc-Set (C a b) → + Set l4) + (f : + (x : A) + (y : B (unit-trunc-Set x)) + (z : C (unit-trunc-Set x) (unit-trunc-Set y)) → + type-Set (D (unit-trunc-Set x) (unit-trunc-Set y) (unit-trunc-Set z))) + where + + apply-thrice-dependent-universal-property-trunc-Set' : + (a : type-trunc-Set A) + (b : type-trunc-Set (B a)) + (c : type-trunc-Set (C a b)) → + type-Set (D a b c) + apply-thrice-dependent-universal-property-trunc-Set' = + apply-twice-dependent-universal-property-trunc-Set' + ( λ x y → Π-Set (trunc-Set (C x y)) (D x y)) + ( λ x y → + apply-dependent-universal-property-trunc-Set' + ( D (unit-trunc-Set x) (unit-trunc-Set y)) + ( f x y)) ``` ### The universal property of set truncations @@ -421,7 +467,7 @@ module _ equiv-unit-trunc-set = equiv-unit-trunc A ``` -### Distributive of set truncation over coproduct +### Distributivity of set truncation over coproduct ```agda module _ diff --git a/src/foundation/standard-apartness-relations.lagda.md b/src/foundation/standard-apartness-relations.lagda.md index 73ece0d8621..1a6c9f5ca7c 100644 --- a/src/foundation/standard-apartness-relations.lagda.md +++ b/src/foundation/standard-apartness-relations.lagda.md @@ -37,7 +37,7 @@ is-standard-Apartness-Relation : {l1 l2 : Level} (l3 : Level) {A : UU l1} (R : Apartness-Relation l2 A) → UU (l1 ⊔ l2 ⊔ lsuc l3) is-standard-Apartness-Relation {l1} {l2} l3 {A} R = - LEM l3 → (x y : A) → (x ≠ y) ↔ apart-Apartness-Relation R x y + level-LEM l3 → (x y : A) → (x ≠ y) ↔ apart-Apartness-Relation R x y ``` ## Properties diff --git a/src/foundation/truncation-equivalences.lagda.md b/src/foundation/truncation-equivalences.lagda.md index da39546ed68..78b0c0162da 100644 --- a/src/foundation/truncation-equivalences.lagda.md +++ b/src/foundation/truncation-equivalences.lagda.md @@ -12,6 +12,8 @@ open import foundation.connected-maps open import foundation.connected-types open import foundation.contractible-types open import foundation.dependent-pair-types +open import foundation.equivalences-arrows +open import foundation.function-extensionality open import foundation.functoriality-truncation open import foundation.identity-types open import foundation.precomposition-functions-into-subuniverses @@ -60,7 +62,7 @@ truncation-equivalence : truncation-equivalence k A B = Σ (A → B) (is-truncation-equivalence k) module _ - {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : truncation-equivalence k A B) where @@ -85,39 +87,17 @@ module _ ### A map `f : A → B` is a `k`-equivalence if and only if `- ∘ f : (B → X) → (A → X)` is an equivalence for every `k`-truncated type `X` ```agda -is-equiv-precomp-is-truncation-equivalence : - {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) → - is-truncation-equivalence k f → - (X : Truncated-Type l3 k) → is-equiv (precomp f (type-Truncated-Type X)) -is-equiv-precomp-is-truncation-equivalence k f H X = - is-equiv-bottom-is-equiv-top-square - ( precomp unit-trunc (type-Truncated-Type X)) - ( precomp unit-trunc (type-Truncated-Type X)) - ( precomp (map-trunc k f) (type-Truncated-Type X)) - ( precomp f (type-Truncated-Type X)) - ( precomp-coherence-square-maps - ( unit-trunc) - ( f) - ( map-trunc k f) - ( unit-trunc) - ( inv-htpy (coherence-square-map-trunc k f)) - ( type-Truncated-Type X)) - ( is-truncation-trunc X) - ( is-truncation-trunc X) - ( is-equiv-precomp-is-equiv (map-trunc k f) H (type-Truncated-Type X)) - -is-truncation-equivalence-is-equiv-precomp : - {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) → - ( (l : Level) (X : Truncated-Type l k) → - is-equiv (precomp f (type-Truncated-Type X))) → - is-truncation-equivalence k f -is-truncation-equivalence-is-equiv-precomp k {A} {B} f H = - is-equiv-is-equiv-precomp-Truncated-Type k - ( trunc k A) - ( trunc k B) - ( map-trunc k f) - ( λ X → - is-equiv-top-is-equiv-bottom-square +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B} + where + + abstract + is-equiv-precomp-is-truncation-equivalence : + is-truncation-equivalence k f → + {l : Level} (X : Truncated-Type l k) → + is-equiv (precomp f (type-Truncated-Type X)) + is-equiv-precomp-is-truncation-equivalence H X = + is-equiv-bottom-is-equiv-top-square ( precomp unit-trunc (type-Truncated-Type X)) ( precomp unit-trunc (type-Truncated-Type X)) ( precomp (map-trunc k f) (type-Truncated-Type X)) @@ -131,7 +111,79 @@ is-truncation-equivalence-is-equiv-precomp k {A} {B} f H = ( type-Truncated-Type X)) ( is-truncation-trunc X) ( is-truncation-trunc X) - ( H _ X)) + ( is-equiv-precomp-is-equiv (map-trunc k f) H (type-Truncated-Type X)) + + abstract + is-truncation-equivalence-is-equiv-precomp : + ( (l : Level) (X : Truncated-Type l k) → + is-equiv (precomp f (type-Truncated-Type X))) → + is-truncation-equivalence k f + is-truncation-equivalence-is-equiv-precomp H = + is-equiv-is-equiv-precomp-Truncated-Type k + ( trunc k A) + ( trunc k B) + ( map-trunc k f) + ( λ X → + is-equiv-top-is-equiv-bottom-square + ( precomp unit-trunc (type-Truncated-Type X)) + ( precomp unit-trunc (type-Truncated-Type X)) + ( precomp (map-trunc k f) (type-Truncated-Type X)) + ( precomp f (type-Truncated-Type X)) + ( precomp-coherence-square-maps + ( unit-trunc) + ( f) + ( map-trunc k f) + ( unit-trunc) + ( inv-htpy (coherence-square-map-trunc k f)) + ( type-Truncated-Type X)) + ( is-truncation-trunc X) + ( is-truncation-trunc X) + ( H _ X)) +``` + +### The recursion principle of truncation equivalences + +```agda +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B} + (H : is-truncation-equivalence k f) + where + + rec-is-truncation-equivalence : + {l : Level} (X : Truncated-Type l k) → + (A → type-Truncated-Type X) → B → type-Truncated-Type X + rec-is-truncation-equivalence X = + map-inv-is-equiv (is-equiv-precomp-is-truncation-equivalence H X) + + compute-rec-is-truncation-equivalence : + {l : Level} (X : Truncated-Type l k) → + (g : A → type-Truncated-Type X) (x : A) → + rec-is-truncation-equivalence X g (f x) ＝ g x + compute-rec-is-truncation-equivalence X g = + htpy-eq + ( is-section-map-inv-is-equiv + ( is-equiv-precomp-is-truncation-equivalence H X) + ( g)) + +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} + (f : truncation-equivalence k A B) + where + + rec-truncation-equivalence : + {l : Level} (X : Truncated-Type l k) → + (A → type-Truncated-Type X) → B → type-Truncated-Type X + rec-truncation-equivalence = + rec-is-truncation-equivalence + ( is-truncation-equivalence-truncation-equivalence f) + + compute-rec-truncation-equivalence : + {l : Level} (X : Truncated-Type l k) → + (g : A → type-Truncated-Type X) (x : A) → + rec-truncation-equivalence X g (map-truncation-equivalence f x) ＝ g x + compute-rec-truncation-equivalence = + compute-rec-is-truncation-equivalence + ( is-truncation-equivalence-truncation-equivalence f) ``` ### Equivalences are `k`-equivalences for all `k` @@ -182,8 +234,21 @@ module _ is-truncation-equivalence-is-connected-map : is-connected-map k f → is-truncation-equivalence k f is-truncation-equivalence-is-connected-map c = - is-truncation-equivalence-is-equiv-precomp k f - ( λ l X → dependent-universal-property-is-connected-map k c (λ _ → X)) + is-truncation-equivalence-is-equiv-precomp + ( λ l X → dependent-universal-property-is-connected-map c (λ _ → X)) +``` + +### The unit maps of `k`-truncation are `k`-equivalences + +```agda +module _ + {l : Level} {k : 𝕋} {A : UU l} + where + + is-truncation-equivalence-unit-trunc : + is-truncation-equivalence k (unit-trunc {k = k} {A}) + is-truncation-equivalence-unit-trunc = + is-truncation-equivalence-is-equiv-precomp (λ l → is-truncation-trunc) ``` ### The `k`-equivalences are closed under composition @@ -209,16 +274,16 @@ module _ truncation-equivalence k A B → truncation-equivalence k A C pr1 (truncation-equivalence-comp g f) = - map-truncation-equivalence k g ∘ map-truncation-equivalence k f + map-truncation-equivalence g ∘ map-truncation-equivalence f pr2 (truncation-equivalence-comp g f) = is-truncation-equivalence-comp - ( map-truncation-equivalence k g) - ( map-truncation-equivalence k f) - ( is-truncation-equivalence-truncation-equivalence k f) - ( is-truncation-equivalence-truncation-equivalence k g) + ( map-truncation-equivalence g) + ( map-truncation-equivalence f) + ( is-truncation-equivalence-truncation-equivalence f) + ( is-truncation-equivalence-truncation-equivalence g) ``` -### The class of `k`-equivalences has the 3-for-2 property +### Cancellation property of truncation equivalences ```agda module _ @@ -250,6 +315,43 @@ module _ ( e)) ``` +### The class of `k`-equivalences has the 3-for-2 property + +```agda +module _ + {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (g : B → X) (h : A → B) (K : f ~ g ∘ h) + where + + abstract + is-truncation-equivalence-top-map-triangle : + is-truncation-equivalence k g → + is-truncation-equivalence k f → + is-truncation-equivalence k h + is-truncation-equivalence-top-map-triangle G F = + is-truncation-equivalence-right-factor g h + ( is-truncation-equivalence-htpy' k K F) + ( G) + + abstract + is-truncation-equivalence-left-map-triangle : + is-truncation-equivalence k h → + is-truncation-equivalence k g → + is-truncation-equivalence k f + is-truncation-equivalence-left-map-triangle H G = + is-truncation-equivalence-htpy k K + ( is-truncation-equivalence-comp g h H G) + + abstract + is-truncation-equivalence-right-map-triangle : + is-truncation-equivalence k f → + is-truncation-equivalence k h → + is-truncation-equivalence k g + is-truncation-equivalence-right-map-triangle F = + is-truncation-equivalence-left-factor g h + ( is-truncation-equivalence-htpy' k K F) +``` + ### Sections of `k`-equivalences are `k`-equivalences ```agda @@ -341,8 +443,7 @@ module _ is-truncation-equivalence-map-Σ-map-base-unit-trunc' : is-truncation-equivalence k map-Σ-map-base-unit-trunc' is-truncation-equivalence-map-Σ-map-base-unit-trunc' = - is-truncation-equivalence-is-equiv-precomp k - ( map-Σ-map-base-unit-trunc') + is-truncation-equivalence-is-equiv-precomp ( λ l (Y , TY) → is-equiv-equiv ( equiv-ev-pair) @@ -365,8 +466,7 @@ module _ is-truncation-equivalence-map-Σ-map-base-unit-trunc : is-truncation-equivalence k map-Σ-map-base-unit-trunc is-truncation-equivalence-map-Σ-map-base-unit-trunc = - is-truncation-equivalence-is-equiv-precomp k - ( map-Σ-map-base-unit-trunc) + is-truncation-equivalence-is-equiv-precomp ( λ l (Y , TY) → is-equiv-equiv {f = precomp (λ x → unit-trunc (pr1 x) , pr2 x) Y} @@ -451,7 +551,7 @@ module _ type-trunc k (fiber f b) ≃ type-trunc k (fiber (map-trunc (succ-𝕋 k) f) (unit-trunc b)) equiv-trunc-fiber-map-trunc-fiber = - equiv-trunc-truncation-equivalence k + equiv-trunc-truncation-equivalence ( truncation-equivalence-fiber-map-trunc-fiber) ``` @@ -478,15 +578,15 @@ module _ truncation-equivalence k A B → is-connected k B → is-connected k A is-connected-truncation-equivalence-is-connected f = is-connected-is-truncation-equivalence-is-connected - ( map-truncation-equivalence k f) - ( is-truncation-equivalence-truncation-equivalence k f) + ( map-truncation-equivalence f) + ( is-truncation-equivalence-truncation-equivalence f) is-connected-truncation-equivalence-is-connected' : truncation-equivalence k A B → is-connected k A → is-connected k B is-connected-truncation-equivalence-is-connected' f = is-connected-is-truncation-equivalence-is-connected' - ( map-truncation-equivalence k f) - ( is-truncation-equivalence-truncation-equivalence k f) + ( map-truncation-equivalence f) + ( is-truncation-equivalence-truncation-equivalence f) ``` ### Every `(k+1)`-equivalence is `k`-connected @@ -684,6 +784,22 @@ module _ ( is-connected-map-section-is-truncation-equivalence-succ k (s , h) e) ``` +### An `n`-truncation equivalence between `n`-truncated types is an equivalence + +```agda +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} {f : A → B} + where + + is-equiv-is-truncation-equivalence : + is-trunc k A → is-trunc k B → is-truncation-equivalence k f → is-equiv f + is-equiv-is-truncation-equivalence a b = + is-equiv-source-is-equiv-target-equiv-arrow f (map-trunc k f) + ( equiv-unit-trunc (A , a) , + equiv-unit-trunc (B , b) , + inv-htpy (coherence-square-map-trunc k f)) +``` + ## References - The notion of `k`-equivalence is a special case of the notion of diff --git a/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md b/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md index 27f1fb5de1f..f9a568c844e 100644 --- a/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md +++ b/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md @@ -42,9 +42,7 @@ is-weakly-constant-map-precomp-unit-trunc-Prop : {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : type-trunc-Prop A → B) → is-weakly-constant-map (g ∘ unit-trunc-Prop) is-weakly-constant-map-precomp-unit-trunc-Prop g x y = - ap - ( g) - ( eq-is-prop (is-prop-type-trunc-Prop)) + ap g (eq-is-prop is-prop-type-trunc-Prop) precomp-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) → diff --git a/src/literature/wikipedia-list-of-theorems.lagda.md b/src/literature/wikipedia-list-of-theorems.lagda.md index 0c7846e7b9a..d6ff543f4fd 100644 --- a/src/literature/wikipedia-list-of-theorems.lagda.md +++ b/src/literature/wikipedia-list-of-theorems.lagda.md @@ -140,6 +140,15 @@ open import order-theory.knaster-tarski-fixed-point-theorem using greatest-fixed-point-knaster-tarski-Suplattice) ``` +### König's theorem (set theory) {#Q1077462} + +**Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke) + +```agda +open import set-theory.konigs-theorem using + ( Königs-Theorem) +``` + ### Lawvere's fixed point theorem {#Q15809744} **Author:** [Egbert Rijke](https://egbertrijke.github.io) diff --git a/src/logic/dirk-gentlys-principle.lagda.md b/src/logic/dirk-gentlys-principle.lagda.md index a0a110c912c..64800258c8e 100644 --- a/src/logic/dirk-gentlys-principle.lagda.md +++ b/src/logic/dirk-gentlys-principle.lagda.md @@ -74,12 +74,12 @@ instance-Dirk-Gently-Principle-LEM' P Q (inr np) = inl-disjunction (ex-falso ∘ np) level-Dirk-Gently-Principle-LEM : - (l1 l2 : Level) → LEM l1 → level-Dirk-Gently-Principle l1 l2 + (l1 l2 : Level) → level-LEM l1 → level-Dirk-Gently-Principle l1 l2 level-Dirk-Gently-Principle-LEM l1 l2 lem P Q = instance-Dirk-Gently-Principle-LEM' P Q (lem P) level-Dirk-Gently-Principle-LEM' : - (l1 l2 : Level) → LEM l2 → level-Dirk-Gently-Principle l1 l2 + (l1 l2 : Level) → level-LEM l2 → level-Dirk-Gently-Principle l1 l2 level-Dirk-Gently-Principle-LEM' l1 l2 lem P Q = swap-disjunction (level-Dirk-Gently-Principle-LEM l2 l1 lem Q P) ``` diff --git a/src/order-theory/zorns-lemma.lagda.md b/src/order-theory/zorns-lemma.lagda.md index a2e403817ae..53dd5cad612 100644 --- a/src/order-theory/zorns-lemma.lagda.md +++ b/src/order-theory/zorns-lemma.lagda.md @@ -105,7 +105,7 @@ module _ ```agda module _ - {l1 l2 l3 : Level} (lem : LEM (l1 ⊔ l3)) + {l1 l2 l3 : Level} (lem : level-LEM (l1 ⊔ l3)) where inhabited-zorns-lemma-zorns-lemma : diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md index 6ce59643c86..089be79c696 100644 --- a/src/set-theory.lagda.md +++ b/src/set-theory.lagda.md @@ -38,7 +38,7 @@ set-level structure. In fact, assuming univalence, it is a proper In this module, we consider ideas historically related to the study of set theories both as foundations of set-level mathematics, but also as a study of hierarchies in mathematics. This includes ideas such as -[cardinality](set-theory.cardinalities.md) and +[cardinality](set-theory.cardinals.md) and [infinity](set-theory.infinite-sets.md), the [cumulative hierarchy](set-theory.cumulative-hierarchy.md) as a model of set theory, and [Russell's paradox](set-theory.russells-paradox.md). @@ -52,18 +52,29 @@ open import set-theory.baire-space public open import set-theory.bounded-increasing-binary-sequences public open import set-theory.cantor-space public open import set-theory.cantors-diagonal-argument public -open import set-theory.cardinalities public +open import set-theory.cardinality-projective-sets public +open import set-theory.cardinality-recursive-sets public +open import set-theory.cardinals public +open import set-theory.complemented-inequality-cardinals public open import set-theory.countable-sets public open import set-theory.cumulative-hierarchy public +open import set-theory.dependent-products-cardinals public +open import set-theory.dependent-sums-cardinals public +open import set-theory.equality-cardinals 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-cardinals public open import set-theory.inequality-increasing-binary-sequences public open import set-theory.infinite-sets public +open import set-theory.inhabited-cardinals public +open import set-theory.konigs-theorem public open import set-theory.positive-elements-increasing-binary-sequences public open import set-theory.russells-paradox public +open import set-theory.strict-indexed-inequality-cardinals public open import set-theory.strict-lower-bounds-increasing-binary-sequences public open import set-theory.uncountable-sets public +open import set-theory.zero-cardinal public ``` ## See also diff --git a/src/set-theory/cardinalities.lagda.md b/src/set-theory/cardinalities.lagda.md deleted file mode 100644 index 26956dc000c..00000000000 --- a/src/set-theory/cardinalities.lagda.md +++ /dev/null @@ -1,225 +0,0 @@ -# Cardinalities of sets - -```agda -module set-theory.cardinalities where -``` - -
Imports - -```agda -open import foundation.binary-relations -open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.function-extensionality -open import foundation.functoriality-propositional-truncation -open import foundation.identity-types -open import foundation.large-binary-relations -open import foundation.law-of-excluded-middle -open import foundation.mere-embeddings -open import foundation.mere-equivalences -open import foundation.propositional-extensionality -open import foundation.propositions -open import foundation.set-truncations -open import foundation.sets -open import foundation.universe-levels -``` - -
- -## Idea - -The -{{#concept "cardinality" Disambiguation="of a set" Agda=cardinality WD="cardinality" WDID=Q4049983}} -of a [set](foundation-core.sets.md) is its -[isomorphism](category-theory.isomorphisms-in-categories.md) class. We take -isomorphism classes of sets by [set truncating](foundation.set-truncations.md) -the universe of sets of any given -[universe level](foundation.universe-levels.md). Note that this definition takes -advantage of the [univalence axiom](foundation.univalence.md): By the univalence -axiom [isomorphic sets](foundation.isomorphisms-of-sets.md) are -[equal](foundation-core.identity-types.md), and will be mapped to the same -element in the set truncation of the universe of all sets. - -## Definition - -### Cardinalities - -```agda -cardinal-Set : (l : Level) → Set (lsuc l) -cardinal-Set l = trunc-Set (Set l) - -cardinal : (l : Level) → UU (lsuc l) -cardinal l = type-Set (cardinal-Set l) - -cardinality : {l : Level} → Set l → cardinal l -cardinality A = unit-trunc-Set A -``` - -### Inequality of cardinalities - -```agda -leq-cardinality-Prop' : - {l1 l2 : Level} → Set l1 → cardinal l2 → Prop (l1 ⊔ l2) -leq-cardinality-Prop' {l1} {l2} X = - map-universal-property-trunc-Set - ( Prop-Set (l1 ⊔ l2)) - ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y')) - -compute-leq-cardinality-Prop' : - {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - ( leq-cardinality-Prop' X (cardinality Y)) ＝ - ( mere-emb-Prop (type-Set X) (type-Set Y)) -compute-leq-cardinality-Prop' {l1} {l2} X = - triangle-universal-property-trunc-Set - ( Prop-Set (l1 ⊔ l2)) - ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y')) - -leq-cardinality-Prop : - {l1 l2 : Level} → cardinal l1 → cardinal l2 → Prop (l1 ⊔ l2) -leq-cardinality-Prop {l1} {l2} = - map-universal-property-trunc-Set - ( hom-set-Set (cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) - ( leq-cardinality-Prop') - -leq-cardinality : - {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2) -leq-cardinality X Y = type-Prop (leq-cardinality-Prop X Y) - -is-prop-leq-cardinality : - {l1 l2 : Level} {X : cardinal l1} {Y : cardinal l2} → - is-prop (leq-cardinality X Y) -is-prop-leq-cardinality {X = X} {Y = Y} = - is-prop-type-Prop (leq-cardinality-Prop X Y) - -compute-leq-cardinality : - {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - ( leq-cardinality (cardinality X) (cardinality Y)) ≃ - ( mere-emb (type-Set X) (type-Set Y)) -compute-leq-cardinality {l1} {l2} X Y = - equiv-eq-Prop - ( ( htpy-eq - ( triangle-universal-property-trunc-Set - ( hom-set-Set (cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) - ( leq-cardinality-Prop') X) (cardinality Y)) ∙ - ( compute-leq-cardinality-Prop' X Y)) - -unit-leq-cardinality : - {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - mere-emb (type-Set X) (type-Set Y) → - leq-cardinality (cardinality X) (cardinality Y) -unit-leq-cardinality X Y = map-inv-equiv (compute-leq-cardinality X Y) - -inv-unit-leq-cardinality : - {l1 l2 : Level} (X : Set l1) (Y : Set l2) → - leq-cardinality (cardinality X) (cardinality Y) → - mere-emb (type-Set X) (type-Set Y) -inv-unit-leq-cardinality X Y = pr1 (compute-leq-cardinality X Y) - -refl-leq-cardinality : is-reflexive-Large-Relation cardinal leq-cardinality -refl-leq-cardinality {l} = - apply-dependent-universal-property-trunc-Set' - ( λ X → set-Prop (leq-cardinality-Prop X X)) - ( λ A → unit-leq-cardinality A A (refl-mere-emb (type-Set A))) - -transitive-leq-cardinality : - {l1 l2 l3 : Level} - (X : cardinal l1) - (Y : cardinal l2) - (Z : cardinal l3) → - leq-cardinality X Y → - leq-cardinality Y Z → - leq-cardinality X Z -transitive-leq-cardinality X Y Z = - apply-dependent-universal-property-trunc-Set' - ( λ u → - set-Prop - ( function-Prop - ( leq-cardinality u Y) - ( function-Prop (leq-cardinality Y Z) - ( leq-cardinality-Prop u Z)))) - ( λ a → - apply-dependent-universal-property-trunc-Set' - ( λ v → - set-Prop - (function-Prop - (leq-cardinality (cardinality a) v) - (function-Prop (leq-cardinality v Z) - (leq-cardinality-Prop (cardinality a) Z)))) - ( λ b → - apply-dependent-universal-property-trunc-Set' - ( λ w → - set-Prop - (function-Prop - (leq-cardinality (cardinality a) (cardinality b)) - (function-Prop (leq-cardinality (cardinality b) w) - (leq-cardinality-Prop (cardinality a) w)))) - ( λ c aImports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.connected-maps +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-truncation +open import foundation.homotopies +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.mere-equivalences +open import foundation.postcomposition-functions +open import foundation.projective-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.retractions +open import foundation.retracts-of-types +open import foundation.set-truncations +open import foundation.sets +open import foundation.surjective-maps +open import foundation.truncated-types +open import foundation.truncation-equivalences +open import foundation.truncation-levels +open import foundation.truncations +open import foundation.universe-levels + +open import set-theory.cardinality-recursive-sets +open import set-theory.cardinals + +open import univalent-combinatorics.counting +open import univalent-combinatorics.distributivity-of-set-truncation-over-finite-products +open import univalent-combinatorics.finite-choice +open import univalent-combinatorics.finite-types +open import univalent-combinatorics.standard-finite-types +``` + + + +## Idea + +A [set](foundation-core.sets.md) $I$ is +{{#concept "cardinality-projective" Disambiguation="sets" Agda=Cardinality-Projective-Set}} +if it is [projective](foundation.projective-types.md) and the +[postcomposition map](foundation.postcomposition-functions.md) +$$\mathrm{cardinality} ∘ {-} : (I → \mathrm{Set}) → (I → \mathrm{Cardinal})$$ is +0-connected. + +## Definitions + +### The predicate of being cardinality-preprojective at a universe level + +```agda +module _ + {l1 : Level} (l2 : Level) (I : Set l1) + where + + is-cardinality-preprojective-set-Level : UU (l1 ⊔ lsuc l2) + is-cardinality-preprojective-set-Level = + is-connected-map zero-𝕋 (postcomp (type-Set I) (cardinality {l2})) + + is-prop-is-cardinality-preprojective-set-Level : + is-prop is-cardinality-preprojective-set-Level + is-prop-is-cardinality-preprojective-set-Level = + is-prop-is-connected-map zero-𝕋 (postcomp (type-Set I) cardinality) + + is-cardinality-preprojective-set-prop-Level : Prop (l1 ⊔ lsuc l2) + is-cardinality-preprojective-set-prop-Level = + ( is-cardinality-preprojective-set-Level , + is-prop-is-cardinality-preprojective-set-Level) +``` + +### The predicate of being cardinality-projective at a universe level + +```agda +module _ + {l1 : Level} (l2 : Level) (I : Set l1) + where + + is-cardinality-projective-set-Level : UU (l1 ⊔ lsuc l2) + is-cardinality-projective-set-Level = + is-connected-map zero-𝕋 (postcomp (type-Set I) (cardinality {l2})) × + is-projective-Level' l2 (type-Set I) + + is-prop-is-cardinality-projective-set-Level : + is-prop is-cardinality-projective-set-Level + is-prop-is-cardinality-projective-set-Level = + is-prop-product + ( is-prop-is-cardinality-preprojective-set-Level l2 I) + ( is-prop-is-projective-Level' l2 (type-Set I)) + + is-cardinality-projective-set-prop-Level : Prop (l1 ⊔ lsuc l2) + is-cardinality-projective-set-prop-Level = + ( is-cardinality-projective-set-Level , + is-prop-is-cardinality-projective-set-Level) +``` + +### The universe of cardinality-projective sets at a universe level + +```agda +Cardinality-Projective-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Cardinality-Projective-Set l1 l2 = + Σ (Set l1) (is-cardinality-projective-set-Level l2) + +module _ + {l1 l2 : Level} (I : Cardinality-Projective-Set l1 l2) + where + + set-Cardinality-Projective-Set : Set l1 + set-Cardinality-Projective-Set = pr1 I + + type-Cardinality-Projective-Set : UU l1 + type-Cardinality-Projective-Set = type-Set set-Cardinality-Projective-Set + + is-set-type-Cardinality-Projective-Set : + is-set type-Cardinality-Projective-Set + is-set-type-Cardinality-Projective-Set = + is-set-type-Set set-Cardinality-Projective-Set + + is-cardinality-projective-Cardinality-Projective-Set : + is-cardinality-projective-set-Level l2 set-Cardinality-Projective-Set + is-cardinality-projective-Cardinality-Projective-Set = pr2 I + + is-cardinality-preprojective-Cardinality-Projective-Set : + is-cardinality-preprojective-set-Level l2 set-Cardinality-Projective-Set + is-cardinality-preprojective-Cardinality-Projective-Set = + pr1 is-cardinality-projective-Cardinality-Projective-Set + + is-projective-Cardinality-Projective-Set : + is-projective-Level' l2 type-Cardinality-Projective-Set + is-projective-Cardinality-Projective-Set = + pr2 is-cardinality-projective-Cardinality-Projective-Set + + is-set-equivalence-postcomp-cardinality-type-Cardinality-Projective-Set : + is-truncation-equivalence zero-𝕋 + ( postcomp type-Cardinality-Projective-Set (cardinality {l2})) + is-set-equivalence-postcomp-cardinality-type-Cardinality-Projective-Set = + is-truncation-equivalence-is-connected-map + ( postcomp type-Cardinality-Projective-Set cardinality) + ( is-cardinality-preprojective-Cardinality-Projective-Set) + + ind-Cardinality-Projective-Set : + {l3 : Level} + (P : (type-Cardinality-Projective-Set → Cardinal l2) → Set l3) → + ( (Y : type-Cardinality-Projective-Set → Set l2) → + type-Set (P (cardinality ∘ Y))) → + (X : type-Cardinality-Projective-Set → Cardinal l2) → type-Set (P X) + ind-Cardinality-Projective-Set = + ind-is-connected-map is-cardinality-preprojective-Cardinality-Projective-Set + + compute-ind-Cardinality-Projective-Set : + {l3 : Level} + (P : (type-Cardinality-Projective-Set → Cardinal l2) → Set l3) + (T : + (Y : type-Cardinality-Projective-Set → Set l2) → + type-Set (P (cardinality ∘ Y))) + (Y : type-Cardinality-Projective-Set → Set l2) → + ind-Cardinality-Projective-Set P T (cardinality ∘ Y) ＝ T Y + compute-ind-Cardinality-Projective-Set = + compute-ind-is-connected-map + ( is-cardinality-preprojective-Cardinality-Projective-Set) + + apply-twice-ind-Cardinality-Projective-Set : + {l3 : Level} + (P : (X Y : type-Cardinality-Projective-Set → Cardinal l2) → Set l3) → + ( (X Y : type-Cardinality-Projective-Set → Set l2) → + type-Set (P (cardinality ∘ X) (cardinality ∘ Y))) → + (X Y : type-Cardinality-Projective-Set → Cardinal l2) → type-Set (P X Y) + apply-twice-ind-Cardinality-Projective-Set P h X = + ind-Cardinality-Projective-Set + ( P X) + ( λ Y → + ind-Cardinality-Projective-Set + ( λ X → P X (cardinality ∘ Y)) + ( λ X → h X Y) + ( X)) + + constr-Cardinality-Projective-Set : + {l : Level} → + ((type-Cardinality-Projective-Set → Set l2) → Cardinal l) → + (type-Cardinality-Projective-Set → Cardinal l2) → + Cardinal l + constr-Cardinality-Projective-Set {l} = + rec-is-truncation-equivalence + ( is-set-equivalence-postcomp-cardinality-type-Cardinality-Projective-Set) + ( Cardinal-Set l) + + compute-constr-Cardinality-Projective-Set : + {l : Level} → + (T : (type-Cardinality-Projective-Set → Set l2) → Cardinal l) + (Y : type-Cardinality-Projective-Set → Set l2) → + constr-Cardinality-Projective-Set T (cardinality ∘ Y) ＝ T Y + compute-constr-Cardinality-Projective-Set {l} = + compute-rec-is-truncation-equivalence + ( is-set-equivalence-postcomp-cardinality-type-Cardinality-Projective-Set) + ( Cardinal-Set l) +``` + +## Properties + +### Distributive property of cardinality-preprojective sets + +A set `I` is cardinality-preprojective if and only if the distributive map + +```text + ║I → Set║₀ → (I → Cardinal) +``` + +is an equivalence. + +**Proof.** We have the commuting triangle + +```text + (I → Set) + / \ + / \ + ∨ ∨ + ║I → Set║₀ -----> (I → Cardinal) +``` + +where the left vertical map is 0-connected hence by the cancellation/composition +property of 0-connected maps, `I` is cardinality-projective if and only if the +bottom horizontal map is. But the horizontal map is a map between sets, and so +is 0-connected if and only if it is an equivalence. ∎ + +```agda +module _ + {l1 l2 : Level} (I : Set l1) + where + + is-set-equivalence-map-distributive-trunc-set-is-set-equivalence-postcomp-cardinality-Set : + is-truncation-equivalence zero-𝕋 + ( postcomp (type-Set I) (cardinality {l2})) → + is-truncation-equivalence zero-𝕋 + ( map-distributive-trunc-function-type zero-𝕋 (type-Set I) (Set l2)) + is-set-equivalence-map-distributive-trunc-set-is-set-equivalence-postcomp-cardinality-Set + H = + is-truncation-equivalence-right-map-triangle + ( postcomp (type-Set I) cardinality) + ( map-distributive-trunc-function-type zero-𝕋 (type-Set I) (Set l2)) + ( unit-trunc-Set) + ( λ f → inv (eq-htpy (compute-distributive-trunc-function-type zero-𝕋 f))) + ( H) + ( is-truncation-equivalence-unit-trunc) + + is-equiv-map-distributive-trunc-set-is-set-equivalence-postcomp-cardinality-Set : + is-truncation-equivalence zero-𝕋 + ( postcomp (type-Set I) (cardinality {l2})) → + is-equiv (map-distributive-trunc-function-type zero-𝕋 (type-Set I) (Set l2)) + is-equiv-map-distributive-trunc-set-is-set-equivalence-postcomp-cardinality-Set + H = + is-equiv-is-truncation-equivalence + ( is-set-type-trunc-Set) + ( is-set-function-type is-set-Cardinal) + ( is-set-equivalence-map-distributive-trunc-set-is-set-equivalence-postcomp-cardinality-Set + ( H)) + + is-equiv-map-distributive-trunc-set-is-cardinality-preprojective-set : + is-cardinality-preprojective-set-Level l2 I → + is-equiv (map-distributive-trunc-function-type zero-𝕋 (type-Set I) (Set l2)) + is-equiv-map-distributive-trunc-set-is-cardinality-preprojective-set H = + is-equiv-map-distributive-trunc-set-is-set-equivalence-postcomp-cardinality-Set + ( is-truncation-equivalence-is-connected-map _ H) + + is-cardinality-preprojective-set-is-is-equiv-map-distributive-trunc-set : + is-equiv + ( map-distributive-trunc-function-type zero-𝕋 (type-Set I) (Set l2)) → + is-cardinality-preprojective-set-Level l2 I + is-cardinality-preprojective-set-is-is-equiv-map-distributive-trunc-set H = + is-connected-map-left-map-triangle + ( postcomp (type-Set I) cardinality) + ( map-distributive-trunc-function-type zero-𝕋 (type-Set I) (Set l2)) + ( unit-trunc-Set) + ( λ f → inv (eq-htpy (compute-distributive-trunc-function-type zero-𝕋 f))) + ( is-connected-map-unit-trunc zero-𝕋) + ( is-connected-map-is-equiv H) + +is-equiv-map-distributive-trunc-set-Cardinality-Projective-Set : + {l1 l2 : Level} (I : Cardinality-Projective-Set l1 l2) → + is-equiv + ( map-distributive-trunc-function-type zero-𝕋 + ( type-Cardinality-Projective-Set I) + ( Set l2)) +is-equiv-map-distributive-trunc-set-Cardinality-Projective-Set (I , (H , _)) = + is-equiv-map-distributive-trunc-set-is-cardinality-preprojective-set I H +``` + +### Cardinality-projective sets are cardinality-recursive + +We call the inverse map to the distributive law the "unit map" of the +cardinality-projective set, and this map gives an induction principle for +constructing cardinals over $I$. + +```agda +module _ + {l1 l2 : Level} (I : Cardinality-Projective-Set l1 l2) + (let I' = type-Cardinality-Projective-Set I) + where + + is-cardinality-recursive-Cardinality-Projective-Set : + is-cardinality-recursive-set-Level l2 (set-Cardinality-Projective-Set I) + is-cardinality-recursive-Cardinality-Projective-Set = + retraction-is-equiv + ( is-equiv-map-distributive-trunc-set-Cardinality-Projective-Set I) + + cardinality-recursive-set-Cardinality-Projective-Set : + Cardinality-Recursive-Set l1 l2 + cardinality-recursive-set-Cardinality-Projective-Set = + ( set-Cardinality-Projective-Set I , + is-cardinality-recursive-Cardinality-Projective-Set) + + unit-Cardinality-Projective-Set : + (I' → Cardinal l2) → ║ (I' → Set l2) ║₀ + unit-Cardinality-Projective-Set = + unit-Cardinality-Recursive-Set + ( cardinality-recursive-set-Cardinality-Projective-Set) + + is-retraction-unit-Cardinality-Projective-Set : + is-retraction + ( map-distributive-trunc-function-type zero-𝕋 I' (Set l2)) + ( unit-Cardinality-Projective-Set) + is-retraction-unit-Cardinality-Projective-Set = + is-retraction-unit-Cardinality-Recursive-Set + ( cardinality-recursive-set-Cardinality-Projective-Set) + + compute-unit-Cardinality-Projective-Set : + (K : I' → Set l2) → + unit-Cardinality-Projective-Set (cardinality ∘ K) ＝ unit-trunc-Set K + compute-unit-Cardinality-Projective-Set = + compute-unit-Cardinality-Recursive-Set + ( cardinality-recursive-set-Cardinality-Projective-Set) +``` + +### A set is cardinality-preprojective if the postcomposition map is a set-equivalence + +```agda +module _ + {l1 l2 : Level} (I : Set l1) + where + + is-cardinality-preprojective-set-is-set-equivalence-postcomp-cardinality-Set : + is-truncation-equivalence zero-𝕋 + ( postcomp (type-Set I) (cardinality {l2})) → + is-cardinality-preprojective-set-Level l2 I + is-cardinality-preprojective-set-is-set-equivalence-postcomp-cardinality-Set + H = + is-cardinality-preprojective-set-is-is-equiv-map-distributive-trunc-set I + ( is-equiv-map-distributive-trunc-set-is-set-equivalence-postcomp-cardinality-Set + ( I) + ( H)) +``` + +### The standard finite sets are cardinality-projective + +```agda +module _ + {l : Level} (n : ℕ) + where + + abstract + is-cardinality-preprojective-Fin : + is-cardinality-preprojective-set-Level l (Fin-Set n) + is-cardinality-preprojective-Fin = + is-connected-map-left-map-triangle + ( postcomp (Fin n) cardinality) + ( map-equiv-distributive-trunc-Π-Fin-Set n (λ _ → Set l)) + ( unit-trunc-Set) + ( inv-htpy (triangle-distributive-trunc-Π-Fin-Set n (λ _ → Set l))) + ( is-connected-map-unit-trunc zero-𝕋) + ( is-connected-map-is-equiv + ( is-equiv-map-equiv-distributive-trunc-Π-Fin-Set n (λ _ → Set l))) + + is-cardinality-projective-Fin : + is-cardinality-projective-set-Level l (Fin-Set n) + is-cardinality-projective-Fin = + ( is-cardinality-preprojective-Fin , (λ P → finite-choice-Fin n)) + + cardinality-projective-set-Fin : Cardinality-Projective-Set lzero l + cardinality-projective-set-Fin = (Fin-Set n , is-cardinality-projective-Fin) +``` + +### Sets equipped with counting are cardinality-projective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (c : count A) + where + + abstract + is-cardinality-preprojective-set-count : + is-cardinality-preprojective-set-Level l2 (set-type-count c) + is-cardinality-preprojective-set-count = + is-connected-map-left-map-triangle + ( postcomp A cardinality) + ( map-equiv-distributive-trunc-Π-count-Set c (λ _ → Set l2)) + ( unit-trunc-Set) + ( inv-htpy (triangle-distributive-trunc-Π-count-Set c (λ _ → Set l2))) + ( is-connected-map-unit-trunc zero-𝕋) + ( is-connected-map-is-equiv + ( is-equiv-map-equiv-distributive-trunc-Π-count-Set c (λ _ → Set l2))) + + is-cardinality-projective-set-count : + is-cardinality-projective-set-Level l2 (set-type-count c) + is-cardinality-projective-set-count = + ( is-cardinality-preprojective-set-count , (λ P → finite-choice-count c)) + + cardinality-projective-set-count : Cardinality-Projective-Set l1 l2 + cardinality-projective-set-count = + ( set-type-count c , is-cardinality-projective-set-count) +``` + +### Finite sets are cardinality-projective + +```agda +module _ + {l1 l2 : Level} (A : Finite-Type l1) + where + + abstract + is-cardinality-preprojective-set-Finite-Type : + is-cardinality-preprojective-set-Level l2 (set-Finite-Type A) + is-cardinality-preprojective-set-Finite-Type = + rec-trunc-Prop + ( is-cardinality-preprojective-set-prop-Level l2 (set-Finite-Type A)) + ( is-cardinality-preprojective-set-count) + ( is-finite-type-Finite-Type A) + + is-cardinality-projective-set-Finite-Type : + is-cardinality-projective-set-Level l2 (set-Finite-Type A) + is-cardinality-projective-set-Finite-Type = + ( is-cardinality-preprojective-set-Finite-Type , + ( λ P → finite-choice (is-finite-type-Finite-Type A))) + + cardinality-projective-set-Finite-Type : Cardinality-Projective-Set l1 l2 + cardinality-projective-set-Finite-Type = + ( set-Finite-Type A , is-cardinality-projective-set-Finite-Type) +``` + +## See also + +- In + [Distributivity of set truncation over finite products](univalent-combinatorics.distributivity-of-set-truncation-over-finite-products.md) + it is demonstrated that finite types are cardinality-projective. diff --git a/src/set-theory/cardinality-recursive-sets.lagda.md b/src/set-theory/cardinality-recursive-sets.lagda.md new file mode 100644 index 00000000000..78f7da51700 --- /dev/null +++ b/src/set-theory/cardinality-recursive-sets.lagda.md @@ -0,0 +1,156 @@ +# Cardinality-recursive sets + +```agda +module set-theory.cardinality-recursive-sets where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-truncation +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.mere-equivalences +open import foundation.retractions +open import foundation.retracts-of-types +open import foundation.set-truncations +open import foundation.sets +open import foundation.truncation-levels +open import foundation.truncations +open import foundation.universe-levels + +open import set-theory.cardinals +``` + +
+ +## Idea + +For every type $X$ there is a map +$$║X → \mathrm{Set}║₀ → (X → \mathrm{Cardinal}).$$ We call +[sets](foundation-core.sets.md) $X$ for which this map has a +[retraction](foundation.retractions.md) +{{#concept "cardinality-recursive" Disambiguation="sets" Agda=Cardinality-Recursive-Set}}. +Over such sets we may form +[dependent sum](set-theory.dependent-sums-cardinals.md) and +[dependent product](set-theory.dependent-products-cardinals.md) +[cardinals](set-theory.cardinals.md). + +Note that classically, the universe of sets is itself a set, and so trivially +$║X → \mathrm{Set}║₀ ≃ (X → ║\mathrm{Set}║₀)$. However, with univalence, the +universe of sets $\mathrm{Set}$ brandishes higher structure, and its set +truncation $║Set║₀$ presents cardinals. + +```text + (X → Set) + / \ + surj ∨ \ + ∨ ∨ + ║X → Set║₀ ╰-----> (X → Cardinality) + <<--- +``` + +**Terminology.** This is nonstandard terminology and may be subject to change. + +## Definition + +```agda +module _ + {l1 : Level} (l2 : Level) (X : Set l1) + where + + is-cardinality-recursive-set-Level : UU (l1 ⊔ lsuc l2) + is-cardinality-recursive-set-Level = + retraction + ( map-distributive-trunc-function-type zero-𝕋 (type-Set X) (Set l2)) +``` + +### The universe of cardinality-recursive sets at a universe level + +```agda +Cardinality-Recursive-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Cardinality-Recursive-Set l1 l2 = + Σ (Set l1) (is-cardinality-recursive-set-Level l2) + +module _ + {l1 l2 : Level} (X : Cardinality-Recursive-Set l1 l2) + where + + set-Cardinality-Recursive-Set : Set l1 + set-Cardinality-Recursive-Set = pr1 X + + type-Cardinality-Recursive-Set : UU l1 + type-Cardinality-Recursive-Set = type-Set set-Cardinality-Recursive-Set + + is-set-type-Cardinality-Recursive-Set : + is-set type-Cardinality-Recursive-Set + is-set-type-Cardinality-Recursive-Set = + is-set-type-Set set-Cardinality-Recursive-Set + + is-cardinality-recursive-Cardinality-Recursive-Set : + is-cardinality-recursive-set-Level l2 set-Cardinality-Recursive-Set + is-cardinality-recursive-Cardinality-Recursive-Set = pr2 X + + unit-Cardinality-Recursive-Set : + ( type-Cardinality-Recursive-Set → Cardinal l2) → + ║ (type-Cardinality-Recursive-Set → Set l2) ║₀ + unit-Cardinality-Recursive-Set = + map-retraction + ( map-distributive-trunc-function-type zero-𝕋 + ( type-Cardinality-Recursive-Set) + ( Set l2)) + ( is-cardinality-recursive-Cardinality-Recursive-Set) + + is-retraction-unit-Cardinality-Recursive-Set : + is-retraction + ( map-distributive-trunc-function-type zero-𝕋 + ( type-Cardinality-Recursive-Set) + ( Set l2)) + ( unit-Cardinality-Recursive-Set) + is-retraction-unit-Cardinality-Recursive-Set = + is-retraction-map-retraction + ( map-distributive-trunc-function-type zero-𝕋 + ( type-Cardinality-Recursive-Set) + ( Set l2)) + ( is-cardinality-recursive-Cardinality-Recursive-Set) + + retract-Cardinality-Recursive-Set : + ║ (type-Cardinality-Recursive-Set → Set l2) ║₀ retract-of + ( type-Cardinality-Recursive-Set → Cardinal l2) + retract-Cardinality-Recursive-Set = + ( ( map-distributive-trunc-function-type + ( zero-𝕋) + ( type-Cardinality-Recursive-Set) + ( Set l2)) , + ( is-cardinality-recursive-Cardinality-Recursive-Set)) + + compute-unit-Cardinality-Recursive-Set : + (K : type-Cardinality-Recursive-Set → Set l2) → + unit-Cardinality-Recursive-Set (cardinality ∘ K) ＝ unit-trunc-Set K + compute-unit-Cardinality-Recursive-Set K = + equational-reasoning + unit-Cardinality-Recursive-Set (cardinality ∘ K) + ＝ unit-Cardinality-Recursive-Set + ( map-distributive-trunc-function-type zero-𝕋 + ( type-Cardinality-Recursive-Set) + ( Set l2) + ( unit-trunc K)) + by + ap + ( unit-Cardinality-Recursive-Set) + ( inv (eq-htpy (compute-distributive-trunc-function-type zero-𝕋 K))) + ＝ unit-trunc K + by is-retraction-unit-Cardinality-Recursive-Set (unit-trunc K) +``` + +## See also + +- In + [Distributivity of set truncation over finite products](univalent-combinatorics.distributivity-of-set-truncation-over-finite-products.md) + it is demonstrated that finite types are cardinality-recursive. diff --git a/src/set-theory/cardinals.lagda.md b/src/set-theory/cardinals.lagda.md new file mode 100644 index 00000000000..7c930b915ef --- /dev/null +++ b/src/set-theory/cardinals.lagda.md @@ -0,0 +1,64 @@ +# Cardinals + +```agda +module set-theory.cardinals where +``` + +
Imports + +```agda +open import foundation.equivalences +open import foundation.functoriality-propositional-truncation +open import foundation.identity-types +open import foundation.mere-equivalences +open import foundation.set-truncations +open import foundation.sets +open import foundation.universe-levels +``` + +
+ +## Idea + +The +{{#concept "cardinality" Disambiguation="of a set" Agda=cardinality WD="cardinality" WDID=Q4049983}} +of a [set](foundation-core.sets.md) is its +[isomorphism](category-theory.isomorphisms-in-categories.md) class. We take +isomorphism classes of sets by [set truncating](foundation.set-truncations.md) +the universe of sets of any given +[universe level](foundation.universe-levels.md), and such an isomorphism class +is called a +{{#concept "cardinal" Disambiguation="of sets" WD="cardinal number" WDID=Q163875}}. + +Note that this definition takes advantage of the +[univalence axiom](foundation.univalence.md): By the univalence axiom +[isomorphic sets](foundation.isomorphisms-of-sets.md) are +[equal](foundation-core.identity-types.md), and will be mapped to the same +element in the set truncation of the universe of all sets. + +## Definition + +### Cardinals + +```agda +Cardinal-Set : (l : Level) → Set (lsuc l) +Cardinal-Set l = trunc-Set (Set l) + +Cardinal : (l : Level) → UU (lsuc l) +Cardinal l = type-Set (Cardinal-Set l) + +is-set-Cardinal : {l : Level} → is-set (Cardinal l) +is-set-Cardinal {l} = is-set-type-Set (Cardinal-Set l) +``` + +### The cardinality of a set + +```agda +cardinality : {l : Level} → Set l → Cardinal l +cardinality A = unit-trunc-Set A +``` + +## External links + +- [Cardinality](https://en.wikipedia.org/wiki/Cardinality) at Wikipedia +- [cardinal number](https://ncatlab.org/nlab/show/cardinal+number) at $n$Lab diff --git a/src/set-theory/complemented-inequality-cardinals.lagda.md b/src/set-theory/complemented-inequality-cardinals.lagda.md new file mode 100644 index 00000000000..0de213282c8 --- /dev/null +++ b/src/set-theory/complemented-inequality-cardinals.lagda.md @@ -0,0 +1,269 @@ +# Complemented inequality on cardinals + +```agda +module set-theory.complemented-inequality-cardinals where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.identity-types +open import foundation.large-binary-relations +open import foundation.mere-decidable-embeddings +open import foundation.propositional-extensionality +open import foundation.propositions +open import foundation.set-truncations +open import foundation.sets +open import foundation.univalence +open import foundation.universe-levels +open import foundation.weak-limited-principle-of-omniscience + +open import order-theory.large-posets +open import order-theory.large-preorders + +open import set-theory.cardinals +open import set-theory.equality-cardinals +``` + +
+ +## Idea + +We may say a [cardinal](set-theory.cardinals.md) `X` is +{{#concept "less than or equal to" Agda=leq-complemented-Cardinal}} a cardinal +`Y` if any [set](foundation-core.sets.md) in the isomorphism class represented +by `X` [embeds](foundation-core.embeddings.md) as a +[decidable subtype](foundation.decidable-subtypes.md) into any set in the +isomorphism class represented by `Y`. In other words, if there is a +[decidable embedding](foundation.decidable-embeddings.md) from the first to the +second. This defines the +{{#concept "complemented ordering" Disambiguation="on cardinalities of sets"}} +on cardinalities of sets. + +Under the assumption of the +[weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md), +this relation is antisymmetric and hence defines a +[partial order](order-theory.posets.md) on cardinals. + +## Definition + +### Complemented boundedness of the cardinality of a set + +```agda +module _ + {l1 l2 : Level} (X : Set l1) + where + + leq-complemented-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2) + leq-complemented-prop-Cardinal' = + map-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( λ Y' → mere-decidable-emb-Prop (type-Set X) (type-Set Y')) + + compute-leq-complemented-prop-Cardinal' : + (Y : Set l2) → + leq-complemented-prop-Cardinal' (cardinality Y) ＝ + mere-decidable-emb-Prop (type-Set X) (type-Set Y) + compute-leq-complemented-prop-Cardinal' = + triangle-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( λ Y' → mere-decidable-emb-Prop (type-Set X) (type-Set Y')) +``` + +### Complemented inequality of cardinals + +```agda +module _ + {l1 l2 : Level} + where + + leq-complemented-prop-Cardinal : + Cardinal l1 → Cardinal l2 → Prop (l1 ⊔ l2) + leq-complemented-prop-Cardinal = + map-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( leq-complemented-prop-Cardinal') + + leq-complemented-Cardinal : + Cardinal l1 → Cardinal l2 → UU (l1 ⊔ l2) + leq-complemented-Cardinal X Y = + type-Prop (leq-complemented-prop-Cardinal X Y) + + is-prop-leq-complemented-Cardinal : + {X : Cardinal l1} {Y : Cardinal l2} → + is-prop (leq-complemented-Cardinal X Y) + is-prop-leq-complemented-Cardinal {X} {Y} = + is-prop-type-Prop (leq-complemented-prop-Cardinal X Y) +``` + +### Complemented inequality of cardinalities + +```agda +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + leq-complemented-prop-cardinality : Prop (l1 ⊔ l2) + leq-complemented-prop-cardinality = + leq-complemented-prop-Cardinal (cardinality X) (cardinality Y) + + leq-complemented-cardinality : UU (l1 ⊔ l2) + leq-complemented-cardinality = + leq-complemented-Cardinal (cardinality X) (cardinality Y) + + is-prop-leq-complemented-cardinality : + is-prop leq-complemented-cardinality + is-prop-leq-complemented-cardinality = + is-prop-leq-complemented-Cardinal + + compute-leq-complemented-prop-cardinality' : + leq-complemented-prop-cardinality ＝ + mere-decidable-emb-Prop (type-Set X) (type-Set Y) + compute-leq-complemented-prop-cardinality' = + ( htpy-eq + ( triangle-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( leq-complemented-prop-Cardinal') X) (cardinality Y)) ∙ + ( compute-leq-complemented-prop-Cardinal' X Y) + + compute-leq-complemented-cardinality' : + leq-complemented-cardinality ＝ + mere-decidable-emb (type-Set X) (type-Set Y) + compute-leq-complemented-cardinality' = + ap type-Prop compute-leq-complemented-prop-cardinality' + + compute-leq-complemented-cardinality : + leq-complemented-cardinality ≃ + mere-decidable-emb (type-Set X) (type-Set Y) + compute-leq-complemented-cardinality = + equiv-eq compute-leq-complemented-cardinality' + + unit-leq-complemented-cardinality : + mere-decidable-emb (type-Set X) (type-Set Y) → + leq-complemented-cardinality + unit-leq-complemented-cardinality = + map-inv-equiv compute-leq-complemented-cardinality + + inv-unit-leq-complemented-cardinality : + leq-complemented-cardinality → + mere-decidable-emb (type-Set X) (type-Set Y) + inv-unit-leq-complemented-cardinality = + pr1 compute-leq-complemented-cardinality +``` + +### Complemented inequality on cardinals is reflexive + +```agda +refl-leq-complemented-cardinality : + is-reflexive-Large-Relation Set leq-complemented-cardinality +refl-leq-complemented-cardinality A = + unit-leq-complemented-cardinality A A + ( refl-mere-decidable-emb (type-Set A)) + +refl-leq-complemented-Cardinal : + is-reflexive-Large-Relation Cardinal leq-complemented-Cardinal +refl-leq-complemented-Cardinal = + apply-dependent-universal-property-trunc-Set' + ( λ X → set-Prop (leq-complemented-prop-Cardinal X X)) + ( refl-leq-complemented-cardinality) +``` + +### Complemented inequality on cardinals is transitive + +```agda +module _ + {l1 l2 l3 : Level} + where + + transitive-leq-complemented-cardinality : + (X : Set l1) (Y : Set l2) (Z : Set l3) → + leq-complemented-cardinality Y Z → + leq-complemented-cardinality X Y → + leq-complemented-cardinality X Z + transitive-leq-complemented-cardinality X Y Z Y≤Z X≤Y = + unit-leq-complemented-cardinality X Z + ( transitive-mere-decidable-emb + ( inv-unit-leq-complemented-cardinality Y Z Y≤Z) + ( inv-unit-leq-complemented-cardinality X Y X≤Y)) + + transitive-leq-complemented-Cardinal : + (X : Cardinal l1) (Y : Cardinal l2) (Z : Cardinal l3) → + leq-complemented-Cardinal Y Z → + leq-complemented-Cardinal X Y → + leq-complemented-Cardinal X Z + transitive-leq-complemented-Cardinal = + apply-thrice-dependent-universal-property-trunc-Set' + ( λ X Y Z → + ( leq-complemented-Cardinal Y Z → + leq-complemented-Cardinal X Y → + leq-complemented-Cardinal X Z) , + ( is-set-function-type + ( is-set-function-type + ( is-set-is-prop is-prop-leq-complemented-Cardinal)))) + ( transitive-leq-complemented-cardinality) +``` + +## Properties + +### Assuming the weak limited principle of omniscience, then complemented inequality forms a partial order + +This is a direct consequence of the +[Cantor–Schröder–Bernstein theorem for decidable embeddings](foundation.cantor-schroder-bernstein-decidable-embeddings.md). + +```agda +module _ + {l : Level} (wlpo : level-WLPO l) + where + + antisymmetric-leq-complemented-cardinality : + (X Y : Set l) → + leq-complemented-cardinality X Y → + leq-complemented-cardinality Y X → + cardinality X ＝ cardinality Y + antisymmetric-leq-complemented-cardinality X Y X≤Y Y≤X = + eq-mere-equiv-cardinality X Y + ( antisymmetric-mere-decidable-emb + ( wlpo) + ( inv-unit-leq-complemented-cardinality X Y X≤Y) + ( inv-unit-leq-complemented-cardinality Y X Y≤X)) + + antisymmetric-leq-complemented-Cardinal : + (X Y : Cardinal l) → + leq-complemented-Cardinal X Y → leq-complemented-Cardinal Y X → X ＝ Y + antisymmetric-leq-complemented-Cardinal = + apply-twice-dependent-universal-property-trunc-Set' + ( λ X Y → + set-Prop + ( function-Prop + ( leq-complemented-Cardinal X Y) + ( function-Prop + ( leq-complemented-Cardinal Y X) + ( Id-Prop (Cardinal-Set l) X Y)))) + ( antisymmetric-leq-complemented-cardinality) +``` + +### The large poset of cardinals under complemented inequality + +```agda +large-preorder-complemented-Cardinal : Large-Preorder lsuc (_⊔_) +large-preorder-complemented-Cardinal = + λ where + .type-Large-Preorder → Cardinal + .leq-prop-Large-Preorder → leq-complemented-prop-Cardinal + .refl-leq-Large-Preorder → refl-leq-complemented-Cardinal + .transitive-leq-Large-Preorder → transitive-leq-complemented-Cardinal + +large-poset-complemented-Cardinal : WLPO → Large-Poset lsuc (_⊔_) +large-poset-complemented-Cardinal wlpo = + λ where + .large-preorder-Large-Poset → large-preorder-complemented-Cardinal + .antisymmetric-leq-Large-Poset → antisymmetric-leq-complemented-Cardinal wlpo +``` + +## See also + +- [Inequality of cardinals](set-theory.inequality-cardinals.md) diff --git a/src/set-theory/dependent-products-cardinals.lagda.md b/src/set-theory/dependent-products-cardinals.lagda.md new file mode 100644 index 00000000000..ba06b027946 --- /dev/null +++ b/src/set-theory/dependent-products-cardinals.lagda.md @@ -0,0 +1,135 @@ +# Dependent products of cardinals + +```agda +module set-theory.dependent-products-cardinals where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.functoriality-set-truncation +open import foundation.identity-types +open import foundation.set-truncations +open import foundation.sets +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import foundation-core.propositions + +open import set-theory.cardinality-projective-sets +open import set-theory.cardinality-recursive-sets +open import set-theory.cardinals +open import set-theory.inhabited-cardinals +``` + +
+ +## Idea + +Given a family of cardinals $κ : I → \mathrm{Cardinal}$ over a +[cardinality-recursive set](set-theory.cardinality-recursive-sets.md) $I$, then +we may define the {{#concept "dependent product cardinal" Agda=Π-Cardinal'}} +$Π_{i∈I}κᵢ$, as the cardinality of the +[dependent product](foundation.dependent-function-types.md) of any family of +representing sets $Kᵢ$. + +## Definitions + +```agda +module _ + {l1 l2 : Level} (X : Set l1) + where + + cardinality-Π : (type-Set X → Set l2) → Cardinal (l1 ⊔ l2) + cardinality-Π Y = cardinality (Π-Set X Y) +``` + +### Dependent products of cardinals over cardinality-recursive sets + +```agda +module _ + {l1 l2 : Level} (X : Cardinality-Recursive-Set l1 l2) + (let set-X = set-Cardinality-Recursive-Set X) + where + + Π-Cardinal' : + (type-Set set-X → Cardinal l2) → Cardinal (l1 ⊔ l2) + Π-Cardinal' Y = + map-trunc-Set (Π-Set set-X) (unit-Cardinality-Recursive-Set X Y) + + compute-Π-Cardinal' : + (K : type-Cardinality-Recursive-Set X → Set l2) → + Π-Cardinal' (cardinality ∘ K) ＝ cardinality (Π-Set set-X K) + compute-Π-Cardinal' K = + equational-reasoning + map-trunc-Set + ( Π-Set set-X) + ( unit-Cardinality-Recursive-Set X (cardinality ∘ K)) + ＝ map-trunc-Set (Π-Set set-X) (unit-trunc-Set K) + by + ap + ( map-trunc-Set (Π-Set set-X)) + ( compute-unit-Cardinality-Recursive-Set X K) + ＝ cardinality (Π-Set set-X K) + by naturality-unit-trunc-Set (Π-Set set-X) K +``` + +### Dependent products of cardinals over cardinality-projective sets + +```agda +module _ + {l1 l2 : Level} (X : Cardinality-Projective-Set l1 l2) + where + + Π-Cardinal : + (type-Cardinality-Projective-Set X → Cardinal l2) → Cardinal (l1 ⊔ l2) + Π-Cardinal = + Π-Cardinal' (cardinality-recursive-set-Cardinality-Projective-Set X) + + compute-Π-Cardinal : + (Y : type-Cardinality-Projective-Set X → Set l2) → + Π-Cardinal (cardinality ∘ Y) ＝ + cardinality (Π-Set (set-Cardinality-Projective-Set X) Y) + compute-Π-Cardinal = + compute-Π-Cardinal' (cardinality-recursive-set-Cardinality-Projective-Set X) +``` + +## Properties + +### Dependent products of inhabited cardinals are inhabited + +```agda +module _ + {l1 l2 : Level} (X : Cardinality-Projective-Set l1 l2) + (let type-X = type-Cardinality-Projective-Set X) + where + + is-inhabited-Π-Cardinal : + (K : type-X → Cardinal l2) → + ((x : type-X) → is-inhabited-Cardinal (K x)) → + is-inhabited-Cardinal (Π-Cardinal X K) + is-inhabited-Π-Cardinal = + ind-Cardinality-Projective-Set X + ( λ K → + set-Prop + ( function-Prop + ( (x : type-X) → is-inhabited-Cardinal (K x)) + ( is-inhabited-prop-Cardinal (Π-Cardinal X K)))) + ( λ Y y → + inv-tr + ( is-inhabited-Cardinal) + ( compute-Π-Cardinal X Y) + ( unit-is-inhabited-cardinality + ( Π-Set (set-Cardinality-Projective-Set X) Y) + ( is-projective-Cardinality-Projective-Set X + ( type-Set ∘ Y) + ( λ x → inv-unit-is-inhabited-cardinality (Y x) (y x))))) + + Π-Inhabited-Cardinal : + (type-X → Inhabited-Cardinal l2) → Inhabited-Cardinal (l1 ⊔ l2) + Π-Inhabited-Cardinal K = + ( Π-Cardinal X (pr1 ∘ K) , is-inhabited-Π-Cardinal (pr1 ∘ K) (pr2 ∘ K)) +``` diff --git a/src/set-theory/dependent-sums-cardinals.lagda.md b/src/set-theory/dependent-sums-cardinals.lagda.md new file mode 100644 index 00000000000..ac7a7f1f34f --- /dev/null +++ b/src/set-theory/dependent-sums-cardinals.lagda.md @@ -0,0 +1,162 @@ +# Dependent sums of cardinals + +```agda +module set-theory.dependent-sums-cardinals where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.functoriality-set-truncation +open import foundation.identity-types +open import foundation.inhabited-types +open import foundation.mere-embeddings +open import foundation.projective-types +open import foundation.set-truncations +open import foundation.sets +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import foundation-core.propositions + +open import set-theory.cardinality-projective-sets +open import set-theory.cardinality-recursive-sets +open import set-theory.cardinals +open import set-theory.inequality-cardinals +open import set-theory.inhabited-cardinals +``` + +
+ +## Idea + +Given a family of cardinals $κ : I → \mathrm{Cardinal}$ over a +[cardinality-recursive set](set-theory.cardinality-recursive-sets.md) $I$, then +we may define the {{#concept "dependent sum cardinal" Agda=Σ-Cardinal'}} +$Σ_{i∈I}κᵢ$, as the cardinality of the +[dependent sum](foundation.dependent-pair-types.md) of any family of +representing sets $Kᵢ$. + +## Definitions + +### The cardinality of a dependent sum of sets + +```agda +module _ + {l1 l2 : Level} (X : Set l1) + where + + cardinality-Σ : (type-Set X → Set l2) → Cardinal (l1 ⊔ l2) + cardinality-Σ Y = cardinality (Σ-Set X Y) +``` + +### Dependent sums of cardinals over cardinality-recursive sets + +```agda +module _ + {l1 l2 : Level} (X : Cardinality-Recursive-Set l1 l2) + (let set-X = set-Cardinality-Recursive-Set X) + (let type-X = type-Cardinality-Recursive-Set X) + where + + Σ-Cardinal' : + (type-X → Cardinal l2) → Cardinal (l1 ⊔ l2) + Σ-Cardinal' K = + map-trunc-Set (Σ-Set set-X) (unit-Cardinality-Recursive-Set X K) + + compute-Σ-Cardinal' : + (Y : type-X → Set l2) → + Σ-Cardinal' (cardinality ∘ Y) ＝ cardinality (Σ-Set set-X Y) + compute-Σ-Cardinal' Y = + equational-reasoning + Σ-Cardinal' (cardinality ∘ Y) + ＝ map-trunc-Set (Σ-Set set-X) (unit-trunc-Set Y) + by + ap + ( map-trunc-Set (Σ-Set set-X)) + ( compute-unit-Cardinality-Recursive-Set X Y) + ＝ cardinality (Σ-Set set-X Y) + by naturality-unit-trunc-Set (Σ-Set set-X) Y +``` + +### Dependent sums of cardinals over cardinality-projective sets + +```agda +module _ + {l1 l2 : Level} (X : Cardinality-Projective-Set l1 l2) + where + + Σ-Cardinal : + (type-Cardinality-Projective-Set X → Cardinal l2) → Cardinal (l1 ⊔ l2) + Σ-Cardinal = + Σ-Cardinal' (cardinality-recursive-set-Cardinality-Projective-Set X) + + compute-Σ-Cardinal : + (Y : type-Cardinality-Projective-Set X → Set l2) → + Σ-Cardinal (cardinality ∘ Y) ＝ + cardinality (Σ-Set (set-Cardinality-Projective-Set X) Y) + compute-Σ-Cardinal = + compute-Σ-Cardinal' (cardinality-recursive-set-Cardinality-Projective-Set X) +``` + +## Properties + +### Dependent sums of inhabited cardinals are inhabited + +```agda +module _ + {l1 l2 : Level} (X : Cardinality-Projective-Set l1 l2) + (let type-X = type-Cardinality-Projective-Set X) + (|x| : is-inhabited type-X) + where + + is-inhabited-Σ-Cardinal : + (K : type-X → Cardinal l2) → + ((x : type-X) → is-inhabited-Cardinal (K x)) → + is-inhabited-Cardinal (Σ-Cardinal X K) + is-inhabited-Σ-Cardinal = + ind-Cardinality-Projective-Set X + ( λ K → + set-Prop + ( function-Prop + ( (x : type-X) → is-inhabited-Cardinal (K x)) + ( is-inhabited-prop-Cardinal (Σ-Cardinal X K)))) + ( λ Y y → + inv-tr + ( is-inhabited-Cardinal) + ( compute-Σ-Cardinal X Y) + ( unit-is-inhabited-cardinality + ( Σ-Set (set-Cardinality-Projective-Set X) Y) + ( is-inhabited-Σ + ( |x|) + ( λ x → inv-unit-is-inhabited-cardinality (Y x) (y x))))) + + Σ-Inhabited-Cardinal : + (type-X → Inhabited-Cardinal l2) → Inhabited-Cardinal (l1 ⊔ l2) + Σ-Inhabited-Cardinal K = + ( Σ-Cardinal X (pr1 ∘ K) , is-inhabited-Σ-Cardinal (pr1 ∘ K) (pr2 ∘ K)) +``` + +### Inequality of cardinalities is preserved under dependent sums over projective types + +```agda +module _ + {l1 l2 : Level} (X : Set l1) + (is-projective-X : is-projective-Level' l2 (type-Set X)) + where + + leq-cardinality-Σ : + (K P : type-Set X → Set l2) → + ((i : type-Set X) → leq-cardinality (K i) (P i)) → + leq-cardinality (Σ-Set X K) (Σ-Set X P) + leq-cardinality-Σ K P f = + unit-leq-cardinality + ( Σ-Set X K) + ( Σ-Set X P) + ( mere-emb-tot + ( is-projective-X) + ( λ x → inv-unit-leq-cardinality (K x) (P x) (f x))) +``` diff --git a/src/set-theory/equality-cardinals.lagda.md b/src/set-theory/equality-cardinals.lagda.md new file mode 100644 index 00000000000..8e1f4227d50 --- /dev/null +++ b/src/set-theory/equality-cardinals.lagda.md @@ -0,0 +1,313 @@ +# Equality of cardinals + +```agda +module set-theory.equality-cardinals where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.functoriality-propositional-truncation +open import foundation.identity-types +open import foundation.large-equivalence-relations +open import foundation.large-similarity-relations +open import foundation.mere-equivalences +open import foundation.propositional-extensionality +open import foundation.propositions +open import foundation.set-truncations +open import foundation.sets +open import foundation.univalence +open import foundation.universe-levels + +open import set-theory.cardinals +``` + +
+ +## Idea + +Two [cardinals of sets](set-theory.cardinals.md) `X` and `Y` are +{{#concept "similar" Disambiguation="cardinals" Agda=sim-Cardinal}} if there +[merely exists](foundation.inhabited-types.md) an +[equivalence](foundation-core.equivalences.md) between any two representing +[sets](foundation-core.sets.md). This characterizes +[equality](foundation-core.identity-types.md) of cardinals. + +## Definition + +### The underlying similarity of cardinalities + +```agda +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + sim-prop-cardinality' : Prop (l1 ⊔ l2) + sim-prop-cardinality' = mere-equiv-Prop (type-Set X) (type-Set Y) + + sim-cardinality' : UU (l1 ⊔ l2) + sim-cardinality' = mere-equiv (type-Set X) (type-Set Y) + + is-prop-sim-sim-cardinality' : is-prop sim-cardinality' + is-prop-sim-sim-cardinality' = is-prop-mere-equiv (type-Set X) (type-Set Y) + +refl-sim-cardinality' : {l : Level} (X : Set l) → sim-cardinality' X X +refl-sim-cardinality' X = refl-mere-equiv (type-Set X) + +transitive-sim-cardinality' : + {l1 l2 l3 : Level} (X : Set l1) (Y : Set l2) (Z : Set l3) → + sim-cardinality' Y Z → sim-cardinality' X Y → sim-cardinality' X Z +transitive-sim-cardinality' X Y Z = + transitive-mere-equiv (type-Set X) (type-Set Y) (type-Set Z) + +symmetric-sim-cardinality' : + {l1 l2 : Level} (X : Set l1) (Y : Set l2) → + sim-cardinality' X Y → sim-cardinality' Y X +symmetric-sim-cardinality' X Y = + symmetric-mere-equiv (type-Set X) (type-Set Y) +``` + +### Similarity of cardinalities with a cardinal + +```agda +module _ + {l1 l2 : Level} (X : Set l1) + where + + sim-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2) + sim-prop-Cardinal' = + map-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( sim-prop-cardinality' X) + + sim-Cardinal' : Cardinal l2 → UU (l1 ⊔ l2) + sim-Cardinal' Y = type-Prop (sim-prop-Cardinal' Y) + + is-prop-sim-sim-Cardinal' : (Y : Cardinal l2) → is-prop (sim-Cardinal' Y) + is-prop-sim-sim-Cardinal' Y = is-prop-type-Prop (sim-prop-Cardinal' Y) + + eq-compute-sim-prop-Cardinal' : + (Y : Set l2) → + sim-prop-Cardinal' (cardinality Y) ＝ sim-prop-cardinality' X Y + eq-compute-sim-prop-Cardinal' = + triangle-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( sim-prop-cardinality' X) + + eq-compute-sim-Cardinal' : + (Y : Set l2) → + sim-Cardinal' (cardinality Y) ＝ sim-cardinality' X Y + eq-compute-sim-Cardinal' Y = + ap type-Prop (eq-compute-sim-prop-Cardinal' Y) +``` + +### Similarity of cardinals + +```agda +module _ + {l1 l2 : Level} (X : Cardinal l1) (Y : Cardinal l2) + where + + sim-prop-Cardinal : Prop (l1 ⊔ l2) + sim-prop-Cardinal = + map-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( sim-prop-Cardinal') + ( X) + ( Y) + + sim-Cardinal : UU (l1 ⊔ l2) + sim-Cardinal = type-Prop sim-prop-Cardinal + + is-prop-sim-sim-Cardinal : is-prop sim-Cardinal + is-prop-sim-sim-Cardinal = is-prop-type-Prop sim-prop-Cardinal + + sim-set-Cardinal : Set (l1 ⊔ l2) + sim-set-Cardinal = set-Prop sim-prop-Cardinal +``` + +### Similarity of cardinalities + +```agda +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + sim-prop-cardinality : Prop (l1 ⊔ l2) + sim-prop-cardinality = sim-prop-Cardinal (cardinality X) (cardinality Y) + + sim-cardinality : UU (l1 ⊔ l2) + sim-cardinality = type-Prop sim-prop-cardinality + + is-prop-sim-sim-cardinality : is-prop sim-cardinality + is-prop-sim-sim-cardinality = is-prop-type-Prop sim-prop-cardinality + + eq-compute-sim-prop-cardinality : + sim-prop-cardinality ＝ mere-equiv-Prop (type-Set X) (type-Set Y) + eq-compute-sim-prop-cardinality = + ( htpy-eq + ( triangle-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( sim-prop-Cardinal') + ( X)) + ( cardinality Y)) ∙ + ( eq-compute-sim-prop-Cardinal' X Y) + + eq-compute-sim-cardinality : + sim-cardinality ＝ mere-equiv (type-Set X) (type-Set Y) + eq-compute-sim-cardinality = + ap type-Prop eq-compute-sim-prop-cardinality + + compute-sim-cardinality : + sim-cardinality ≃ mere-equiv (type-Set X) (type-Set Y) + compute-sim-cardinality = equiv-eq eq-compute-sim-cardinality + + unit-sim-cardinality : + mere-equiv (type-Set X) (type-Set Y) → sim-cardinality + unit-sim-cardinality = map-inv-equiv compute-sim-cardinality + + inv-unit-sim-cardinality : + sim-cardinality → mere-equiv (type-Set X) (type-Set Y) + inv-unit-sim-cardinality = pr1 compute-sim-cardinality +``` + +## Properties + +### Equality of cardinalities is equivalent to mere equivalence + +```agda +is-effective-cardinality : + {l : Level} (X Y : Set l) → + (cardinality X ＝ cardinality Y) ≃ mere-equiv (type-Set X) (type-Set Y) +is-effective-cardinality X Y = + ( equiv-trunc-Prop (extensionality-Set X Y)) ∘e + ( is-effective-unit-trunc-Set (Set _) X Y) + +eq-mere-equiv-cardinality : + {l : Level} (X Y : Set l) → + mere-equiv (type-Set X) (type-Set Y) → cardinality X ＝ cardinality Y +eq-mere-equiv-cardinality X Y = map-inv-equiv (is-effective-cardinality X Y) +``` + +### Similarity of cardinals is reflexive + +```agda +refl-sim-cardinality : {l : Level} (X : Set l) → sim-cardinality X X +refl-sim-cardinality X = unit-sim-cardinality X X (refl-mere-equiv (type-Set X)) + +refl-sim-Cardinal : {l : Level} (X : Cardinal l) → sim-Cardinal X X +refl-sim-Cardinal = + apply-dependent-universal-property-trunc-Set' + ( λ X → sim-set-Cardinal X X) + ( refl-sim-cardinality) +``` + +### Similarity of cardinals is symmetric + +```agda +symmetric-sim-cardinality : + {l1 l2 : Level} + (X : Set l1) (Y : Set l2) → + sim-cardinality X Y → sim-cardinality Y X +symmetric-sim-cardinality X Y p = + unit-sim-cardinality Y X + ( symmetric-sim-cardinality' X Y (inv-unit-sim-cardinality X Y p)) + +abstract + symmetric-sim-Cardinal : + {l1 l2 : Level} + (X : Cardinal l1) (Y : Cardinal l2) → + sim-Cardinal X Y → sim-Cardinal Y X + symmetric-sim-Cardinal = + apply-twice-dependent-universal-property-trunc-Set' + ( λ X Y → hom-set-Set (sim-set-Cardinal X Y) (sim-set-Cardinal Y X)) + ( symmetric-sim-cardinality) +``` + +### Similarity of cardinals is transitive + +```agda +transitive-sim-cardinality : + {l1 l2 l3 : Level} + (X : Set l1) (Y : Set l2) (Z : Set l3) → + sim-cardinality Y Z → sim-cardinality X Y → sim-cardinality X Z +transitive-sim-cardinality X Y Z p q = + unit-sim-cardinality X Z + ( transitive-sim-cardinality' X Y Z + ( inv-unit-sim-cardinality Y Z p) + ( inv-unit-sim-cardinality X Y q)) + +abstract + transitive-sim-Cardinal : + {l1 l2 l3 : Level} + (X : Cardinal l1) (Y : Cardinal l2) (Z : Cardinal l3) → + sim-Cardinal Y Z → sim-Cardinal X Y → sim-Cardinal X Z + transitive-sim-Cardinal = + apply-thrice-dependent-universal-property-trunc-Set' + ( λ X Y Z → + hom-set-Set + ( sim-set-Cardinal Y Z) + ( hom-set-Set (sim-set-Cardinal X Y) (sim-set-Cardinal X Z))) + ( transitive-sim-cardinality) +``` + +### Similarity of cardinals is extensional + +```agda +module _ + {l : Level} + where + + sim-eq-Cardinal : + (X Y : Cardinal l) → X ＝ Y → sim-Cardinal X Y + sim-eq-Cardinal X .X refl = refl-sim-Cardinal X + + sim-eq-cardinality : + (X Y : Set l) → cardinality X ＝ cardinality Y → sim-cardinality X Y + sim-eq-cardinality X Y = sim-eq-Cardinal (cardinality X) (cardinality Y) + + eq-sim-cardinality : + (X Y : Set l) → sim-cardinality X Y → cardinality X ＝ cardinality Y + eq-sim-cardinality X Y p = + eq-mere-equiv-cardinality X Y (inv-unit-sim-cardinality X Y p) + + abstract + eq-sim-Cardinal : + (X Y : Cardinal l) → sim-Cardinal X Y → X ＝ Y + eq-sim-Cardinal = + apply-twice-dependent-universal-property-trunc-Set' + ( λ X Y → + hom-set-Set + ( sim-set-Cardinal X Y) + ( set-Prop (Id-Prop (Cardinal-Set l) X Y))) + ( eq-sim-cardinality) + + abstract + antisymmetric-sim-Cardinal : + (X Y : Cardinal l) → sim-Cardinal X Y → sim-Cardinal Y X → X ＝ Y + antisymmetric-sim-Cardinal X Y p _ = eq-sim-Cardinal X Y p +``` + +### Similarity of cardinals is a large similarity relation + +```agda +large-equivalence-relation-Cardinal : Large-Equivalence-Relation (_⊔_) Cardinal +large-equivalence-relation-Cardinal = + λ where + .sim-prop-Large-Equivalence-Relation → sim-prop-Cardinal + .refl-sim-Large-Equivalence-Relation → refl-sim-Cardinal + .symmetric-sim-Large-Equivalence-Relation → symmetric-sim-Cardinal + .transitive-sim-Large-Equivalence-Relation → transitive-sim-Cardinal + +large-similarity-relation-Cardinal : Large-Similarity-Relation (_⊔_) Cardinal +large-similarity-relation-Cardinal = + λ where + .large-equivalence-relation-Large-Similarity-Relation → + large-equivalence-relation-Cardinal + .eq-sim-Large-Similarity-Relation → + eq-sim-Cardinal +``` diff --git a/src/set-theory/inequality-cardinals.lagda.md b/src/set-theory/inequality-cardinals.lagda.md new file mode 100644 index 00000000000..717d4df0b24 --- /dev/null +++ b/src/set-theory/inequality-cardinals.lagda.md @@ -0,0 +1,237 @@ +# Inequality on cardinals + +```agda +module set-theory.inequality-cardinals where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.identity-types +open import foundation.large-binary-relations +open import foundation.law-of-excluded-middle +open import foundation.mere-embeddings +open import foundation.propositional-extensionality +open import foundation.propositions +open import foundation.set-truncations +open import foundation.sets +open import foundation.univalence +open import foundation.universe-levels + +open import order-theory.large-posets +open import order-theory.large-preorders + +open import set-theory.cardinals +open import set-theory.equality-cardinals +``` + +
+ +## Idea + +We say a [cardinal of sets](set-theory.cardinals.md) `X` is +{{#concept "less than or equal to" Agda=leq-Cardinal}} a cardinal `Y` if any +[set](foundation-core.sets.md) in the isomorphism class represented by `X` +embeds into any set in the isomorphism class represented by `Y`. This defines +the {{#concept "standard ordering" Disambiguation="on cardinalities of sets"}} +on cardinalities of sets. + +Under the assumption of the +[law of excluded middle](foundation.law-of-excluded-middle.md), this relation is +antisymmetric and hence defines a [partial order](order-theory.posets.md) on +cardinalites. + +## Definition + +### Boundedness of the cardinality of a set + +```agda +module _ + {l1 l2 : Level} (X : Set l1) + where + + leq-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2) + leq-prop-Cardinal' = + map-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y')) + + compute-leq-prop-Cardinal' : + (Y : Set l2) → + leq-prop-Cardinal' (cardinality Y) ＝ + mere-emb-Prop (type-Set X) (type-Set Y) + compute-leq-prop-Cardinal' = + triangle-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y')) +``` + +### Inequality of cardinals + +```agda +module _ + {l1 l2 : Level} + where + + leq-prop-Cardinal : Cardinal l1 → Cardinal l2 → Prop (l1 ⊔ l2) + leq-prop-Cardinal = + map-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( leq-prop-Cardinal') + + leq-Cardinal : Cardinal l1 → Cardinal l2 → UU (l1 ⊔ l2) + leq-Cardinal X Y = type-Prop (leq-prop-Cardinal X Y) + + is-prop-leq-Cardinal : + {X : Cardinal l1} {Y : Cardinal l2} → is-prop (leq-Cardinal X Y) + is-prop-leq-Cardinal {X} {Y} = is-prop-type-Prop (leq-prop-Cardinal X Y) +``` + +### Inequality of cardinalities + +```agda +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + leq-prop-cardinality : Prop (l1 ⊔ l2) + leq-prop-cardinality = leq-prop-Cardinal (cardinality X) (cardinality Y) + + leq-cardinality : UU (l1 ⊔ l2) + leq-cardinality = leq-Cardinal (cardinality X) (cardinality Y) + + is-prop-leq-cardinality : is-prop leq-cardinality + is-prop-leq-cardinality = is-prop-leq-Cardinal + + eq-compute-leq-prop-cardinality : + leq-prop-cardinality ＝ mere-emb-Prop (type-Set X) (type-Set Y) + eq-compute-leq-prop-cardinality = + ( htpy-eq + ( triangle-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( leq-prop-Cardinal') X) (cardinality Y)) ∙ + ( compute-leq-prop-Cardinal' X Y) + + eq-compute-leq-cardinality : + leq-cardinality ＝ mere-emb (type-Set X) (type-Set Y) + eq-compute-leq-cardinality = + ap type-Prop eq-compute-leq-prop-cardinality + + compute-leq-cardinality : + leq-cardinality ≃ mere-emb (type-Set X) (type-Set Y) + compute-leq-cardinality = equiv-eq eq-compute-leq-cardinality + + unit-leq-cardinality : + mere-emb (type-Set X) (type-Set Y) → leq-cardinality + unit-leq-cardinality = map-inv-equiv compute-leq-cardinality + + inv-unit-leq-cardinality : + leq-cardinality → mere-emb (type-Set X) (type-Set Y) + inv-unit-leq-cardinality = pr1 compute-leq-cardinality +``` + +### Inequality on cardinals is reflexive + +```agda +refl-leq-cardinality : is-reflexive-Large-Relation Set leq-cardinality +refl-leq-cardinality A = unit-leq-cardinality A A (refl-mere-emb (type-Set A)) + +refl-leq-Cardinal : is-reflexive-Large-Relation Cardinal leq-Cardinal +refl-leq-Cardinal = + apply-dependent-universal-property-trunc-Set' + ( λ X → set-Prop (leq-prop-Cardinal X X)) + ( refl-leq-cardinality) +``` + +### Inequality on cardinals is transitive + +```agda +module _ + {l1 l2 l3 : Level} + where + + transitive-leq-cardinality : + (X : Set l1) (Y : Set l2) (Z : Set l3) → + leq-cardinality Y Z → leq-cardinality X Y → leq-cardinality X Z + transitive-leq-cardinality X Y Z Y≤Z X≤Y = + unit-leq-cardinality X Z + ( transitive-mere-emb + ( inv-unit-leq-cardinality Y Z Y≤Z) + ( inv-unit-leq-cardinality X Y X≤Y)) + + transitive-leq-Cardinal : + (X : Cardinal l1) (Y : Cardinal l2) (Z : Cardinal l3) → + leq-Cardinal Y Z → leq-Cardinal X Y → leq-Cardinal X Z + transitive-leq-Cardinal = + apply-thrice-dependent-universal-property-trunc-Set' + ( λ X Y Z → + ( leq-Cardinal Y Z → leq-Cardinal X Y → leq-Cardinal X Z) , + ( is-set-function-type + ( is-set-function-type + ( is-set-is-prop is-prop-leq-Cardinal)))) + ( transitive-leq-cardinality) +``` + +## Properties + +### Assuming excluded middle, then inequality is antisymmetric + +Using that mere equivalence characterizes equality of cardinals we can conclude +by the Cantor–Schröder–Bernstein theorem, assuming the law of excluded middle, +that `leq-Cardinal` is antisymmetric and hence a partial order. + +```agda +module _ + {l : Level} (lem : level-LEM l) + where + + antisymmetric-leq-cardinality : + (X Y : Set l) → + leq-cardinality X Y → + leq-cardinality Y X → + cardinality X ＝ cardinality Y + antisymmetric-leq-cardinality X Y X≤Y Y≤X = + eq-mere-equiv-cardinality X Y + ( antisymmetric-mere-emb + ( lem) + ( inv-unit-leq-cardinality X Y X≤Y) + ( inv-unit-leq-cardinality Y X Y≤X)) + + antisymmetric-leq-Cardinal : + (X Y : Cardinal l) → + leq-Cardinal X Y → leq-Cardinal Y X → X ＝ Y + antisymmetric-leq-Cardinal = + apply-twice-dependent-universal-property-trunc-Set' + ( λ X Y → + set-Prop + ( function-Prop + ( leq-Cardinal X Y) + ( function-Prop (leq-Cardinal Y X) (Id-Prop (Cardinal-Set l) X Y)))) + ( antisymmetric-leq-cardinality) +``` + +### The large poset of cardinals + +```agda +large-preorder-Cardinal : Large-Preorder lsuc (_⊔_) +large-preorder-Cardinal = + λ where + .type-Large-Preorder → Cardinal + .leq-prop-Large-Preorder → leq-prop-Cardinal + .refl-leq-Large-Preorder → refl-leq-Cardinal + .transitive-leq-Large-Preorder → transitive-leq-Cardinal + +large-poset-Cardinal : LEM → Large-Poset lsuc (_⊔_) +large-poset-Cardinal lem = + λ where + .large-preorder-Large-Poset → large-preorder-Cardinal + .antisymmetric-leq-Large-Poset → antisymmetric-leq-Cardinal lem +``` + +## See also + +- [Complemented inequality of cardinals](set-theory.complemented-inequality-cardinals.md) diff --git a/src/set-theory/infinite-sets.lagda.md b/src/set-theory/infinite-sets.lagda.md index d94e6be82f9..0016b645382 100644 --- a/src/set-theory/infinite-sets.lagda.md +++ b/src/set-theory/infinite-sets.lagda.md @@ -24,7 +24,7 @@ open import univalent-combinatorics.standard-finite-types A [set](foundation-core.sets.md) `A` is said to be {{#concept "infinite" Disambiguation="set" WD="infinite set" WDID=Q205140}} if -it contains arbitrarily [large](set-theory.cardinalities.md) +it contains arbitrarily [large](set-theory.cardinals.md) [finite](univalent-combinatorics.finite-types.md) [subsets](foundation-core.subtypes.md). diff --git a/src/set-theory/inhabited-cardinals.lagda.md b/src/set-theory/inhabited-cardinals.lagda.md new file mode 100644 index 00000000000..cf5b41c8557 --- /dev/null +++ b/src/set-theory/inhabited-cardinals.lagda.md @@ -0,0 +1,128 @@ +# Inhabited cardinals + +```agda +module set-theory.inhabited-cardinals where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.inhabited-types +open import foundation.propositional-extensionality +open import foundation.propositions +open import foundation.set-truncations +open import foundation.sets +open import foundation.subtypes +open import foundation.univalence +open import foundation.universe-levels + +open import set-theory.cardinals +``` + +
+ +## Idea + +A [cardinal](set-theory.cardinals.md) `κ` is +{{#concept "inhabited" Disambiguation="set-cardinal" Agda=is-inhabited-Cardinal}}, +if any [set](foundation-core.sets.md) in its isomorphism class is +[inhabited](foundation.inhabited-types.md). + +## Definitions + +### The predicate on cardinals of being inhabited + +```agda +module _ + {l : Level} (κ : Cardinal l) + where + + is-inhabited-prop-Cardinal : Prop l + is-inhabited-prop-Cardinal = + apply-universal-property-trunc-Set' κ + ( Prop-Set l) + ( is-inhabited-Prop ∘ type-Set) + + is-inhabited-Cardinal : UU l + is-inhabited-Cardinal = type-Prop is-inhabited-prop-Cardinal + + is-prop-is-inhabited-Cardinal : is-prop is-inhabited-Cardinal + is-prop-is-inhabited-Cardinal = + is-prop-type-Prop is-inhabited-prop-Cardinal +``` + +### Inhabited cardinalities + +```agda +module _ + {l : Level} (X : Set l) + where + + is-inhabited-prop-cardinality : Prop l + is-inhabited-prop-cardinality = is-inhabited-prop-Cardinal (cardinality X) + + is-inhabited-cardinality : UU l + is-inhabited-cardinality = is-inhabited-Cardinal (cardinality X) + + is-prop-is-inhabited-cardinality : is-prop is-inhabited-cardinality + is-prop-is-inhabited-cardinality = + is-prop-is-inhabited-Cardinal (cardinality X) + + eq-compute-is-inhabited-prop-cardinality : + is-inhabited-prop-cardinality ＝ is-inhabited-Prop (type-Set X) + eq-compute-is-inhabited-prop-cardinality = + triangle-universal-property-trunc-Set + ( Prop-Set l) + ( is-inhabited-Prop ∘ type-Set) + ( X) + + eq-compute-is-inhabited-cardinality : + is-inhabited-cardinality ＝ is-inhabited (type-Set X) + eq-compute-is-inhabited-cardinality = + ap type-Prop eq-compute-is-inhabited-prop-cardinality + + compute-is-inhabited-cardinality : + is-inhabited-cardinality ≃ is-inhabited (type-Set X) + compute-is-inhabited-cardinality = + equiv-eq eq-compute-is-inhabited-cardinality + + unit-is-inhabited-cardinality : + is-inhabited (type-Set X) → is-inhabited-cardinality + unit-is-inhabited-cardinality = + map-inv-equiv compute-is-inhabited-cardinality + + inv-unit-is-inhabited-cardinality : + is-inhabited-cardinality → is-inhabited (type-Set X) + inv-unit-is-inhabited-cardinality = + map-equiv compute-is-inhabited-cardinality +``` + +### The universe of inhabited cardinals + +```agda +Inhabited-Cardinal : (l : Level) → UU (lsuc l) +Inhabited-Cardinal l = Σ (Cardinal l) is-inhabited-Cardinal + +is-set-Inhabited-Cardinal : {l : Level} → is-set (Inhabited-Cardinal l) +is-set-Inhabited-Cardinal = + is-set-type-subtype is-inhabited-prop-Cardinal is-set-Cardinal + +Inhabited-Cardinal-Set : (l : Level) → Set (lsuc l) +Inhabited-Cardinal-Set l = (Inhabited-Cardinal l , is-set-Inhabited-Cardinal) + +module _ + {l : Level} (κ : Inhabited-Cardinal l) + where + + cardinal-Inhabited-Cardinal : Cardinal l + cardinal-Inhabited-Cardinal = pr1 κ + + is-inhabited-Inhabited-Cardinal : + is-inhabited-Cardinal cardinal-Inhabited-Cardinal + is-inhabited-Inhabited-Cardinal = pr2 κ +``` diff --git a/src/set-theory/konigs-theorem.lagda.md b/src/set-theory/konigs-theorem.lagda.md new file mode 100644 index 00000000000..2325b6c6636 --- /dev/null +++ b/src/set-theory/konigs-theorem.lagda.md @@ -0,0 +1,134 @@ +# Kőnig's theorem + +```agda +module set-theory.konigs-theorem where +``` + +
Imports + +```agda +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.identity-types +open import foundation.nonsurjective-maps +open import foundation.projective-types +open import foundation.propositions +open import foundation.sets +open import foundation.universe-levels + +open import set-theory.cardinality-projective-sets +open import set-theory.cardinals +open import set-theory.dependent-products-cardinals +open import set-theory.dependent-sums-cardinals +open import set-theory.strict-indexed-inequality-cardinals +``` + +
+ +## Idea + +{{#concept "Kőnig's theorem" Disambiguation="for cardinals/set theory" WD="König's theorem" WDID=Q1077462 Agda=Königs-Theorem}} +states that for any pair of families of [cardinals](set-theory.cardinals.md) $A$ +and $B$ over $I$, $Aᵢ < Bᵢ$ for all $i$ then we have that $ΣᵢAᵢ < ΠᵢBᵢ$. + +In constructive mathematics we have to be more mindful of our statements than +usual. Here $I$ is any +[cardinality-projective set](set-theory.cardinality-projective-sets.md) and by +$Aᵢ < Bᵢ$ we mean that $Bᵢ$ is [inhabited](foundation.inhabited-types.md) and +that for every map $f : Aᵢ → Bᵢ$ there +[exists](foundation.existential-quantification.md) an element of $Bᵢ$ that $f$ +does not hit. + +## Lemma + +Given a projective type $I$ and a pair of families of types $A$ and $B$ over $I$ +such that for every $i : I$ every function from $Aᵢ$ to $Bᵢ$ misses an element, +then every function from $ΣᵢAᵢ$ to $ΠᵢBᵢ$ misses an element. + +```agda +module _ + {l1 l2 l3 : Level} + {I : UU l1} (p : is-projective-Level' (l2 ⊔ l3) I) + {A : I → UU l2} {B : I → UU l3} + where + + is-nonsurjective-map-Σ-Π-is-projective-base' : + (H : (i : I) (f : A i → B i) → is-nonsurjective f) + (g : Σ I A → ((i : I) → B i)) → is-nonsurjective g + is-nonsurjective-map-Σ-Π-is-projective-base' H g = + map-trunc-Prop + ( λ h → (pr1 ∘ h , (λ ((i , a) , r) → pr2 (h i) (a , htpy-eq r i)))) + ( p (λ i → nonim (λ a → g (i , a) i)) (λ i → H i (λ a → g (i , a) i))) +``` + +## Theorem + +```agda +module _ + {l1 l2 : Level} + (I : Set l1) + (is-projective-I : is-projective-Level' l2 (type-Set I)) + where + + cardinality-Königs-Theorem' : + (A B : type-Set I → Set l2) → + ((i : type-Set I) → le-indexed-cardinality' (A i) (B i)) → + le-indexed-cardinality' (Σ-Set I A) (Π-Set I B) + cardinality-Königs-Theorem' A B p = + ( is-projective-I (type-Set ∘ B) (pr1 ∘ p) , + is-nonsurjective-map-Σ-Π-is-projective-base' is-projective-I (pr2 ∘ p)) + + cardinality-Königs-Theorem : + (A B : type-Set I → Set l2) → + ((i : type-Set I) → le-indexed-cardinality (A i) (B i)) → + le-indexed-cardinality (Σ-Set I A) (Π-Set I B) + cardinality-Königs-Theorem A B p = + unit-le-indexed-cardinality + ( Σ-Set I A) + ( Π-Set I B) + ( cardinality-Königs-Theorem' A B + ( λ i → inv-unit-le-indexed-cardinality (A i) (B i) (p i))) + +module _ + {l1 l2 : Level} + (I : Cardinality-Projective-Set l1 l2) + (let type-I = type-Cardinality-Projective-Set I) + (let set-I = set-Cardinality-Projective-Set I) + where + + Königs-Theorem : + (A B : type-I → Cardinal l2) → + ((i : type-I) → le-indexed-Cardinal (A i) (B i)) → + le-indexed-Cardinal (Σ-Cardinal I A) (Π-Cardinal I B) + Königs-Theorem = + apply-twice-ind-Cardinality-Projective-Set I + ( λ A B → + set-Prop + ( function-Prop + ( (i : type-I) → le-indexed-Cardinal (A i) (B i)) + ( le-indexed-prop-Cardinal (Σ-Cardinal I A) (Π-Cardinal I B)))) + ( λ A B p → + binary-tr + ( le-indexed-Cardinal) + ( inv (compute-Σ-Cardinal I A)) + ( inv (compute-Π-Cardinal I B)) + ( cardinality-Königs-Theorem + ( set-I) + ( is-projective-Cardinality-Projective-Set I) + ( A) + ( B) + ( p))) +``` + +## Comments + +More generally, for every localization `L` contained in `Set` there is an +`L`-modal Kőnig's theorem. + +## External links + +- [Kőnig's theorem (set theory)]() + on Wikipedia diff --git a/src/set-theory/strict-indexed-inequality-cardinals.lagda.md b/src/set-theory/strict-indexed-inequality-cardinals.lagda.md new file mode 100644 index 00000000000..6c5ec9d7edf --- /dev/null +++ b/src/set-theory/strict-indexed-inequality-cardinals.lagda.md @@ -0,0 +1,201 @@ +# Strict indexed inequality on cardinals + +```agda +module set-theory.strict-indexed-inequality-cardinals where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.identity-types +open import foundation.inhabited-types +open import foundation.large-binary-relations +open import foundation.law-of-excluded-middle +open import foundation.mere-embeddings +open import foundation.negation +open import foundation.nonsurjective-maps +open import foundation.propositional-extensionality +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.set-truncations +open import foundation.sets +open import foundation.univalence +open import foundation.universe-levels + +open import set-theory.cardinals +open import set-theory.complemented-inequality-cardinals +open import set-theory.inequality-cardinals +open import set-theory.inhabited-cardinals +``` + +
+ +## Idea + +We may say a [cardinal](set-theory.cardinals.md) `X` is +{{#concept "indexed less than" Disambiguation="set-cardinal" Agda=le-indexed-Cardinal}} +a cardinal `Y` if `Y` is inhabited and any map `f` of +[sets](foundation-core.sets.md) from the isomorphism class of `X` into sets in +the isomorphism class of `Y` is +[nonsurjective](foundation.nonsurjective-maps.md) in the sense that there exists +an element in `Y` that `f` does not hit. This is a positive way of saying that +`X` is less than `Y`. This defines the +{{#concept "strict indexing ordering" Disambiguation="on set-cardinals"}}. + +## Definition + +### The underlying strict indexed inequality between cardinalities of sets + +```agda +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + le-indexed-cardinality' : UU (l1 ⊔ l2) + le-indexed-cardinality' = + is-inhabited (type-Set Y) × + ((f : type-Set X → type-Set Y) → is-nonsurjective f) + + le-indexed-prop-cardinality' : Prop (l1 ⊔ l2) + le-indexed-prop-cardinality' = + product-Prop + ( is-inhabited-Prop (type-Set Y)) + ( Π-Prop + ( type-Set X → type-Set Y) + ( is-nonsurjective-Prop)) + + is-prop-le-indexed-cardinality' : + is-prop le-indexed-cardinality' + is-prop-le-indexed-cardinality' = + is-prop-type-Prop le-indexed-prop-cardinality' +``` + +### Strict indexed inequality of a cardinal with respect to a set + +```agda +module _ + {l1 l2 : Level} (X : Set l1) + where + + le-indexed-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2) + le-indexed-prop-Cardinal' = + map-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( le-indexed-prop-cardinality' X) + + le-indexed-Cardinal' : Cardinal l2 → UU (l1 ⊔ l2) + le-indexed-Cardinal' Y = + type-Prop (le-indexed-prop-Cardinal' Y) + + compute-le-indexed-prop-Cardinal' : + (Y : Set l2) → + le-indexed-prop-Cardinal' (cardinality Y) ＝ + le-indexed-prop-cardinality' X Y + compute-le-indexed-prop-Cardinal' = + triangle-universal-property-trunc-Set + ( Prop-Set (l1 ⊔ l2)) + ( le-indexed-prop-cardinality' X) +``` + +### Strict indexed inequality of cardinals + +```agda +module _ + {l1 l2 : Level} + where + + le-indexed-prop-Cardinal : + Cardinal l1 → Cardinal l2 → Prop (l1 ⊔ l2) + le-indexed-prop-Cardinal = + map-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( le-indexed-prop-Cardinal') + + le-indexed-Cardinal : Cardinal l1 → Cardinal l2 → UU (l1 ⊔ l2) + le-indexed-Cardinal X Y = type-Prop (le-indexed-prop-Cardinal X Y) +``` + +### Strict indexed inequality of cardinalities of sets + +```agda +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + le-indexed-prop-cardinality : Prop (l1 ⊔ l2) + le-indexed-prop-cardinality = + le-indexed-prop-Cardinal (cardinality X) (cardinality Y) + + le-indexed-cardinality : UU (l1 ⊔ l2) + le-indexed-cardinality = type-Prop le-indexed-prop-cardinality + + is-prop-le-indexed-cardinality : is-prop le-indexed-cardinality + is-prop-le-indexed-cardinality = is-prop-type-Prop le-indexed-prop-cardinality + + eq-compute-le-indexed-prop-cardinality : + le-indexed-prop-cardinality ＝ le-indexed-prop-cardinality' X Y + eq-compute-le-indexed-prop-cardinality = + ( htpy-eq + ( triangle-universal-property-trunc-Set + ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) + ( le-indexed-prop-Cardinal') + ( X)) + ( cardinality Y)) ∙ + ( compute-le-indexed-prop-Cardinal' X Y) + + eq-compute-le-indexed-cardinality : + le-indexed-cardinality ＝ le-indexed-cardinality' X Y + eq-compute-le-indexed-cardinality = + ap type-Prop eq-compute-le-indexed-prop-cardinality + + compute-le-indexed-cardinality : + le-indexed-cardinality ≃ le-indexed-cardinality' X Y + compute-le-indexed-cardinality = + equiv-eq eq-compute-le-indexed-cardinality + + unit-le-indexed-cardinality : + le-indexed-cardinality' X Y → le-indexed-cardinality + unit-le-indexed-cardinality = map-inv-equiv compute-le-indexed-cardinality + + inv-unit-le-indexed-cardinality : + le-indexed-cardinality → le-indexed-cardinality' X Y + inv-unit-le-indexed-cardinality = map-equiv compute-le-indexed-cardinality +``` + +## Properties + +### Strict indexed inequality is irreflexive + +```agda +module _ + {l : Level} + where abstract + + irreflexive-le-indexed-cardinality' : + (A : Set l) → ¬ le-indexed-cardinality' A A + irreflexive-le-indexed-cardinality' A p = + rec-trunc-Prop empty-Prop (λ (x , p) → p (x , refl)) (pr2 p id) + + irreflexive-le-indexed-cardinality : + (A : Set l) → ¬ le-indexed-cardinality A A + irreflexive-le-indexed-cardinality A = + map-neg + ( inv-unit-le-indexed-cardinality A A) + ( irreflexive-le-indexed-cardinality' A) + + irreflexive-le-indexed-Cardinal : + (A : Cardinal l) → ¬ le-indexed-Cardinal A A + irreflexive-le-indexed-Cardinal = + apply-dependent-universal-property-trunc-Set' + ( λ X → set-Prop (neg-Prop (le-indexed-prop-Cardinal X X))) + ( irreflexive-le-indexed-cardinality) +``` diff --git a/src/set-theory/zero-cardinal.lagda.md b/src/set-theory/zero-cardinal.lagda.md new file mode 100644 index 00000000000..bdcde8a9392 --- /dev/null +++ b/src/set-theory/zero-cardinal.lagda.md @@ -0,0 +1,29 @@ +# The zero cardinal + +```agda +module set-theory.zero-cardinal where +``` + +
Imports + +```agda +open import foundation.empty-types +open import foundation.universe-levels + +open import set-theory.cardinals +``` + +
+ +## Idea + +The {{#concept "zero cardinal" Agda=zero-Cardinal}}, or **empty cardinal**, is +the isomorphism class of [empty](foundation.empty-types.md) +[sets](foundation-core.sets.md). + +## Definitions + +```agda +zero-Cardinal : Cardinal lzero +zero-Cardinal = cardinality empty-Set +``` diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md index de8f09d97b7..297572055d6 100644 --- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md @@ -407,9 +407,7 @@ module _ is-truncation-equivalence k f → is-truncated-acyclic-map k f is-truncated-acyclic-map-is-truncation-equivalence e = is-truncated-acyclic-map-is-epimorphism-Truncated-Type f - ( λ C → - is-emb-is-equiv - ( is-equiv-precomp-is-truncation-equivalence k f e C)) + ( λ C → is-emb-is-equiv (is-equiv-precomp-is-truncation-equivalence e C)) ``` ### `k`-acyclic maps are closed under pullbacks diff --git a/src/univalent-combinatorics/complements-isolated-elements.lagda.md b/src/univalent-combinatorics/complements-isolated-elements.lagda.md index c993815344f..2a12c8eb1fb 100644 --- a/src/univalent-combinatorics/complements-isolated-elements.lagda.md +++ b/src/univalent-combinatorics/complements-isolated-elements.lagda.md @@ -27,7 +27,7 @@ open import univalent-combinatorics.finite-types ## Idea For any element `x` in a [finite type](univalent-combinatorics.finite-types.md) -`X` of [cardinality](set-theory.cardinalities.md) `n+1`, we can construct its +`X` of [cardinality](set-theory.cardinals.md) `n+1`, we can construct its **complement**, which is a type of cardinality `n`. ## Definition diff --git a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md index 9a0db96729f..95ed6cfe55d 100644 --- a/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md +++ b/src/univalent-combinatorics/counting-decidable-subtypes.lagda.md @@ -118,7 +118,7 @@ is-decidable-count-subtype P e f x = pair ( pr1 y ＝ x) ( pair - ( is-set-count e (pr1 y) x) + ( is-set-type-count e (pr1 y) x) ( has-decidable-equality-count e (pr1 y) x))) ( f))) ``` diff --git a/src/univalent-combinatorics/counting.lagda.md b/src/univalent-combinatorics/counting.lagda.md index 71aae67e0f5..a0f7e1317bc 100644 --- a/src/univalent-combinatorics/counting.lagda.md +++ b/src/univalent-combinatorics/counting.lagda.md @@ -71,12 +71,15 @@ module _ inv-equiv-count : X ≃ Fin number-of-elements-count inv-equiv-count = inv-equiv equiv-count - is-set-count : is-set X - is-set-count = + is-set-type-count : is-set X + is-set-type-count = is-set-equiv' ( Fin number-of-elements-count) ( equiv-count) ( is-set-Fin number-of-elements-count) + + set-type-count : Set l + set-type-count = (X , is-set-type-count) ``` ## Properties diff --git a/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md b/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md index 8ef38ae7ee0..ee730f0bd7c 100644 --- a/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md +++ b/src/univalent-combinatorics/distributivity-of-set-truncation-over-finite-products.lagda.md @@ -132,6 +132,11 @@ module _ map-equiv-distributive-trunc-Π-Fin-Set = map-equiv equiv-distributive-trunc-Π-Fin-Set + is-equiv-map-equiv-distributive-trunc-Π-Fin-Set : + is-equiv map-equiv-distributive-trunc-Π-Fin-Set + is-equiv-map-equiv-distributive-trunc-Π-Fin-Set = + is-equiv-map-equiv equiv-distributive-trunc-Π-Fin-Set + triangle-distributive-trunc-Π-Fin-Set : ( map-equiv-distributive-trunc-Π-Fin-Set ∘ unit-trunc-Set) ~ ( map-Π (λ x → unit-trunc-Set)) @@ -146,15 +151,15 @@ module _ distributive-trunc-Π-count-Set : count A → is-contr - ( Σ ( ( type-trunc-Set ((x : A) → B x)) ≃ - ( (x : A) → type-trunc-Set (B x))) + ( Σ ( ║ ((x : A) → B x) ║₀ ≃ + ( (x : A) → ║ B x ║₀)) ( λ e → ( map-equiv e ∘ unit-trunc-Set) ~ ( map-Π (λ x → unit-trunc-Set)))) distributive-trunc-Π-count-Set (pair k e) = is-contr-equiv - ( Σ ( ( type-trunc-Set ((x : A) → B x)) ≃ - ( (x : Fin k) → type-trunc-Set (B (map-equiv e x)))) + ( Σ ( ( ║ ((x : A) → B x) ║₀) ≃ + ( (x : Fin k) → ║ B (map-equiv e x) ║₀)) ( λ f → ( map-equiv f ∘ unit-trunc-Set) ~ ( map-Π (λ x → unit-trunc-Set) ∘ precomp-Π (map-equiv e) B))) @@ -164,7 +169,7 @@ module _ ( map-Π (λ x → unit-trunc-Set) ∘ precomp-Π (map-equiv e) B)) ( equiv-postcomp-equiv ( equiv-precomp-Π e (type-trunc-Set ∘ B)) - ( type-trunc-Set ((x : A) → B x))) + ( ║ ((x : A) → B x) ║₀)) ( λ f → equiv-Π-equiv-family ( λ h → @@ -175,8 +180,8 @@ module _ map-Π (λ y → unit-trunc-Set) h x))) ∘e ( equiv-funext)))) ( is-contr-equiv' - ( Σ ( ( type-trunc-Set ((x : Fin k) → B (map-equiv e x))) ≃ - ( (x : Fin k) → type-trunc-Set (B (map-equiv e x)))) + ( Σ ( ( ║ ((x : Fin k) → B (map-equiv e x)) ║₀) ≃ + ( (x : Fin k) → ║ B (map-equiv e x) ║₀)) ( λ f → ( map-equiv f ∘ unit-trunc-Set) ~ ( map-Π (λ x → unit-trunc-Set)))) @@ -186,7 +191,7 @@ module _ ( map-Π (λ x → unit-trunc-Set) ∘ precomp-Π (map-equiv e) B)) ( equiv-precomp-equiv ( equiv-trunc-Set (equiv-precomp-Π e B)) - ( (x : Fin k) → type-trunc-Set (B (map-equiv e x)))) + ( (x : Fin k) → ║ B (map-equiv e x) ║₀)) ( λ f → equiv-Π ( λ h → @@ -242,36 +247,51 @@ module _ ( x)))))))) ∘e ( equiv-funext)))) ( distributive-trunc-Π-Fin-Set k (B ∘ map-equiv e))) +``` + +## Corollaries + +### Set-truncation distributes over sets equipped with counting +```agda module _ - {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (c : count A) + {l1 l2 : Level} {A : UU l1} (c : count A) (B : A → UU l2) where equiv-distributive-trunc-Π-count-Set : - ( type-trunc-Set ((x : A) → B x)) ≃ ((x : A) → type-trunc-Set (B x)) + ║ ((x : A) → B x) ║₀ ≃ ((x : A) → ║ B x ║₀) equiv-distributive-trunc-Π-count-Set = pr1 (center (distributive-trunc-Π-count-Set B c)) map-equiv-distributive-trunc-Π-count-Set : - ( type-trunc-Set ((x : A) → B x)) → ((x : A) → type-trunc-Set (B x)) + ║ ((x : A) → B x) ║₀ → ((x : A) → ║ B x ║₀) map-equiv-distributive-trunc-Π-count-Set = map-equiv equiv-distributive-trunc-Π-count-Set + is-equiv-map-equiv-distributive-trunc-Π-count-Set : + is-equiv map-equiv-distributive-trunc-Π-count-Set + is-equiv-map-equiv-distributive-trunc-Π-count-Set = + is-equiv-map-equiv equiv-distributive-trunc-Π-count-Set + triangle-distributive-trunc-Π-count-Set : ( map-equiv-distributive-trunc-Π-count-Set ∘ unit-trunc-Set) ~ ( map-Π (λ x → unit-trunc-Set)) triangle-distributive-trunc-Π-count-Set = pr2 (center (distributive-trunc-Π-count-Set B c)) +``` +### Set-truncation distributes over finite sets + +```agda module _ - {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (H : is-finite A) + {l1 l2 : Level} {A : UU l1} (H : is-finite A) (B : A → UU l2) where abstract distributive-trunc-Π-is-finite-Set : is-contr - ( Σ ( ( type-trunc-Set ((x : A) → B x)) ≃ - ( (x : A) → type-trunc-Set (B x))) + ( Σ ( ( ║ ((x : A) → B x) ║₀) ≃ + ( (x : A) → ║ B x ║₀)) ( λ e → ( map-equiv e ∘ unit-trunc-Set) ~ ( map-Π (λ x → unit-trunc-Set)))) @@ -281,18 +301,68 @@ module _ ( distributive-trunc-Π-count-Set B) equiv-distributive-trunc-Π-is-finite-Set : - ( type-trunc-Set ((x : A) → B x)) ≃ ((x : A) → type-trunc-Set (B x)) + ║ ((x : A) → B x) ║₀ ≃ ((x : A) → ║ B x ║₀) equiv-distributive-trunc-Π-is-finite-Set = pr1 (center distributive-trunc-Π-is-finite-Set) map-equiv-distributive-trunc-Π-is-finite-Set : - ( type-trunc-Set ((x : A) → B x)) → ((x : A) → type-trunc-Set (B x)) + ║ ((x : A) → B x) ║₀ → ((x : A) → ║ B x ║₀) map-equiv-distributive-trunc-Π-is-finite-Set = map-equiv equiv-distributive-trunc-Π-is-finite-Set + is-equiv-map-equiv-distributive-trunc-Π-is-finite-Set : + is-equiv map-equiv-distributive-trunc-Π-is-finite-Set + is-equiv-map-equiv-distributive-trunc-Π-is-finite-Set = + is-equiv-map-equiv equiv-distributive-trunc-Π-is-finite-Set + triangle-distributive-trunc-Π-is-finite-Set : ( map-equiv-distributive-trunc-Π-is-finite-Set ∘ unit-trunc-Set) ~ ( map-Π (λ x → unit-trunc-Set)) triangle-distributive-trunc-Π-is-finite-Set = pr2 (center distributive-trunc-Π-is-finite-Set) + +module _ + {l1 l2 : Level} (A : Finite-Type l1) (B : type-Finite-Type A → UU l2) + (let H = is-finite-type-Finite-Type A) + where + + distributive-trunc-Π-Finite-Type : + is-contr + ( Σ ( ( ║ ((x : type-Finite-Type A) → B x) ║₀) ≃ + ( (x : type-Finite-Type A) → ║ B x ║₀)) + ( λ e → + ( map-equiv e ∘ unit-trunc-Set) ~ + ( map-Π (λ x → unit-trunc-Set)))) + distributive-trunc-Π-Finite-Type = + distributive-trunc-Π-is-finite-Set H B + + equiv-distributive-trunc-Π-Finite-Type : + ║ ((x : type-Finite-Type A) → B x) ║₀ ≃ + ((x : type-Finite-Type A) → ║ B x ║₀) + equiv-distributive-trunc-Π-Finite-Type = + equiv-distributive-trunc-Π-is-finite-Set H B + + map-equiv-distributive-trunc-Π-Finite-Type : + ║ ((x : type-Finite-Type A) → B x) ║₀ → + ((x : type-Finite-Type A) → ║ B x ║₀) + map-equiv-distributive-trunc-Π-Finite-Type = + map-equiv-distributive-trunc-Π-is-finite-Set H B + + is-equiv-map-equiv-distributive-trunc-Π-Finite-Type : + is-equiv map-equiv-distributive-trunc-Π-Finite-Type + is-equiv-map-equiv-distributive-trunc-Π-Finite-Type = + is-equiv-map-equiv-distributive-trunc-Π-is-finite-Set H B + + triangle-distributive-trunc-Π-Finite-Type : + ( map-equiv-distributive-trunc-Π-Finite-Type ∘ unit-trunc-Set) ~ + ( map-Π (λ x → unit-trunc-Set)) + triangle-distributive-trunc-Π-Finite-Type = + triangle-distributive-trunc-Π-is-finite-Set H B ``` + +## See also + +- [Finite choice](univalent-combinatorics.finite-choice.md) for distributivity + of propositional truncation over finite products. +- Distributivity of set-truncation in particular means that finite sets are + [cardinality-projective](set-theory.cardinality-projective-sets.md). diff --git a/src/univalent-combinatorics/ferrers-diagrams.lagda.md b/src/univalent-combinatorics/ferrers-diagrams.lagda.md index 57d99eae92a..4d2809e13ea 100644 --- a/src/univalent-combinatorics/ferrers-diagrams.lagda.md +++ b/src/univalent-combinatorics/ferrers-diagrams.lagda.md @@ -40,7 +40,7 @@ ferrers diagram of a [finite type](univalent-combinatorics.finite-types.md) `A` consists of a finite type `X` and a family `Y` of inhabited finite types over `X` such that `Σ X Y` is merely equivalent to `A`. The number of finite Ferrers diagrams of `A` is the [partition number](univalent-combinatorics.partitions.md) -of the [cardinality](set-theory.cardinalities.md) of `A`. +of the [cardinality](set-theory.cardinals.md) of `A`. ## Definition diff --git a/src/univalent-combinatorics/finite-choice.lagda.md b/src/univalent-combinatorics/finite-choice.lagda.md index 43f0971a20d..e9d809bc9b4 100644 --- a/src/univalent-combinatorics/finite-choice.lagda.md +++ b/src/univalent-combinatorics/finite-choice.lagda.md @@ -193,3 +193,7 @@ module _ ( double-negation-type-Prop ((x : X) → Y x)) ( λ e → finite-double-negation-choice-count e H) ``` + +## See also + +- [Distributivity of set truncation over finite products](univalent-combinatorics.distributivity-of-set-truncation-over-finite-products.md) diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index 4dae49548c7..b3428795afb 100644 --- a/src/univalent-combinatorics/finite-types.lagda.md +++ b/src/univalent-combinatorics/finite-types.lagda.md @@ -450,7 +450,7 @@ abstract is-set-is-finite {l} {X} H = apply-universal-property-trunc-Prop H ( is-set-Prop X) - ( λ e → is-set-count e) + ( λ e → is-set-type-count e) is-set-type-Finite-Type : {l : Level} (X : Finite-Type l) → is-set (type-Finite-Type X) diff --git a/src/univalent-combinatorics/finitely-many-connected-components.lagda.md b/src/univalent-combinatorics/finitely-many-connected-components.lagda.md index b2d49dc3a59..b93098a62c8 100644 --- a/src/univalent-combinatorics/finitely-many-connected-components.lagda.md +++ b/src/univalent-combinatorics/finitely-many-connected-components.lagda.md @@ -214,7 +214,7 @@ has-finitely-many-connected-components-finite-Π : has-finitely-many-connected-components ((a : A) → B a) has-finitely-many-connected-components-finite-Π {B = B} H K = is-finite-equiv' - ( equiv-distributive-trunc-Π-is-finite-Set B H) + ( equiv-distributive-trunc-Π-is-finite-Set H B) ( is-finite-Π H K) ``` diff --git a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md index 7e7423d0377..d8e33ac8d4e 100644 --- a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md +++ b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md @@ -22,7 +22,9 @@ open import foundation.sets open import foundation.surjective-maps open import foundation.universe-levels -open import set-theory.cardinalities +open import set-theory.cardinals +open import set-theory.equality-cardinals +open import set-theory.inequality-cardinals open import univalent-combinatorics.dedekind-finite-sets open import univalent-combinatorics.dedekind-finite-types @@ -167,7 +169,7 @@ module _ ```agda cardinality-Kuratowski-Finite-Set : - {l : Level} → Kuratowski-Finite-Set l → cardinal l + {l : Level} → Kuratowski-Finite-Set l → Cardinal l cardinality-Kuratowski-Finite-Set X = cardinality (set-Kuratowski-Finite-Set X) @@ -177,11 +179,11 @@ module _ antisymmetric-leq-cardinality-Kuratowski-Finite-Set : leq-cardinality - ( cardinality-Kuratowski-Finite-Set X) - ( cardinality-Kuratowski-Finite-Set Y) → + ( set-Kuratowski-Finite-Set X) + ( set-Kuratowski-Finite-Set Y) → leq-cardinality - ( cardinality-Kuratowski-Finite-Set Y) - ( cardinality-Kuratowski-Finite-Set X) → + ( set-Kuratowski-Finite-Set Y) + ( set-Kuratowski-Finite-Set X) → cardinality-Kuratowski-Finite-Set X ＝ cardinality-Kuratowski-Finite-Set Y antisymmetric-leq-cardinality-Kuratowski-Finite-Set p q = diff --git a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md index adf834e7dae..9587db8e975 100644 --- a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md +++ b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md @@ -899,10 +899,16 @@ module _ ( eq-pair-Σ ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i))) + ( is-set-type-count + ( eX) + ( pr1 (two-elements-transposition eX Y)) + ( i)))) ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX (pr1 (two-elements-transposition eX Y)) j))))) ∙ + ( is-set-type-count + ( eX) + ( pr1 (two-elements-transposition eX Y)) + ( j)))))) ∙ ( r1) cases-inward-edge-left-two-elements-orientation-count i j np Y x nq nr (inr (pair r1 r2)) = @@ -928,7 +934,10 @@ module _ { y = inl r1} ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i)))) ∙ + ( is-set-type-count + ( eX) + ( pr1 (two-elements-transposition eX Y)) + ( i))))) ∙ ( r2) inward-edge-left-two-elements-orientation-count : @@ -1013,7 +1022,7 @@ module _ ( λ r → nr (inv r))))} ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -1096,7 +1105,7 @@ module _ ( eq-pair-Σ ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -1106,7 +1115,7 @@ module _ ( pr1 (two-elements-transposition eX Y))))) ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -1173,10 +1182,16 @@ module _ ( eq-pair-Σ ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i))) + ( is-set-type-count + ( eX) + ( pr1 (two-elements-transposition eX Y)) + ( i)))) ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX (pr1 (two-elements-transposition eX Y)) j))))) ∙ + ( is-set-type-count + ( eX) + ( pr1 (two-elements-transposition eX Y)) + ( j)))))) ∙ ( r1) cases-inward-edge-right-two-elements-orientation-count i j np Y x nq nr (inr (pair r1 r2)) = @@ -1205,10 +1220,15 @@ module _ ( eq-pair-Σ ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX (pr1 (two-elements-transposition eX Y)) i))) + ( is-set-type-count + ( eX) + ( pr1 (two-elements-transposition eX Y)) i))) ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX (pr1 (two-elements-transposition eX Y)) j))))) ∙ + ( is-set-type-count + ( eX) + ( pr1 (two-elements-transposition eX Y)) + ( j)))))) ∙ ( ( ap ( λ d → pr1 @@ -1225,7 +1245,7 @@ module _ { y = inr (λ q → nq (inv r2 ∙ q))} ( eq-is-prop ( is-prop-is-decidable - ( is-set-count + ( is-set-type-count ( eX) ( pr1 (pr2 (two-elements-transposition eX Y))) ( i))))) ∙ @@ -1312,7 +1332,7 @@ module _ ( λ r → nr (inv r))))} ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -1395,7 +1415,7 @@ module _ ( eq-pair-Σ ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -1405,7 +1425,7 @@ module _ ( pr1 (two-elements-transposition eX Y))))) ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -1765,7 +1785,7 @@ module _ ( R) ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -1787,8 +1807,8 @@ module _ ( has-decidable-equality-count eX x i) ( has-decidable-equality-count eX x j)} ( eq-pair-Σ - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i))) - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j)))) ∙ + ( eq-is-prop (is-prop-is-decidable (is-set-type-count eX x i))) + ( eq-is-prop (is-prop-is-decidable (is-set-type-count eX x j)))) ∙ ap ( λ k → pr1 @@ -2019,7 +2039,7 @@ module _ ( R) ( eq-is-prop ( is-prop-is-decidable - ( is-set-count eX + ( is-set-type-count eX ( map-equiv ( transposition ( standard-2-Element-Decidable-Subtype @@ -2041,8 +2061,8 @@ module _ ( has-decidable-equality-count eX x j) ( has-decidable-equality-count eX x i)} ( eq-pair-Σ - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j))) - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i)))) ∙ + ( eq-is-prop (is-prop-is-decidable (is-set-type-count eX x j))) + ( eq-is-prop (is-prop-is-decidable (is-set-type-count eX x i)))) ∙ ( ap ( λ k → pr1 @@ -2707,8 +2727,10 @@ module _ ( has-decidable-equality-count eX x j)} { y = pair (inr nq) (inr nr)} ( eq-pair-Σ - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i))) - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j)))))))) ∙ + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x i))) + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x j)))))))) ∙ ( ( is-fixed-point-standard-transposition ( has-decidable-equality-count eX) ( np) @@ -2729,8 +2751,10 @@ module _ ( has-decidable-equality-count eX x j) ( has-decidable-equality-count eX x i)} ( eq-pair-Σ - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j))) - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i))))) ∙ + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x j))) + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x i))))) ∙ ( ap ( λ k → pr1 @@ -3050,8 +3074,10 @@ module _ ( has-decidable-equality-count eX y i)) { y = pair (inr nq) (inr nr)} ( eq-pair-Σ - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i))) - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j))))) ∙ + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x i))) + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x j))))) ∙ ( ap ( λ D → cases-orientation-two-elements-count j i @@ -3066,8 +3092,10 @@ module _ ( has-decidable-equality-count eX x j) ( has-decidable-equality-count eX x i)} ( eq-pair-Σ - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x j))) - ( eq-is-prop (is-prop-is-decidable (is-set-count eX x i)))) ∙ + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x j))) + ( eq-is-prop + ( is-prop-is-decidable (is-set-type-count eX x i)))) ∙ ( ap ( λ w → cases-orientation-two-elements-count j i diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md index dc8a1e1e99a..c007d7dc831 100644 --- a/src/univalent-combinatorics/pigeonhole-principle.lagda.md +++ b/src/univalent-combinatorics/pigeonhole-principle.lagda.md @@ -205,7 +205,7 @@ module _ {f : A → B} → is-injective f → number-of-elements-count eA ≤-ℕ number-of-elements-count eB leq-is-injective-count H = - leq-is-emb-count (is-emb-is-injective (is-set-count eB) H) + leq-is-emb-count (is-emb-is-injective (is-set-type-count eB) H) ``` #### There is no embedding `A ↪ B` between types equipped with a counting if the number of elements of `B` is strictly less than the number of elements of `A` @@ -237,7 +237,7 @@ module _ number-of-elements-count eB <-ℕ number-of-elements-count eA → is-not-injective f is-not-injective-le-count f p H = - is-not-emb-le-count f p (is-emb-is-injective (is-set-count eB) H) + is-not-emb-le-count f p (is-emb-is-injective (is-set-type-count eB) H) ``` #### There is no embedding `ℕ ↪ A` into a type equipped with a counting diff --git a/src/univalent-combinatorics/retracts-of-finite-types.lagda.md b/src/univalent-combinatorics/retracts-of-finite-types.lagda.md index d7b3d888e49..497a61f0f32 100644 --- a/src/univalent-combinatorics/retracts-of-finite-types.lagda.md +++ b/src/univalent-combinatorics/retracts-of-finite-types.lagda.md @@ -64,7 +64,7 @@ abstract {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : count B) (i : A → B) → retraction i → is-emb i is-emb-retract-count e i R = - is-emb-is-injective (is-set-count e) (is-injective-retraction i R) + is-emb-is-injective (is-set-type-count e) (is-injective-retraction i R) emb-retract-count : {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : count B) (i : A → B) →