diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index f0f52a7493..449c7d2160 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -194,6 +194,7 @@ open import foundation.exponents-set-quotients public open import foundation.extensions-types public open import foundation.extensions-types-global-subuniverses public open import foundation.extensions-types-subuniverses public +open import foundation.extremally-isolated-elements public open import foundation.faithful-maps public open import foundation.families-of-equivalences public open import foundation.families-of-maps public diff --git a/src/foundation/extremally-isolated-elements.lagda.md b/src/foundation/extremally-isolated-elements.lagda.md new file mode 100644 index 0000000000..1fb8466924 --- /dev/null +++ b/src/foundation/extremally-isolated-elements.lagda.md @@ -0,0 +1,183 @@ +# Extremally isolated elements + +```agda +module foundation.extremally-isolated-elements where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.constant-maps +open import foundation.decidable-embeddings +open import foundation.decidable-equality +open import foundation.decidable-maps +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.double-negation +open import foundation.embeddings +open import foundation.fundamental-theorem-of-identity-types +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.isolated-elements +open import foundation.maybe +open import foundation.negated-equality +open import foundation.negation +open import foundation.sets +open import foundation.type-arithmetic-unit-type +open import foundation.unit-type +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.coproduct-types +open import foundation-core.decidable-propositions +open import foundation-core.empty-types +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.homotopies +open import foundation-core.propositions +open import foundation-core.subtypes +open import foundation-core.torsorial-type-families +open import foundation-core.transport-along-identifications + +open import logic.de-morgan-maps +open import logic.de-morgan-types +``` + +
+ +## Idea + +An element `a : A` is +{{#concept "extremally isolated" Agda=is-extremally-isolated Agda=extremally-extremally-isolated-element}} +if `a ＝ x` is [De Morgan](logic.de-morgan-types.md) for any `x`. I.e., if the +[proposition](foundation-core.propositions.md) `a ≠ x` is +[decidable](foundation-core.decidable-types.md). + +## Definitions + +### Extremally isolated elements + +```agda +is-extremally-isolated : + {l1 : Level} {X : UU l1} (a : X) → UU l1 +is-extremally-isolated {l1} {X} a = (x : X) → is-decidable (a ≠ x) + +extremally-isolated-element : + {l1 : Level} (X : UU l1) → UU l1 +extremally-isolated-element X = Σ X is-extremally-isolated + +module _ + {l : Level} {X : UU l} (x : extremally-isolated-element X) + where + + element-extremally-isolated-element : X + element-extremally-isolated-element = pr1 x + + is-extremally-isolated-extremally-isolated-element : + is-extremally-isolated element-extremally-isolated-element + is-extremally-isolated-extremally-isolated-element = pr2 x +``` + +### Complements of extremally isolated elements + +```agda +complement-extremally-isolated-element : + {l1 : Level} (X : UU l1) → extremally-isolated-element X → UU l1 +complement-extremally-isolated-element X x = + Σ X (λ y → element-extremally-isolated-element x ≠ y) +``` + +## Properties + +### Isolated elements are extremallly isolated + +```agda +module _ + {l1 : Level} {X : UU l1} + where + + is-extremally-isolated-is-isolated : + (x : X) → is-isolated x → is-extremally-isolated x + is-extremally-isolated-is-isolated x H y = is-de-morgan-is-decidable (H y) + + is-extremally-isolated-isolated-element : + (x : isolated-element X) → + is-extremally-isolated (element-isolated-element x) + is-extremally-isolated-isolated-element (x , H) = + is-extremally-isolated-is-isolated x H + + extremally-isolated-element-isolated-element : + isolated-element X → extremally-isolated-element X + extremally-isolated-element-isolated-element (x , H) = + (x , is-extremally-isolated-isolated-element (x , H)) +``` + +### An element is extremally isolated if and only if the constant map pointing at it is De Morgan + +```agda +module _ + {l1 : Level} {A : UU l1} (a : A) + where + + is-de-morgan-point-is-extremally-isolated : + is-extremally-isolated a → is-de-morgan-map (point a) + is-de-morgan-point-is-extremally-isolated d x = + is-de-morgan-equiv (compute-fiber-point a x) (d x) + + is-extremally-isolated-is-de-morgan-point : + is-de-morgan-map (point a) → is-extremally-isolated a + is-extremally-isolated-is-de-morgan-point d x = + is-de-morgan-equiv' (compute-fiber-point a x) (d x) +``` + +### Being an extremally isolated element is a property + +```agda +module _ + {l1 : Level} {A : UU l1} + where + + is-prop-is-extremally-isolated : (a : A) → is-prop (is-extremally-isolated a) + is-prop-is-extremally-isolated a = + is-prop-Π (λ x → is-prop-is-de-morgan (a ＝ x)) + + is-extremally-isolated-Prop : (a : A) → Prop l1 + pr1 (is-extremally-isolated-Prop a) = is-extremally-isolated a + pr2 (is-extremally-isolated-Prop a) = is-prop-is-extremally-isolated a + + inclusion-extremally-isolated-element : extremally-isolated-element A → A + inclusion-extremally-isolated-element = pr1 + + is-emb-inclusion-extremally-isolated-element : + is-emb inclusion-extremally-isolated-element + is-emb-inclusion-extremally-isolated-element = + is-emb-inclusion-subtype is-extremally-isolated-Prop + + has-decidable-equality-extremally-isolated-element : + (u v : extremally-isolated-element A) → is-decidable (u ≠ v) + has-decidable-equality-extremally-isolated-element (x , dx) (y , dy) = + is-de-morgan-equiv + ( equiv-ap-inclusion-subtype is-extremally-isolated-Prop) + ( dx y) + +module _ + {l1 : Level} {A : UU l1} (a : extremally-isolated-element A) + where + + point-extremally-isolated-element : unit → A + point-extremally-isolated-element = + point (element-extremally-isolated-element a) + + is-de-morgan-point-extremally-isolated-element : + is-de-morgan-map point-extremally-isolated-element + is-de-morgan-point-extremally-isolated-element = + is-de-morgan-point-is-extremally-isolated + ( element-extremally-isolated-element a) + ( is-extremally-isolated-extremally-isolated-element a) +``` + +## See also + +- [Isolated elements](foundation.isolated-elements.md) diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md index 2e2b319881..c6411550ea 100644 --- a/src/set-theory.lagda.md +++ b/src/set-theory.lagda.md @@ -50,6 +50,8 @@ open import set-theory.cantors-diagonal-argument public open import set-theory.cardinalities public open import set-theory.countable-sets public open import set-theory.cumulative-hierarchy public +open import set-theory.decidable-subprojections public +open import set-theory.enumerations public open import set-theory.infinite-sets public open import set-theory.russells-paradox public open import set-theory.uncountable-sets public diff --git a/src/set-theory/countable-sets.lagda.md b/src/set-theory/countable-sets.lagda.md index 2bd4f63177..5e1ca0c71f 100644 --- a/src/set-theory/countable-sets.lagda.md +++ b/src/set-theory/countable-sets.lagda.md @@ -49,6 +49,9 @@ open import foundation-core.identity-types open import lists.shifting-sequences +open import set-theory.decidable-subprojections +open import set-theory.enumerations + open import univalent-combinatorics.standard-finite-types ``` @@ -71,19 +74,18 @@ module _ {l : Level} (X : Set l) where - enumeration : UU l - enumeration = Σ (ℕ → Maybe (type-Set X)) is-surjective + enumeration-set-ℕ : UU l + enumeration-set-ℕ = enumeration ℕ (type-Set X) - map-enumeration : enumeration → (ℕ → Maybe (type-Set X)) - map-enumeration E = pr1 E + map-enumeration-set-ℕ : enumeration-set-ℕ → ℕ → Maybe (type-Set X) + map-enumeration-set-ℕ = map-enumeration - is-surjective-map-enumeration : - (E : enumeration) → is-surjective (map-enumeration E) - is-surjective-map-enumeration E = pr2 E + is-surjective-map-enumeration-set-ℕ : + (E : enumeration-set-ℕ) → is-surjective (map-enumeration-set-ℕ E) + is-surjective-map-enumeration-set-ℕ = is-surjective-map-enumeration is-countable-Prop : Prop l - is-countable-Prop = - ∃ (ℕ → Maybe (type-Set X)) (is-surjective-Prop) + is-countable-Prop = is-enumerable-Prop ℕ (type-Set X) is-countable : UU l is-countable = type-Prop (is-countable-Prop) @@ -99,18 +101,13 @@ module _ {l : Level} (X : Set l) where - decidable-subprojection-ℕ : UU (lsuc l ⊔ l) - decidable-subprojection-ℕ = - Σ ( decidable-subtype l ℕ) - ( λ P → type-decidable-subtype P ↠ type-Set X) + decidable-subprojection-set-ℕ : UU (lsuc l) + decidable-subprojection-set-ℕ = decidable-subprojection l ℕ (type-Set X) - is-countable-Prop' : Prop (lsuc l ⊔ l) - is-countable-Prop' = - exists-structure-Prop - ( decidable-subtype l ℕ) - ( λ P → type-decidable-subtype P ↠ type-Set X) + is-countable-Prop' : Prop (lsuc l) + is-countable-Prop' = is-decidable-subprojection-Prop l ℕ (type-Set X) - is-countable' : UU (lsuc l ⊔ l) + is-countable' : UU (lsuc l) is-countable' = type-Prop is-countable-Prop' is-prop-is-countable' : is-prop is-countable' @@ -124,16 +121,15 @@ surjective map `f : ℕ → X`. Let us call the latter as "directly countable". ```agda is-directly-countable-Prop : {l : Level} → Set l → Prop l -is-directly-countable-Prop X = - ∃ (ℕ → type-Set X) (is-surjective-Prop) +is-directly-countable-Prop X = is-directly-enumerable-Prop ℕ (type-Set X) is-directly-countable : {l : Level} → Set l → UU l is-directly-countable X = type-Prop (is-directly-countable-Prop X) is-prop-is-directly-countable : {l : Level} (X : Set l) → is-prop (is-directly-countable X) -is-prop-is-directly-countable X = is-prop-type-Prop - (is-directly-countable-Prop X) +is-prop-is-directly-countable X = + is-prop-type-Prop (is-directly-countable-Prop X) module _ {l : Level} (X : Set l) (a : type-Set X) @@ -141,21 +137,7 @@ module _ is-directly-countable-is-countable : is-countable X → is-directly-countable X - is-directly-countable-is-countable H = - apply-universal-property-trunc-Prop H - ( is-directly-countable-Prop X) - ( λ P → - unit-trunc-Prop - ( pair - ( f ∘ (pr1 P)) - ( is-surjective-comp is-surjective-f (pr2 P)))) - where - f : Maybe (type-Set X) → type-Set X - f (inl x) = x - f (inr star) = a - - is-surjective-f : is-surjective f - is-surjective-f x = unit-trunc-Prop (pair (inl x) refl) + is-directly-countable-is-countable = is-directly-enumerable-is-enumerable a abstract is-countable-is-directly-countable : @@ -175,7 +157,7 @@ module _ ( λ (n , p) → unit-trunc-Prop ( succ-ℕ (succ-ℕ n) , ap inl p)) - ( inr star) → unit-trunc-Prop (zero-ℕ , refl)))) + ( inr _) → unit-trunc-Prop (zero-ℕ , refl)))) ``` ## Properties @@ -189,35 +171,13 @@ module _ {l : Level} (X : Set l) where - decidable-subprojection-ℕ-enumeration : - enumeration X → decidable-subprojection-ℕ X - pr1 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n) = - f n ≠ inr star - pr1 (pr2 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n)) = - is-prop-neg - pr2 (pr2 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n)) = - is-decidable-is-not-exception-Maybe (f n) - pr1 (pr2 (decidable-subprojection-ℕ-enumeration (f , H))) (n , p) = - value-is-not-exception-Maybe (f n) p - pr2 (pr2 (decidable-subprojection-ℕ-enumeration (f , H))) x = - apply-universal-property-trunc-Prop (H (inl x)) - ( trunc-Prop (fiber _ x)) - ( λ (n , p) → - unit-trunc-Prop - ( ( n , is-not-exception-is-value-Maybe (f n) (x , inv p)) , - ( is-injective-inl - ( ( eq-is-not-exception-Maybe - ( f n) - ( is-not-exception-is-value-Maybe - ( f n) (x , inv p))) ∙ - ( p))))) - - is-countable'-is-countable : - is-countable X → is-countable' X - is-countable'-is-countable H = - apply-universal-property-trunc-Prop H - ( is-countable-Prop' X) - ( λ E → unit-trunc-Prop (decidable-subprojection-ℕ-enumeration E)) + decidable-subprojection-set-ℕ-enumeration-set-ℕ : + enumeration-set-ℕ X → decidable-subprojection-set-ℕ X + decidable-subprojection-set-ℕ-enumeration-set-ℕ = + decidable-subprojection-enumeration + + is-countable'-is-countable : is-countable X → is-countable' X + is-countable'-is-countable = is-decidable-subprojection-is-enumerable ``` Second, we will prove `is-countable' X → is-countable X`. @@ -227,7 +187,7 @@ cases-map-decidable-subtype-ℕ : {l : Level} (X : Set l) → ( P : decidable-subtype l ℕ) → ( f : type-decidable-subtype P → type-Set X) → - ( (n : ℕ) → is-decidable (pr1 (P n)) -> Maybe (type-Set X)) + ( (n : ℕ) → is-decidable (pr1 (P n)) → Maybe (type-Set X)) cases-map-decidable-subtype-ℕ X P f n (inl x) = inl (f (n , x)) cases-map-decidable-subtype-ℕ X P f n (inr x) = inr star @@ -240,8 +200,7 @@ module _ shift-decidable-subtype-ℕ : decidable-subtype l ℕ shift-decidable-subtype-ℕ zero-ℕ = ( raise-empty l) , - ( is-prop-raise-empty , - ( inr (is-empty-raise-empty))) + ( is-prop-raise-empty , inr (is-empty-raise-empty)) shift-decidable-subtype-ℕ (succ-ℕ n) = P n map-shift-decidable-subtype-ℕ : @@ -249,8 +208,8 @@ module _ map-shift-decidable-subtype-ℕ (zero-ℕ , map-raise ()) map-shift-decidable-subtype-ℕ (succ-ℕ n , p) = f (n , p) - map-enumeration-decidable-subprojection-ℕ : ℕ → Maybe (type-Set X) - map-enumeration-decidable-subprojection-ℕ n = + map-enumeration-set-ℕ-decidable-subprojection-set-ℕ : ℕ → Maybe (type-Set X) + map-enumeration-set-ℕ-decidable-subprojection-set-ℕ n = cases-map-decidable-subtype-ℕ ( X) ( shift-decidable-subtype-ℕ) @@ -259,12 +218,14 @@ module _ (pr2 (pr2 (shift-decidable-subtype-ℕ n))) abstract - is-surjective-map-enumeration-decidable-subprojection-ℕ : + is-surjective-map-enumeration-set-ℕ-decidable-subprojection-set-ℕ : ( is-surjective f) → - ( is-surjective map-enumeration-decidable-subprojection-ℕ) - is-surjective-map-enumeration-decidable-subprojection-ℕ H (inl x) = + ( is-surjective map-enumeration-set-ℕ-decidable-subprojection-set-ℕ) + is-surjective-map-enumeration-set-ℕ-decidable-subprojection-set-ℕ + H (inl x) = ( apply-universal-property-trunc-Prop (H x) - ( trunc-Prop (fiber map-enumeration-decidable-subprojection-ℕ (inl x))) + ( trunc-Prop + ( fiber map-enumeration-set-ℕ-decidable-subprojection-set-ℕ (inl x))) ( λ where ( ( n , s) , refl) → unit-trunc-Prop @@ -278,18 +239,19 @@ module _ ( is-prop-is-decidable (pr1 (pr2 (P n))) ( pr2 (pr2 (P n))) ( inl s))))))) - is-surjective-map-enumeration-decidable-subprojection-ℕ H (inr star) = + is-surjective-map-enumeration-set-ℕ-decidable-subprojection-set-ℕ + H (inr _) = ( unit-trunc-Prop (0 , refl)) module _ {l : Level} (X : Set l) where - enumeration-decidable-subprojection-ℕ : - decidable-subprojection-ℕ X → enumeration X - enumeration-decidable-subprojection-ℕ (P , (f , H)) = - ( map-enumeration-decidable-subprojection-ℕ X P f) , - ( is-surjective-map-enumeration-decidable-subprojection-ℕ X P f H) + enumeration-set-ℕ-decidable-subprojection-set-ℕ : + decidable-subprojection-set-ℕ X → enumeration-set-ℕ X + enumeration-set-ℕ-decidable-subprojection-set-ℕ (P , (f , H)) = + ( map-enumeration-set-ℕ-decidable-subprojection-set-ℕ X P f) , + ( is-surjective-map-enumeration-set-ℕ-decidable-subprojection-set-ℕ X P f H) is-countable-is-countable' : is-countable' X → is-countable X @@ -297,7 +259,7 @@ module _ apply-universal-property-trunc-Prop H ( is-countable-Prop X) ( λ D → - ( unit-trunc-Prop (enumeration-decidable-subprojection-ℕ D))) + ( unit-trunc-Prop (enumeration-set-ℕ-decidable-subprojection-set-ℕ D))) ``` ### If a countable set surjects onto a set, then the set is countable @@ -310,37 +272,30 @@ module _ is-directly-countable-is-directly-countably-indexed' : {f : type-Set A → type-Set B} → is-surjective f → is-directly-countable A → is-directly-countable B - is-directly-countable-is-directly-countably-indexed' {f} F = - elim-exists - ( is-directly-countable-Prop B) - ( λ g G → intro-exists (f ∘ g) (is-surjective-comp F G)) + is-directly-countable-is-directly-countably-indexed' = + is-directly-enumerable-is-directly-enumerably-indexed' is-directly-countable-is-directly-countably-indexed : (type-Set A ↠ type-Set B) → is-directly-countable A → is-directly-countable B - is-directly-countable-is-directly-countably-indexed (f , F) = - is-directly-countable-is-directly-countably-indexed' F + is-directly-countable-is-directly-countably-indexed = + is-directly-enumerable-is-directly-enumerably-indexed is-countable-is-countably-indexed' : {f : type-Set A → type-Set B} → is-surjective f → is-countable A → is-countable B - is-countable-is-countably-indexed' {f} F = - elim-exists - ( is-countable-Prop B) - ( λ g G → - intro-exists - ( map-Maybe f ∘ g) - ( is-surjective-comp (is-surjective-map-is-surjective-Maybe F) G)) + is-countable-is-countably-indexed' = + is-enumerable-is-enumerably-indexed' is-countable-is-countably-indexed : (type-Set A ↠ type-Set B) → is-countable A → is-countable B - is-countable-is-countably-indexed (f , F) = - is-countable-is-countably-indexed' F + is-countable-is-countably-indexed = + is-enumerable-is-enumerably-indexed ``` ### Retracts of countable sets are countable @@ -353,19 +308,11 @@ module _ is-directly-countable-retract-of : is-directly-countable A → is-directly-countable B - is-directly-countable-retract-of = - is-directly-countable-is-directly-countably-indexed' A B - { map-retraction-retract R} - ( is-surjective-has-section - ( inclusion-retract R , is-retraction-map-retraction-retract R)) + is-directly-countable-retract-of = is-directly-enumerable-retract-of R is-countable-retract-of : is-countable A → is-countable B - is-countable-retract-of = - is-countable-is-countably-indexed' A B - { map-retraction-retract R} - ( is-surjective-has-section - ( inclusion-retract R , is-retraction-map-retraction-retract R)) + is-countable-retract-of = is-enumerable-retract-of R ``` ### Countable sets are closed under equivalences @@ -398,17 +345,14 @@ abstract (succ-ℕ n) → inl n) , ( λ where ( inl n) → unit-trunc-Prop (succ-ℕ n , refl) - ( inr star) → unit-trunc-Prop (zero-ℕ , refl))) + ( inr _) → unit-trunc-Prop (zero-ℕ , refl))) ``` ### The empty set is countable ```agda is-countable-empty : is-countable empty-Set -is-countable-empty = - is-countable-is-countable' - ( empty-Set) - ( unit-trunc-Prop ((λ _ → empty-Decidable-Prop) , (λ ()) , (λ ()))) +is-countable-empty = is-enumerable-empty' 0 ``` ### The unit set is countable @@ -422,11 +366,11 @@ abstract zero-ℕ → inl star (succ-ℕ x) → inr star) , ( λ where - ( inl star) → unit-trunc-Prop (0 , refl) - ( inr star) → unit-trunc-Prop (1 , refl))) + ( inl _) → unit-trunc-Prop (0 , refl) + ( inr _) → unit-trunc-Prop (1 , refl))) ``` -### If `X` and `Y` are countable sets, then so is their coproduct `X + Y` +### Countable sets are closed under coproducts ```agda module _ @@ -450,7 +394,7 @@ module _ ( is-surjective-is-equiv (is-equiv-map-ℕ-to-ℕ+ℕ))))))) ``` -### If `X` and `Y` are countable sets, then so is their product `X × Y` +### Countable sets are closed under products ```agda module _ @@ -499,7 +443,9 @@ is-countable-ℤ = is-countable-Fin-Set : (n : ℕ) → is-countable (Fin-Set n) is-countable-Fin-Set zero-ℕ = is-countable-empty is-countable-Fin-Set (succ-ℕ n) = - is-countable-coproduct (Fin-Set n) (unit-Set) + is-countable-coproduct + ( Fin-Set n) + ( unit-Set) ( is-countable-Fin-Set n) (is-countable-unit) ``` diff --git a/src/set-theory/decidable-subprojections.lagda.md b/src/set-theory/decidable-subprojections.lagda.md new file mode 100644 index 0000000000..04b2768c4c --- /dev/null +++ b/src/set-theory/decidable-subprojections.lagda.md @@ -0,0 +1,72 @@ +# Decidable subprojections + +```agda +module set-theory.decidable-subprojections where +``` + +
Imports + +```agda +open import foundation.coproduct-types +open import foundation.decidable-subtypes +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.inhabited-types +open import foundation.maybe +open import foundation.negated-equality +open import foundation.negation +open import foundation.postcomposition-functions +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.retracts-of-types +open import foundation.surjective-maps +open import foundation.unit-type +open import foundation.universe-levels + +open import foundation-core.fibers-of-maps +open import foundation-core.identity-types + +open import logic.functoriality-existential-quantification +``` + +
+ +## Idea + +A +{{#concept "decidable subprojection" Disambiguation="of a type" Agda=decidable-subprojection}} +of a type `α` onto a type `X` is a surjection `β ↠ X` for some +[decidable subtype](foundation.decidable-subtypes.md) `β` of `α`. + +## Definition + +```agda +module _ + {l1 l2 : Level} (l3 : Level) (α : UU l1) (X : UU l2) + where + + decidable-subprojection : UU (l1 ⊔ l2 ⊔ lsuc l3) + decidable-subprojection = + Σ (decidable-subtype l3 α) (λ β → type-decidable-subtype β ↠ X) + + is-decidable-subprojection-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3) + is-decidable-subprojection-Prop = + exists-structure-Prop + ( decidable-subtype l3 α) + ( λ β → type-decidable-subtype β ↠ X) + + is-decidable-subprojection : UU (l1 ⊔ l2 ⊔ lsuc l3) + is-decidable-subprojection = type-Prop is-decidable-subprojection-Prop + + is-prop-is-decidable-subprojection : is-prop is-decidable-subprojection + is-prop-is-decidable-subprojection = + is-prop-type-Prop is-decidable-subprojection-Prop +``` + +## See also + +- [Enumerations](set-theory.enumerations.md) diff --git a/src/set-theory/enumerations-fixed-points-maybe.lagda.md b/src/set-theory/enumerations-fixed-points-maybe.lagda.md new file mode 100644 index 0000000000..3553807785 --- /dev/null +++ b/src/set-theory/enumerations-fixed-points-maybe.lagda.md @@ -0,0 +1,297 @@ +# Enumerations by fixed points of the maybe-monad + +```agda +module set-theory.enumerations-fixed-points-maybe where +``` + +
Imports + +```agda +open import elementary-number-theory.equality-natural-numbers +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.type-arithmetic-natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.functoriality-propositional-truncation +open import foundation.decidable-propositions +open import foundation.decidable-subtypes +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.isolated-elements +open import foundation.precomposition-functions +open import foundation.split-surjective-maps +open import foundation.empty-types +open import foundation.coalgebras-maybe +open import foundation.equality-coproduct-types +open import foundation.equivalences +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-coproduct-types +open import foundation.extremally-isolated-elements +open import foundation.maybe +open import foundation.negated-equality +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.raising-universe-levels +open import foundation.retracts-of-types +open import foundation.inhabited-types +open import foundation.sets +open import lists.shifting-sequences +open import foundation.surjective-maps +open import foundation.unit-type +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.fibers-of-maps +open import foundation-core.identity-types + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +Given a type `α`, recall that an `α`-[enumeration](set-theory.enumerations.md) +on another type `X` is a [surjection](foundation.surjective-maps.md) +`α ↠ Maybe X`. When `α` is a [fixed point](foundation.fixed-points.md), then +this condition is equivalent to the following + +1. There is a surjection `α ↠ X` or `X` is [empty](foundation.empty-types.md). +2. There is a [decidable subtype](foundation.decidable-subtypes.md) `β` of `α` + and a surjection `β ↠ X`. + +## Properties + +### Directly α-enumerable types are α-enumerable + +```agda + -- abstract + -- is-enumerable-is-directly-enumerable : + -- (α ≃ Maybe α) → is-directly-enumerable α X → is-enumerable α X + -- is-enumerable-is-directly-enumerable μ H = + -- apply-universal-property-trunc-Prop H + -- ( is-enumerable-Prop α X) + -- ( λ (f , F) → + -- unit-trunc-Prop + -- ( ( λ i → + -- map-coproduct + -- ( λ np → rec-coproduct f (point x₀) (map-equiv μ i)) + -- ( λ nnp → star) + -- ( is-decidable-is-not-exception-Maybe (map-equiv μ i))) , + -- λ where + -- (inl x) → {! !} + -- (inr _) → + -- unit-trunc-Prop + -- ( map-inv-equiv μ exception-Maybe , + -- ( equational-reasoning + -- {! map-coproduct (λ np → rec-coproduct f (λ x₁ → x₀) (pr1 μ (map-inv-equiv μ (inr star)))) (λ nnp → star) (is-decidable-is-not-exception-Maybe (pr1 μ (map-inv-equiv μ (inr star)))) !} + -- ＝ {! !} by {! !} + -- ＝ inr x by {! !})))) + -- -- -- ( ( λ where + -- -- -- zero → inr star + -- -- -- (succ n) → inl ((shift a (pr1 P)) n)) , + -- -- ( λ where + -- -- ( inl x) → + -- -- apply-universal-property-trunc-Prop (pr2 P x) + -- -- ( trunc-Prop (fiber _ (inl x))) + -- -- ( λ (n , p) → + -- -- unit-trunc-Prop ?) + -- -- -- ( succ (succ n) , ap inl p)) + -- -- ( inr star) → unit-trunc-Prop (zero , refl)))) +``` + +### The two definitions of α-enumeration are equivalent + +First, we will prove `enumeration α X → decidable-subprojection l2 α X`. + +```agda +module _ + {l1 l2 : Level} {α : UU l1} {X : UU l2} + where + + decidable-subprojection-enumeration : + enumeration α X → decidable-subprojection l2 α X + pr1 (pr1 (decidable-subprojection-enumeration (f , H)) n) = + f n ≠ inr star + pr1 (pr2 (pr1 (decidable-subprojection-enumeration (f , H)) n)) = + is-prop-neg + pr2 (pr2 (pr1 (decidable-subprojection-enumeration (f , H)) n)) = + is-decidable-is-not-exception-Maybe (f n) + pr1 (pr2 (decidable-subprojection-enumeration (f , H))) (n , p) = + value-is-not-exception-Maybe (f n) p + pr2 (pr2 (decidable-subprojection-enumeration (f , H))) x = + apply-universal-property-trunc-Prop (H (inl x)) + ( trunc-Prop (fiber _ x)) + ( λ (n , p) → + unit-trunc-Prop + ( ( n , is-not-exception-is-value-Maybe (f n) (x , inv p)) , + ( is-injective-inl + ( ( eq-is-not-exception-Maybe + ( f n) + ( is-not-exception-is-value-Maybe + ( f n) (x , inv p))) ∙ + ( p))))) + + is-enumerable'-is-enumerable : + is-enumerable α X → is-enumerable' l2 α X + is-enumerable'-is-enumerable H = + apply-universal-property-trunc-Prop H + ( is-enumerable-Prop' l2 α X) + ( unit-trunc-Prop ∘ decidable-subprojection-enumeration) +``` + +Second, we prove `decidable-subprojection l2 α X → enumeration α X`, assuming +that α is a fixed point of the `Maybe` monad. + +```agda +cases-map-decidable-subtype : + {l1 l2 : Level} (α : UU l1) (X : UU l2) → + ( P : decidable-subtype l2 α) → + ( f : type-decidable-subtype P → X) → + ( (n : α) → is-decidable (pr1 (P n)) → Maybe X) +cases-map-decidable-subtype α X P f n (inl x) = inl (f (n , x)) +cases-map-decidable-subtype α X P f n (inr x) = inr star + +-- module _ +-- {l1 l2 : Level} (α : UU l1) +-- (M : coalgebra-structure-Maybe α) +-- (X : UU l2) +-- (P : decidable-subtype l2 α) +-- (f : type-decidable-subtype P → X) +-- where + +-- shift-decidable-subtype : decidable-subtype l2 α +-- shift-decidable-subtype = {! !} + -- shift-decidable-subtype zero = + -- ( raise-empty l2) , + -- ( is-prop-raise-empty , inr (is-empty-raise-empty)) + -- shift-decidable-subtype (succ n) = P n + +-- map-shift-decidable-subtype : +-- type-decidable-subtype shift-decidable-subtype → X +-- map-shift-decidable-subtype (zero , map-raise ()) +-- map-shift-decidable-subtype (succ n , p) = f (n , p) + +-- map-enumeration-decidable-subprojection : α → Maybe X +-- map-enumeration-decidable-subprojection n = +-- cases-map-decidable-subtype +-- ( X) +-- ( shift-decidable-subtype) +-- ( map-shift-decidable-subtype) +-- ( n) +-- (pr2 (pr2 (shift-decidable-subtype n))) + +-- abstract +-- is-surjective-map-enumeration-decidable-subprojection : +-- ( is-surjective f) → +-- ( is-surjective map-enumeration-decidable-subprojection) +-- is-surjective-map-enumeration-decidable-subprojection H (inl x) = +-- ( apply-universal-property-trunc-Prop (H x) +-- ( trunc-Prop (fiber map-enumeration-decidable-subprojection (inl x))) +-- ( λ where +-- ( ( n , s) , refl) → +-- unit-trunc-Prop +-- ( ( succ n) , +-- ( ap +-- ( cases-map-decidable-subtype X +-- ( shift-decidable-subtype) +-- ( map-shift-decidable-subtype) +-- (succ n)) +-- ( pr1 +-- ( is-prop-is-decidable (pr1 (pr2 (P n))) +-- ( pr2 (pr2 (P n))) +-- ( inl s))))))) +-- is-surjective-map-enumeration-decidable-subprojection H (inr star) = +-- ( unit-trunc-Prop (0 , refl)) + +-- module _ +-- {l : Level} (X : Set l) +-- where + +-- enumeration-decidable-subprojection : +-- decidable-subprojection X → enumeration X +-- enumeration-decidable-subprojection (P , (f , H)) = +-- ( map-enumeration-decidable-subprojection X P f) , +-- ( is-surjective-map-enumeration-decidable-subprojection X P f H) + +-- is-enumerable-is-enumerable' : +-- is-enumerable' X → is-enumerable X +-- is-enumerable-is-enumerable' H = +-- apply-universal-property-trunc-Prop H +-- ( is-enumerable-Prop X) +-- ( λ D → +-- ( unit-trunc-Prop (enumeration-decidable-subprojection D))) +``` + +### The type α is α-enumerable when α is a `Maybe`-fixed point + +```text +abstract + is-enumerable : is-enumerable α α + is-enumerable = + unit-trunc-Prop + ( ( λ where + zero → inr star + (succ n) → inl n) , + ( λ where + ( inl n) → unit-trunc-Prop (succ n , refl) + ( inr star) → unit-trunc-Prop (zero , refl))) +``` + +### Enumerable types are closed under coproducts + +```text +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + is-enumerable-coproduct : + is-enumerable X → is-enumerable Y → is-enumerable (coproduct-Set X Y) + is-enumerable-coproduct H H' = + apply-twice-universal-property-trunc-Prop H' H + ( is-enumerable-Prop (coproduct-Set X Y)) + ( λ h' h → + ( unit-trunc-Prop + ( pair + ( map-maybe-coproduct ∘ + ( map-coproduct (pr1 h) (pr1 h') ∘ map-to+α)) + ( is-surjective-comp + ( is-surjective-map-maybe-coproduct) + ( is-surjective-comp + ( is-surjective-map-coproduct (pr2 h) (pr2 h')) + ( is-surjective-is-equiv (is-equiv-map-to+α))))))) +``` + +### Enumerable types are closed under products + +```text +module _ + {l1 l2 : Level} (X : Set l1) (Y : Set l2) + where + + is-enumerable-product : + is-enumerable X → is-enumerable Y → is-enumerable (product-Set X Y) + is-enumerable-product H H' = + apply-twice-universal-property-trunc-Prop H' H + ( is-enumerable-Prop (product-Set X Y)) + ( λ h' h → + ( unit-trunc-Prop + ( pair + ( map-maybe-product ∘ + ( map-product (pr1 h) (pr1 h') ∘ map-to-ℕ×ℕ)) + ( is-surjective-comp + ( is-surjective-map-maybe-product) + ( is-surjective-comp + ( is-surjective-map-product (pr2 h) (pr2 h')) + ( is-surjective-is-equiv (is-equiv-map-to-ℕ×ℕ))))))) +``` + +### Countable types are enumerable + +> TODO: use that ℕ is the least fixed point of `Maybe`. diff --git a/src/set-theory/enumerations.lagda.md b/src/set-theory/enumerations.lagda.md new file mode 100644 index 0000000000..da74d5955f --- /dev/null +++ b/src/set-theory/enumerations.lagda.md @@ -0,0 +1,281 @@ +# Enumerations of types + +```agda +module set-theory.enumerations where +``` + +
Imports + +```agda +open import foundation.coproduct-types +open import foundation.decidable-subtypes +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.inhabited-types +open import foundation.maybe +open import foundation.negated-equality +open import foundation.negation +open import foundation.postcomposition-functions +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.retracts-of-types +open import foundation.surjective-maps +open import foundation.unit-type +open import foundation.universe-levels + +open import foundation-core.fibers-of-maps +open import foundation-core.identity-types + +open import logic.functoriality-existential-quantification + +open import set-theory.decidable-subprojections +``` + +
+ +## Idea + +Given a type `α`, a type `X` is said to be +`α`-{{#concept "enumerated" Disambiguation="type" Agda=enumeration}} if there is +a [surjective map](foundation.surjective-maps.md) `α ↠ 1 + X`. + +A type `X` is +`α`-{{#concept "enumerable" Disambiguation="type" Agda=is-enumerable}} if there +[exists](foundation.existential-quantification.md) an `α`-enumeration of `X`. + +If `α` and `X` are [discrete types](foundation.discrete-types.md), then `X` is +`α`-enumerated if and only if `X` is a +[retract](foundation.retracts-of-types.md) of `α` or +[empty](foundation-core.empty-types.md). + +## Definitions + +### The type of α-enumerations of X + +```agda +enumeration : {l1 l2 : Level} (α : UU l1) (X : UU l2) → UU (l1 ⊔ l2) +enumeration α X = (α ↠ Maybe X) + +module _ + {l1 l2 : Level} {α : UU l1} {X : UU l2} (E : enumeration α X) + where + + map-enumeration : α → Maybe X + map-enumeration = pr1 E + + is-surjective-map-enumeration : is-surjective map-enumeration + is-surjective-map-enumeration = pr2 E +``` + +### The type of α-enumerations + +```agda +enumerations : {l1 : Level} (l2 : Level) (α : UU l1) → UU (l1 ⊔ lsuc l2) +enumerations l2 α = Σ (UU l2) (λ X → (α ↠ Maybe X)) +``` + +### The predicate of being α-enumerable + +```agda +module _ + {l1 l2 : Level} (α : UU l1) (X : UU l2) + where + + is-enumerable : UU (l1 ⊔ l2) + is-enumerable = ║ enumeration α X ║₋₁ + + is-prop-is-enumberable : is-prop is-enumerable + is-prop-is-enumberable = is-prop-type-trunc-Prop + + is-enumerable-Prop : Prop (l1 ⊔ l2) + is-enumerable-Prop = trunc-Prop (enumeration α X) +``` + +### Direct α-enumerability + +A type `X` is {{#concept "directly α-enumerable" Agda=is-directly-enumerable}} +if there is a surjective map `α ↠ X`. + +```agda +is-directly-enumerable-Prop : {l1 l2 : Level} → UU l1 → UU l2 → Prop (l1 ⊔ l2) +is-directly-enumerable-Prop α X = ∃ (α → X) (is-surjective-Prop) + +is-directly-enumerable : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +is-directly-enumerable α X = type-Prop (is-directly-enumerable-Prop α X) + +is-prop-is-directly-enumerable : + {l1 l2 : Level} (α : UU l1) (X : UU l2) → is-prop (is-directly-enumerable α X) +is-prop-is-directly-enumerable α X = + is-prop-type-Prop (is-directly-enumerable-Prop α X) + +module _ + {l1 l2 : Level} {α : UU l1} {X : UU l2} (x₀ : X) + where + + is-directly-enumerable-is-enumerable : + is-enumerable α X → is-directly-enumerable α X + is-directly-enumerable-is-enumerable H = + apply-universal-property-trunc-Prop H + ( is-directly-enumerable-Prop α X) + ( λ P → + unit-trunc-Prop + ( f ∘ pr1 P , is-surjective-comp is-surjective-f (pr2 P))) + where + f : Maybe X → X + f (inl x) = x + f (inr _) = x₀ + + is-surjective-f : is-surjective f + is-surjective-f x = unit-trunc-Prop (inl x , refl) +``` + +For the converse, we need a shifting structure `α ≃ Maybe α`. See +[enumerations by fixed points of the maybe-monad](set-theory.enumerations-fixed-points-maybe.md). + +## Properties + +### If X has an α-enumeration then X is a decidable subprojection of α + +```agda +module _ + {l1 l2 : Level} {α : UU l1} {X : UU l2} + where + + decidable-subprojection-enumeration : + enumeration α X → decidable-subprojection l2 α X + pr1 (pr1 (decidable-subprojection-enumeration (f , H)) n) = + f n ≠ inr star + pr1 (pr2 (pr1 (decidable-subprojection-enumeration (f , H)) n)) = + is-prop-neg + pr2 (pr2 (pr1 (decidable-subprojection-enumeration (f , H)) n)) = + is-decidable-is-not-exception-Maybe (f n) + pr1 (pr2 (decidable-subprojection-enumeration (f , H))) (n , p) = + value-is-not-exception-Maybe (f n) p + pr2 (pr2 (decidable-subprojection-enumeration (f , H))) x = + map-trunc-Prop + ( λ (n , p) → + ( n , is-not-exception-is-value-Maybe (f n) (x , inv p)) , + ( is-injective-inl + ( ( eq-is-not-exception-Maybe + ( f n) + ( is-not-exception-is-value-Maybe (f n) (x , inv p))) ∙ + ( p)))) + ( H (inl x)) + + is-decidable-subprojection-is-enumerable : + is-enumerable α X → is-decidable-subprojection l2 α X + is-decidable-subprojection-is-enumerable H = + apply-universal-property-trunc-Prop H + ( is-decidable-subprojection-Prop l2 α X) + ( unit-trunc-Prop ∘ decidable-subprojection-enumeration) +``` + +### α-enumerations transfer along covers + +```agda +module _ + {l1 l2 l3 : Level} {α : UU l1} {A : UU l2} {B : UU l3} + where + + is-directly-enumerable-is-directly-enumerably-indexed' : + {f : A → B} → is-surjective f → + is-directly-enumerable α A → is-directly-enumerable α B + is-directly-enumerable-is-directly-enumerably-indexed' {f} F = + map-exists (is-surjective) (postcomp α f) (λ _ → is-surjective-comp F) + + is-directly-enumerable-is-directly-enumerably-indexed : + (A ↠ B) → is-directly-enumerable α A → is-directly-enumerable α B + is-directly-enumerable-is-directly-enumerably-indexed (f , F) = + is-directly-enumerable-is-directly-enumerably-indexed' F + + is-enumerable-is-enumerably-indexed' : + {f : A → B} → is-surjective f → is-enumerable α A → is-enumerable α B + is-enumerable-is-enumerably-indexed' {f} F = + map-exists + ( is-surjective) + ( postcomp α (map-Maybe f)) + ( λ _ → is-surjective-comp (is-surjective-map-is-surjective-Maybe F)) + + is-enumerable-is-enumerably-indexed : + (A ↠ B) → is-enumerable α A → is-enumerable α B + is-enumerable-is-enumerably-indexed (f , F) = + is-enumerable-is-enumerably-indexed' F +``` + +### Retracts of α-enumerable types are α-enumerable + +```agda +module _ + {l1 l2 l3 : Level} {α : UU l1} {A : UU l2} {B : UU l3} (R : B retract-of A) + where + + is-directly-enumerable-retract-of : + is-directly-enumerable α A → is-directly-enumerable α B + is-directly-enumerable-retract-of = + is-directly-enumerable-is-directly-enumerably-indexed' + { f = map-retraction-retract R} + ( is-surjective-has-section + ( inclusion-retract R , is-retraction-map-retraction-retract R)) + + is-enumerable-retract-of : + is-enumerable α A → is-enumerable α B + is-enumerable-retract-of = + is-enumerable-is-enumerably-indexed' + { f = map-retraction-retract R} + ( is-surjective-has-section + ( inclusion-retract R , is-retraction-map-retraction-retract R)) +``` + +### α-enumerable types are closed under equivalences + +```agda +module _ + {l1 l2 l3 : Level} {α : UU l1} {A : UU l2} {B : UU l3} (e : B ≃ A) + where + + is-directly-enumerable-equiv : + is-directly-enumerable α A → is-directly-enumerable α B + is-directly-enumerable-equiv = + is-directly-enumerable-retract-of (retract-equiv e) + + is-enumerable-equiv : + is-enumerable α A → is-enumerable α B + is-enumerable-equiv = + is-enumerable-retract-of (retract-equiv e) +``` + +### The empty type is α-enumerable iff α is inhabited + +```agda +module _ + {l : Level} {α : UU l} + where + + enumeration-emtpy : is-inhabited α → enumeration α empty + enumeration-emtpy |x₀| = + ( ( λ _ → exception-Maybe) , + ( λ where (inr _) → map-trunc-Prop (_, refl) |x₀|)) + + is-enumerable-empty : is-inhabited α → is-enumerable α empty + is-enumerable-empty |x₀| = + unit-trunc-Prop ( enumeration-emtpy |x₀|) + + is-enumerable-empty' : α → is-enumerable α empty + is-enumerable-empty' x₀ = is-enumerable-empty (unit-trunc-Prop x₀) + + is-inhabited-enumeration-empty : enumeration α empty → is-inhabited α + is-inhabited-enumeration-empty (f , H) = + map-trunc-Prop pr1 (H exception-Maybe) + + is-inhabited-is-enumerable-empty : is-enumerable α empty → is-inhabited α + is-inhabited-is-enumerable-empty = + rec-trunc-Prop (is-inhabited-Prop α) is-inhabited-enumeration-empty +``` + +## See also + +- [Enumerations by fixed points of the maybe-monad](set-theory.enumerations-fixed-points-maybe.md)