diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 2c2aff28b8..0f9dde78f7 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -8,6 +8,7 @@ module foundation.surjective-maps where ```agda open import foundation.action-on-identifications-functions +open import foundation.coinhabited-pairs-of-types open import foundation.connected-maps open import foundation.contractible-types open import foundation.dependent-pair-types @@ -248,6 +249,21 @@ abstract rec-trunc-Prop empty-Prop (¬A ∘ pr1) (is-surjective-map-surjection A↠B b) ``` +### If a type `A` has a surjection into `B`, `A` and `B` are coinhabited + +```agda +abstract + is-coinhabited-surjection : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → A ↠ B → is-coinhabited A B + pr1 (is-coinhabited-surjection A↠B) = map-is-inhabited (map-surjection A↠B) + pr2 (is-coinhabited-surjection A↠B) |B| = + let open do-syntax-trunc-Prop (is-inhabited-Prop _) + in do + b ← |B| + (a , fa=b) ← is-surjective-map-surjection A↠B b + unit-trunc-Prop a +``` + ### Any split surjective map is surjective ```agda diff --git a/src/logic/propositionally-decidable-types.lagda.md b/src/logic/propositionally-decidable-types.lagda.md index f8496f687d..62d7e2dc16 100644 --- a/src/logic/propositionally-decidable-types.lagda.md +++ b/src/logic/propositionally-decidable-types.lagda.md @@ -19,6 +19,7 @@ open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations open import foundation.retracts-of-types +open import foundation.surjective-maps open import foundation.universe-levels open import foundation-core.cartesian-product-types @@ -170,6 +171,26 @@ module _ is-inhabited-or-empty-iff' e , is-inhabited-or-empty-iff' (inv-iff e) ``` +### Propositionally decidable types are closed under surjections + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + abstract + is-inhabited-or-empty-surjection : + (A ↠ B) → is-inhabited-or-empty A → is-inhabited-or-empty B + is-inhabited-or-empty-surjection A↠B = + is-inhabited-or-empty-is-coinhabited (is-coinhabited-surjection A↠B) + + is-inhabited-or-empty-surjection' : + (A ↠ B) → is-inhabited-or-empty B → is-inhabited-or-empty A + is-inhabited-or-empty-surjection' A↠B = + is-inhabited-or-empty-is-coinhabited + ( is-symmetric-is-coinhabited (is-coinhabited-surjection A↠B)) +``` + ### Propositionally decidable types are closed under retracts ```agda diff --git a/src/metric-spaces/approximations-metric-spaces.lagda.md b/src/metric-spaces/approximations-metric-spaces.lagda.md index bdafb94abc..9fd8695105 100644 --- a/src/metric-spaces/approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/approximations-metric-spaces.lagda.md @@ -10,10 +10,12 @@ module metric-spaces.approximations-metric-spaces where open import elementary-number-theory.positive-rational-numbers open import foundation.cartesian-products-subtypes +open import foundation.coinhabited-pairs-of-types open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.full-subtypes open import foundation.function-types +open import foundation.functoriality-propositional-truncation open import foundation.images open import foundation.images-subtypes open import foundation.inhabited-subtypes @@ -93,6 +95,11 @@ module _ type-approximation-Metric-Space = type-subtype subset-approximation-Metric-Space + inclusion-approximation-Metric-Space : + type-approximation-Metric-Space → type-Metric-Space X + inclusion-approximation-Metric-Space = + inclusion-subtype subset-approximation-Metric-Space + is-approximation-approximation-Metric-Space : is-approximation-Metric-Space X ε subset-approximation-Metric-Space is-approximation-approximation-Metric-Space = pr2 S @@ -243,24 +250,31 @@ module _ is-approximation-im-isometric-equiv-approximation-Metric-Space) ``` -### If a metric space is inhabited, so is any approximation +### A metric space and any approximation of it are coinhabited + +A metric space is inhabited if and only if any approximation of it is inhabited. ```agda module _ - {l1 l2 l3 : Level} - (X : Metric-Space l1 l2) (|X| : is-inhabited (type-Metric-Space X)) - (ε : ℚ⁺) (S : subset-Metric-Space l3 X) + {l1 l2 l3 : Level} (X : Metric-Space l1 l2) (ε : ℚ⁺) + (S : approximation-Metric-Space l3 X ε) where abstract - is-inhabited-is-approximation-inhabited-Metric-Space : - is-approximation-Metric-Space X ε S → - is-inhabited-subtype S - is-inhabited-is-approximation-inhabited-Metric-Space is-approx = - let open do-syntax-trunc-Prop (is-inhabited-subtype-Prop S) + is-coinhabited-approximation-Metric-Space : + is-coinhabited + ( type-approximation-Metric-Space X ε S) + ( type-Metric-Space X) + pr1 is-coinhabited-approximation-Metric-Space = + map-is-inhabited (inclusion-approximation-Metric-Space X ε S) + pr2 is-coinhabited-approximation-Metric-Space |X| = + let + open + do-syntax-trunc-Prop + ( is-inhabited-Prop (type-approximation-Metric-Space X ε S)) in do x ← |X| - (s , Nεsx) ← is-approx x + (s , _) ← is-approximation-approximation-Metric-Space X ε S x unit-trunc-Prop s ``` diff --git a/src/metric-spaces/inhabited-totally-bounded-subspaces-metric-spaces.lagda.md b/src/metric-spaces/inhabited-totally-bounded-subspaces-metric-spaces.lagda.md index 19a7eefb41..04ab52fb2e 100644 --- a/src/metric-spaces/inhabited-totally-bounded-subspaces-metric-spaces.lagda.md +++ b/src/metric-spaces/inhabited-totally-bounded-subspaces-metric-spaces.lagda.md @@ -7,6 +7,8 @@ module metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces where
Imports ```agda +open import elementary-number-theory.positive-rational-numbers + open import foundation.cartesian-products-subtypes open import foundation.dependent-pair-types open import foundation.equivalences @@ -15,10 +17,14 @@ open import foundation.images open import foundation.images-subtypes open import foundation.inhabited-subtypes open import foundation.inhabited-types +open import foundation.propositional-truncations open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.metric-spaces +open import metric-spaces.nets-metric-spaces open import metric-spaces.subspaces-metric-spaces open import metric-spaces.totally-bounded-metric-spaces open import metric-spaces.totally-bounded-subspaces-metric-spaces @@ -135,3 +141,25 @@ product-inhabited-totally-bounded-subspace-Metric-Space ( subset-totally-bounded-subspace-Metric-Space Y T))) ( is-inhabited-Σ |S| (λ _ → |T|))) ``` + +### It is decidable whether or not a totally bounded subspace of a metric space is inhabited + +```agda +module _ + {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) + (S : totally-bounded-subspace-Metric-Space l3 l4 X) + where + + abstract + is-inhabited-or-empty-totally-bounded-subspace-Metric-Space : + is-inhabited-or-empty (type-totally-bounded-subspace-Metric-Space X S) + is-inhabited-or-empty-totally-bounded-subspace-Metric-Space = + rec-trunc-Prop + ( is-inhabited-or-empty-Prop _) + ( λ M → + is-inhabited-or-empty-type-is-inhabited-or-empty-net-Metric-Space + ( subspace-totally-bounded-subspace-Metric-Space X S) + ( one-ℚ⁺) + ( M one-ℚ⁺)) + ( is-totally-bounded-subspace-totally-bounded-subspace-Metric-Space X S) +``` diff --git a/src/metric-spaces/nets-metric-spaces.lagda.md b/src/metric-spaces/nets-metric-spaces.lagda.md index cff36edfd5..da1b4d0142 100644 --- a/src/metric-spaces/nets-metric-spaces.lagda.md +++ b/src/metric-spaces/nets-metric-spaces.lagda.md @@ -9,13 +9,17 @@ module metric-spaces.nets-metric-spaces where ```agda open import elementary-number-theory.positive-rational-numbers +open import foundation.coinhabited-pairs-of-types open import foundation.dependent-pair-types open import foundation.images open import foundation.inhabited-types +open import foundation.logical-equivalences open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import metric-spaces.approximations-metric-spaces open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.equality-of-metric-spaces @@ -33,6 +37,7 @@ open import metric-spaces.uniformly-continuous-functions-metric-spaces open import univalent-combinatorics.finitely-enumerable-subtypes open import univalent-combinatorics.finitely-enumerable-types open import univalent-combinatorics.inhabited-finitely-enumerable-subtypes +open import univalent-combinatorics.inhabited-finitely-enumerable-types ```
@@ -80,6 +85,14 @@ module _ subtype-finitely-enumerable-subtype ( finitely-enumerable-subset-net-Metric-Space) + type-net-Metric-Space : UU (l1 ⊔ l3) + type-net-Metric-Space = type-subtype subset-net-Metric-Space + + finitely-enumerable-type-net-Metric-Space : Finitely-Enumerable-Type (l1 ⊔ l3) + finitely-enumerable-type-net-Metric-Space = + finitely-enumerable-type-finitely-enumerable-subtype + ( finitely-enumerable-subset-net-Metric-Space) + is-approximation-subset-net-Metric-Space : is-approximation-Metric-Space X ε subset-net-Metric-Space is-approximation-subset-net-Metric-Space = pr2 N @@ -90,28 +103,61 @@ module _ is-approximation-subset-net-Metric-Space) ``` -### If a metric space is inhabited, so is any net on it +### A metric space and any net for it are coinhabited + +A metric space is inhabited if and only if any net for it is inhabited. ```agda module _ {l1 l2 l3 : Level} - (X : Metric-Space l1 l2) (|X| : is-inhabited (type-Metric-Space X)) - (ε : ℚ⁺) (S : net-Metric-Space l3 X ε) + (X : Metric-Space l1 l2) (ε : ℚ⁺) (S : net-Metric-Space l3 X ε) where abstract - is-inhabited-net-inhabited-Metric-Space : - is-inhabited-finitely-enumerable-subtype (pr1 S) - is-inhabited-net-inhabited-Metric-Space = - is-inhabited-is-approximation-inhabited-Metric-Space X |X| ε - ( subset-net-Metric-Space X ε S) - ( is-approximation-subset-net-Metric-Space X ε S) - - inhabited-finitely-enumerable-subtype-net-Metric-Space : + is-coinhabited-net-Metric-Space : + is-coinhabited (type-net-Metric-Space X ε S) (type-Metric-Space X) + is-coinhabited-net-Metric-Space = + is-coinhabited-approximation-Metric-Space + ( X) + ( ε) + ( approximation-net-Metric-Space X ε S) + + is-inhabited-type-is-inhabited-net-Metric-Space : + is-inhabited (type-net-Metric-Space X ε S) → + is-inhabited (type-Metric-Space X) + is-inhabited-type-is-inhabited-net-Metric-Space = + forward-implication is-coinhabited-net-Metric-Space + + is-inhabited-net-is-inhabited-type-Metric-Space : + is-inhabited (type-Metric-Space X) → + is-inhabited (type-net-Metric-Space X ε S) + is-inhabited-net-is-inhabited-type-Metric-Space = + backward-implication is-coinhabited-net-Metric-Space + + inhabited-finitely-enumerable-subset-net-is-inhabited-Metric-Space : + is-inhabited (type-Metric-Space X) → inhabited-finitely-enumerable-subtype l3 (type-Metric-Space X) - inhabited-finitely-enumerable-subtype-net-Metric-Space = + inhabited-finitely-enumerable-subset-net-is-inhabited-Metric-Space |S| = ( finitely-enumerable-subset-net-Metric-Space X ε S , - is-inhabited-net-inhabited-Metric-Space) + is-inhabited-net-is-inhabited-type-Metric-Space |S|) +``` + +### Given any net for a metric space `X`, `X` is propositionally decidable + +```agda +module _ + {l1 l2 l3 : Level} + (X : Metric-Space l1 l2) (ε : ℚ⁺) (S : net-Metric-Space l3 X ε) + where + + abstract + is-inhabited-or-empty-type-is-inhabited-or-empty-net-Metric-Space : + is-inhabited-or-empty (type-Metric-Space X) + is-inhabited-or-empty-type-is-inhabited-or-empty-net-Metric-Space = + is-inhabited-or-empty-is-coinhabited + ( is-coinhabited-net-Metric-Space X ε S) + ( is-inhabited-or-empty-type-Finitely-Enumerable-Type + ( finitely-enumerable-type-net-Metric-Space X ε S)) ``` ## Properties diff --git a/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md b/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md index 8e0bf879be..0549a21316 100644 --- a/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md +++ b/src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md @@ -19,7 +19,6 @@ open import foundation.function-types open import foundation.identity-types open import foundation.images open import foundation.inhabited-subtypes -open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.propositions @@ -27,6 +26,8 @@ open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import metric-spaces.approximations-metric-spaces open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces open import metric-spaces.metric-spaces @@ -155,8 +156,11 @@ module _ net δ = im-inhabited-finitely-enumerable-subtype ( inclusion-subset-ℝ S) - ( inhabited-finitely-enumerable-subtype-net-Metric-Space - ( metric-space-subset-ℝ S) |S| δ (M δ)) + ( inhabited-finitely-enumerable-subset-net-is-inhabited-Metric-Space + ( metric-space-subset-ℝ S) + ( δ) + ( M δ) + ( |S|)) is-net : (δ : ℚ⁺) → @@ -399,6 +403,23 @@ module _ is-infimum-inf-inhabited-totally-bounded-subset-ℝ) ``` +### Any totally bounded subset of `ℝ` is propositionally decidable + +```agda +module _ + {l1 l2 l3 : Level} + (S : totally-bounded-subset-ℝ l1 l2 l3) + where + + abstract + is-inhabited-or-empty-totally-bounded-subset-ℝ : + is-inhabited-or-empty (type-totally-bounded-subset-ℝ S) + is-inhabited-or-empty-totally-bounded-subset-ℝ = + is-inhabited-or-empty-totally-bounded-subspace-Metric-Space + ( metric-space-ℝ l2) + ( S) +``` + ### The infimum of an inhabited totally bounded subset of `ℝ` is less than or equal to the supremum ```agda diff --git a/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md b/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md index ca4c8a30d9..3f060650bf 100644 --- a/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md +++ b/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md @@ -67,8 +67,7 @@ module _ subset-totally-bounded-subset-ℝ = pr1 S type-totally-bounded-subset-ℝ : UU (l1 ⊔ lsuc l2) - type-totally-bounded-subset-ℝ = - type-subtype subset-totally-bounded-subset-ℝ + type-totally-bounded-subset-ℝ = type-subtype subset-totally-bounded-subset-ℝ metric-space-totally-bounded-subset-ℝ : Metric-Space (l1 ⊔ lsuc l2) l2 metric-space-totally-bounded-subset-ℝ = diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index b4bb6e56ed..4dae49548c 100644 --- a/src/univalent-combinatorics/finite-types.lagda.md +++ b/src/univalent-combinatorics/finite-types.lagda.md @@ -766,6 +766,23 @@ abstract ( pr2 (has-finite-cardinality-is-finite H))) ``` +### The finite types are propositionally decidable + +```agda +module _ + {l : Level} (X : Finite-Type l) + where + + is-inhabited-or-empty-type-Finite-Type : + is-inhabited-or-empty (type-Finite-Type X) + is-inhabited-or-empty-type-Finite-Type = + rec-trunc-Prop + ( is-inhabited-or-empty-Prop (type-Finite-Type X)) + ( λ (n , Fin-n≃X) → + is-inhabited-or-empty-equiv' Fin-n≃X (is-inhabited-or-empty-Fin n)) + ( is-finite-type-Finite-Type X) +``` + ## External links - [Finiteness in Sheaf Topoi](https://grossack.site/2024/08/19/finiteness-in-sheaf-topoi), diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index a6ad4309bb..c042e396b2 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -7,6 +7,7 @@ module univalent-combinatorics.finitely-enumerable-types where
Imports ```agda +open import elementary-number-theory.equality-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers @@ -42,6 +43,7 @@ open import foundation.unit-type open import foundation.universe-levels open import logic.functoriality-existential-quantification +open import logic.propositionally-decidable-types open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.coproduct-types @@ -419,6 +421,26 @@ module _ is-finitely-enumerable-im-Finitely-Enumerable-Type) ``` +### The finitely enumerable types are propositionally decidable + +```agda +module _ + {l : Level} (X : Finitely-Enumerable-Type l) + where + + abstract + is-inhabited-or-empty-type-Finitely-Enumerable-Type : + is-inhabited-or-empty (type-Finitely-Enumerable-Type X) + is-inhabited-or-empty-type-Finitely-Enumerable-Type = + rec-trunc-Prop + ( is-inhabited-or-empty-Prop (type-Finitely-Enumerable-Type X)) + ( λ (n , Fin-n↠X) → + is-inhabited-or-empty-surjection + ( Fin-n↠X) + ( is-inhabited-or-empty-Fin n)) + ( is-finitely-enumerable-type-Finitely-Enumerable-Type X) +``` + ## See also - A [Kuratowski finite set](univalent-combinatorics.kuratowski-finite-sets.md) diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index de4b1c1276..95b5d6686c 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -29,11 +29,13 @@ open import foundation.equivalences-maybe open import foundation.function-types open import foundation.homotopies open import foundation.identity-types +open import foundation.inhabited-types open import foundation.injective-maps open import foundation.negated-equality open import foundation.negation open import foundation.noncontractible-types open import foundation.preunivalent-type-families +open import foundation.propositional-truncations open import foundation.propositions open import foundation.raising-universe-levels open import foundation.retractions @@ -43,6 +45,8 @@ open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import structured-types.types-equipped-with-endomorphisms ``` @@ -502,6 +506,35 @@ is-preunivalent-Fin = is-preunivalent-retraction-equiv-tr-Set Fin-Set retraction-equiv-tr-Fin ``` +### The standard finite type `Fin n` is inhabited if and only if `n` is nonzero + +```agda +abstract + is-inhabited-is-nonzero-Fin : + (n : ℕ) → is-nonzero-ℕ n → is-inhabited (Fin n) + is-inhabited-is-nonzero-Fin zero-ℕ n≠0 = ex-falso (n≠0 refl) + is-inhabited-is-nonzero-Fin (succ-ℕ n) _ = unit-trunc-Prop (neg-one-Fin n) + + is-nonzero-is-inhabited-Fin : + (n : ℕ) → is-inhabited (Fin n) → is-nonzero-ℕ n + is-nonzero-is-inhabited-Fin _ H refl = rec-trunc-Prop empty-Prop (λ ()) H + +is-empty-is-zero-Fin : (n : ℕ) → is-zero-ℕ n → is-empty (Fin n) +is-empty-is-zero-Fin _ refl () +``` + +### The standard finite types are decidable + +```agda +is-decidable-Fin : (n : ℕ) → is-decidable (Fin n) +is-decidable-Fin zero-ℕ = inr (λ ()) +is-decidable-Fin (succ-ℕ n) = inl (neg-one-Fin n) + +is-inhabited-or-empty-Fin : (n : ℕ) → is-inhabited-or-empty (Fin n) +is-inhabited-or-empty-Fin n = + is-inhabited-or-empty-is-decidable (is-decidable-Fin n) +``` + ## See also - [Classical finite types](univalent-combinatorics.classical-finite-types.md),