From 81677d950e26d9587f12db905b72ebee5b102197 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 23 Oct 2025 18:01:30 -0700 Subject: [PATCH 01/12] Totally bounded sets are propositionally decidable --- .../approximations-metric-spaces.lagda.md | 32 +++++++---- ...y-bounded-subspaces-metric-spaces.lagda.md | 28 ++++++++++ src/metric-spaces/nets-metric-spaces.lagda.md | 54 +++++++++++++------ ...ally-bounded-subsets-real-numbers.lagda.md | 32 ++++++++++- ...ally-bounded-subsets-real-numbers.lagda.md | 3 ++ .../finitely-enumerable-types.lagda.md | 2 + .../inhabited-finite-types.lagda.md | 53 ++++++++++++++++++ ...habited-finitely-enumerable-types.lagda.md | 31 +++++++++++ 8 files changed, 208 insertions(+), 27 deletions(-) diff --git a/src/metric-spaces/approximations-metric-spaces.lagda.md b/src/metric-spaces/approximations-metric-spaces.lagda.md index bdafb94abc9..954449e15c9 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,29 @@ 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 ```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 19a7eefb419..134b25aa485 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 + decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space : + is-inhabited-or-empty (type-totally-bounded-subspace-Metric-Space X S) + decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space = + rec-trunc-Prop + ( is-inhabited-or-empty-Prop _) + ( λ M → + decide-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 cff36edfd50..092badfa9ca 100644 --- a/src/metric-spaces/nets-metric-spaces.lagda.md +++ b/src/metric-spaces/nets-metric-spaces.lagda.md @@ -9,6 +9,7 @@ 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 @@ -16,6 +17,8 @@ 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 +36,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 +84,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 +102,40 @@ 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 + +```agda +module _ + {l1 l2 l3 : Level} + (X : Metric-Space l1 l2) (ε : ℚ⁺) (S : net-Metric-Space l3 X ε) + where + + abstract + 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) +``` + +### Given any net for a metric space `X`, it is propositionally decidable whether `X` 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 : - inhabited-finitely-enumerable-subtype l3 (type-Metric-Space X) - inhabited-finitely-enumerable-subtype-net-Metric-Space = - ( finitely-enumerable-subset-net-Metric-Space X ε S , - is-inhabited-net-inhabited-Metric-Space) + decide-is-inhabited-or-empty-net-Metric-Space : + is-inhabited-or-empty (type-Metric-Space X) + decide-is-inhabited-or-empty-net-Metric-Space = + is-inhabited-or-empty-is-coinhabited + ( is-coinhabited-net-Metric-Space X ε S) + ( decide-is-inhabited-or-empty-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 7a22ced0180..737f7b66de1 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 @@ -27,6 +27,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 @@ -89,6 +91,10 @@ module _ ( metric-space-ℝ l2) ( S) + type-inhabited-totally-bounded-subset-ℝ : UU (l1 ⊔ lsuc l2) + type-inhabited-totally-bounded-subset-ℝ = + type-subtype subset-inhabited-totally-bounded-subset-ℝ + subspace-inhabited-totally-bounded-subset-ℝ : Metric-Space (l1 ⊔ lsuc l2) l2 subspace-inhabited-totally-bounded-subset-ℝ = @@ -142,8 +148,13 @@ module _ net δ = im-inhabited-finitely-enumerable-subtype ( inclusion-subset-ℝ S) - ( inhabited-finitely-enumerable-subtype-net-Metric-Space - ( metric-space-subset-ℝ S) |S| δ (M δ)) + ( finitely-enumerable-subset-net-Metric-Space + ( metric-space-subset-ℝ S) + ( δ) + ( M δ) , + backward-implication + ( is-coinhabited-net-Metric-Space (metric-space-subset-ℝ S) δ (M δ)) + ( |S|)) is-net : (δ : ℚ⁺) → @@ -386,6 +397,23 @@ module _ is-infimum-inf-inhabited-totally-bounded-subset-ℝ) ``` +### It is decidable whether a totally bounded subset of `ℝ` is inhabited + +```agda +module _ + {l1 l2 l3 : Level} + (S : totally-bounded-subset-ℝ l1 l2 l3) + where + + abstract + decide-is-inhabited-or-empty-totally-bounded-subset-ℝ : + is-inhabited-or-empty (type-totally-bounded-subset-ℝ S) + decide-is-inhabited-or-empty-totally-bounded-subset-ℝ = + decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space + ( metric-space-ℝ l2) + ( S) +``` + ## References {{#bibliography}} 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 dab0fa8a2a8..3f060650bf2 100644 --- a/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md +++ b/src/real-numbers/totally-bounded-subsets-real-numbers.lagda.md @@ -66,6 +66,9 @@ module _ subset-totally-bounded-subset-ℝ : subset-ℝ l1 l2 subset-totally-bounded-subset-ℝ = pr1 S + type-totally-bounded-subset-ℝ : UU (l1 ⊔ lsuc l2) + 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-ℝ = metric-space-subset-ℝ subset-totally-bounded-subset-ℝ diff --git a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md index a6ad4309bbc..7dee369ca06 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 diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md index 62ad690ee5d..b22012bc8a4 100644 --- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md @@ -8,12 +8,17 @@ module univalent-combinatorics.inhabited-finite-types where ```agda open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import foundation.coproduct-types +open import foundation.empty-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.identity-types open import foundation.inhabited-types +open import foundation.logical-equivalences +open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.subuniverses @@ -21,8 +26,11 @@ open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.finite-types +open import univalent-combinatorics.standard-finite-types ```
@@ -180,3 +188,48 @@ pr1 (is-finite-and-inhabited-type-Type-With-Cardinality-ℕ-succ-ℕ n F) = pr2 (is-finite-and-inhabited-type-Type-With-Cardinality-ℕ-succ-ℕ n F) = is-inhabited-type-Type-With-Cardinality-ℕ-succ-ℕ n F ``` + +### 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 propositionally decidable + +```agda +decide-is-inhabited-or-empty-Fin : (n : ℕ) → is-inhabited-or-empty (Fin n) +decide-is-inhabited-or-empty-Fin zero-ℕ = inr (λ ()) +decide-is-inhabited-or-empty-Fin (succ-ℕ n) = + inl (unit-trunc-Prop (neg-one-Fin n)) +``` + +### The finite types are propositionally decidable + +```agda +module _ + {l : Level} (X : Finite-Type l) + where + + decide-is-inhabited-or-empty-Finite-Type : + is-inhabited-or-empty (type-Finite-Type X) + decide-is-inhabited-or-empty-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) + ( decide-is-inhabited-or-empty-Fin N)) + ( is-finite-type-Finite-Type X) +``` diff --git a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md index d4508201a31..fc8a9cfa7cd 100644 --- a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md @@ -7,8 +7,10 @@ module univalent-combinatorics.inhabited-finitely-enumerable-types where
Imports ```agda +open import elementary-number-theory.equality-natural-numbers open import elementary-number-theory.natural-numbers +open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.existential-quantification @@ -23,7 +25,10 @@ open import foundation.subtypes open import foundation.surjective-maps open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import univalent-combinatorics.finitely-enumerable-types +open import univalent-combinatorics.inhabited-finite-types open import univalent-combinatorics.standard-finite-types ``` @@ -92,3 +97,29 @@ abstract (succ-ℕ n , Fin-sn↠X) → (n , Fin-sn↠X)) ( ∃eX) ``` + +### The finitely enumerable types are propositionally decidable + +```agda +module _ + {l : Level} (X : Finitely-Enumerable-Type l) + where + + abstract + decide-is-inhabited-or-empty-Finitely-Enumerable-Type : + is-inhabited-or-empty (type-Finitely-Enumerable-Type X) + decide-is-inhabited-or-empty-Finitely-Enumerable-Type = + rec-trunc-Prop + ( is-inhabited-or-empty-Prop (type-Finitely-Enumerable-Type X)) + ( λ (N , Fin-n↠X) → + rec-coproduct + ( λ N=0 → + inr (is-empty-surjection Fin-n↠X (is-empty-is-zero-Fin N N=0))) + ( λ N≠0 → + inl + ( map-is-inhabited + ( map-surjection Fin-n↠X) + ( is-inhabited-is-nonzero-Fin N N≠0))) + ( is-decidable-is-zero-ℕ N)) + ( is-finitely-enumerable-type-Finitely-Enumerable-Type X) +``` From e09868df5e925f6aac974b4fb75d471f1f6f472c Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 24 Oct 2025 10:26:46 -0700 Subject: [PATCH 02/12] Update src/metric-spaces/approximations-metric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- src/metric-spaces/approximations-metric-spaces.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/metric-spaces/approximations-metric-spaces.lagda.md b/src/metric-spaces/approximations-metric-spaces.lagda.md index 954449e15c9..b511867dea7 100644 --- a/src/metric-spaces/approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/approximations-metric-spaces.lagda.md @@ -252,6 +252,7 @@ module _ ### 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) (ε : ℚ⁺) From 7230b11425ae873d3c261b312bf51ebebc817a13 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 24 Oct 2025 10:26:53 -0700 Subject: [PATCH 03/12] Update src/metric-spaces/nets-metric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- src/metric-spaces/nets-metric-spaces.lagda.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/metric-spaces/nets-metric-spaces.lagda.md b/src/metric-spaces/nets-metric-spaces.lagda.md index 092badfa9ca..1cdc2fde72b 100644 --- a/src/metric-spaces/nets-metric-spaces.lagda.md +++ b/src/metric-spaces/nets-metric-spaces.lagda.md @@ -104,6 +104,8 @@ module _ ### 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} From 4c2b948547533700ccf77e892ade196bc59e00c3 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 24 Oct 2025 10:26:59 -0700 Subject: [PATCH 04/12] Update src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- .../inhabited-totally-bounded-subsets-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 737f7b66de1..0accc16ae6f 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 @@ -406,7 +406,7 @@ module _ where abstract - decide-is-inhabited-or-empty-totally-bounded-subset-ℝ : + is-inhabited-or-empty-totally-bounded-subset-ℝ : is-inhabited-or-empty (type-totally-bounded-subset-ℝ S) decide-is-inhabited-or-empty-totally-bounded-subset-ℝ = decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space From 9f8d6603f76a47597ec2458068f47859838bc811 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 24 Oct 2025 10:27:05 -0700 Subject: [PATCH 05/12] Update src/metric-spaces/nets-metric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- src/metric-spaces/nets-metric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/metric-spaces/nets-metric-spaces.lagda.md b/src/metric-spaces/nets-metric-spaces.lagda.md index 1cdc2fde72b..e540eea9151 100644 --- a/src/metric-spaces/nets-metric-spaces.lagda.md +++ b/src/metric-spaces/nets-metric-spaces.lagda.md @@ -131,7 +131,7 @@ module _ where abstract - decide-is-inhabited-or-empty-net-Metric-Space : + is-inhabited-or-empty-type-is-inhabited-or-empty-net-Metric-Space : is-inhabited-or-empty (type-Metric-Space X) decide-is-inhabited-or-empty-net-Metric-Space = is-inhabited-or-empty-is-coinhabited From 2c2f0a8eeb17fe33feb94abc718114f39a8177c5 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 24 Oct 2025 10:27:21 -0700 Subject: [PATCH 06/12] Update src/metric-spaces/inhabited-totally-bounded-subspaces-metric-spaces.lagda.md Co-authored-by: Fredrik Bakke --- .../inhabited-totally-bounded-subspaces-metric-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 134b25aa485..99a24f44865 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 @@ -151,7 +151,7 @@ module _ where abstract - decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space : + is-inhabited-or-empty-totally-bounded-subspace-Metric-Space : is-inhabited-or-empty (type-totally-bounded-subspace-Metric-Space X S) decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space = rec-trunc-Prop From 82d0026db5a82b15404bee340b6dfa666e03f3b8 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 24 Oct 2025 10:27:29 -0700 Subject: [PATCH 07/12] Respond to review comments --- src/foundation/surjective-maps.lagda.md | 16 +++++++++++++ .../propositionally-decidable-types.lagda.md | 21 ++++++++++++++++ src/metric-spaces/nets-metric-spaces.lagda.md | 2 +- .../inhabited-finite-types.lagda.md | 24 ++++++++++--------- ...habited-finitely-enumerable-types.lagda.md | 16 ++++--------- 5 files changed, 56 insertions(+), 23 deletions(-) diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 2c2aff28b88..6362b896c17 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -24,6 +24,7 @@ open import foundation.inhabited-types open import foundation.postcomposition-dependent-functions open import foundation.propositional-truncations open import foundation.split-surjective-maps +open import foundation.coinhabited-pairs-of-types open import foundation.structure-identity-principle open import foundation.subtype-identity-principle open import foundation.truncated-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 f8496f687db..bd199728d6a 100644 --- a/src/logic/propositionally-decidable-types.lagda.md +++ b/src/logic/propositionally-decidable-types.lagda.md @@ -17,6 +17,7 @@ open import foundation.functoriality-coproduct-types open import foundation.functoriality-propositional-truncation open import foundation.logical-equivalences open import foundation.negation +open import foundation.surjective-maps open import foundation.propositional-truncations open import foundation.retracts-of-types open import foundation.universe-levels @@ -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/nets-metric-spaces.lagda.md b/src/metric-spaces/nets-metric-spaces.lagda.md index 092badfa9ca..88949f16971 100644 --- a/src/metric-spaces/nets-metric-spaces.lagda.md +++ b/src/metric-spaces/nets-metric-spaces.lagda.md @@ -134,7 +134,7 @@ module _ decide-is-inhabited-or-empty-net-Metric-Space = is-inhabited-or-empty-is-coinhabited ( is-coinhabited-net-Metric-Space X ε S) - ( decide-is-inhabited-or-empty-Finitely-Enumerable-Type + ( is-inhabited-or-empty-type-Finitely-Enumerable-Type ( finitely-enumerable-type-net-Metric-Space X ε S)) ``` diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md index b22012bc8a4..3aad8f87be4 100644 --- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md @@ -12,6 +12,7 @@ open import elementary-number-theory.nonzero-natural-numbers open import foundation.coproduct-types open import foundation.empty-types +open import foundation.decidable-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-function-types @@ -206,13 +207,16 @@ is-empty-is-zero-Fin : (n : ℕ) → is-zero-ℕ n → is-empty (Fin n) is-empty-is-zero-Fin _ refl () ``` -### The standard finite types are propositionally decidable +### The standard finite types are decidable ```agda -decide-is-inhabited-or-empty-Fin : (n : ℕ) → is-inhabited-or-empty (Fin n) -decide-is-inhabited-or-empty-Fin zero-ℕ = inr (λ ()) -decide-is-inhabited-or-empty-Fin (succ-ℕ n) = - inl (unit-trunc-Prop (neg-one-Fin n)) +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) ``` ### The finite types are propositionally decidable @@ -222,14 +226,12 @@ module _ {l : Level} (X : Finite-Type l) where - decide-is-inhabited-or-empty-Finite-Type : + is-inhabited-or-empty-type-Finite-Type : is-inhabited-or-empty (type-Finite-Type X) - decide-is-inhabited-or-empty-Finite-Type = + 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) - ( decide-is-inhabited-or-empty-Fin N)) + ( λ (n , Fin-n≃X) → + is-inhabited-or-empty-equiv' Fin-n≃X (is-inhabited-or-empty-Fin n)) ( is-finite-type-Finite-Type X) ``` diff --git a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md index fc8a9cfa7cd..58f25e84a96 100644 --- a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md @@ -106,20 +106,14 @@ module _ where abstract - decide-is-inhabited-or-empty-Finitely-Enumerable-Type : + is-inhabited-or-empty-type-Finitely-Enumerable-Type : is-inhabited-or-empty (type-Finitely-Enumerable-Type X) - decide-is-inhabited-or-empty-Finitely-Enumerable-Type = + 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) → - rec-coproduct - ( λ N=0 → - inr (is-empty-surjection Fin-n↠X (is-empty-is-zero-Fin N N=0))) - ( λ N≠0 → - inl - ( map-is-inhabited - ( map-surjection Fin-n↠X) - ( is-inhabited-is-nonzero-Fin N N≠0))) - ( is-decidable-is-zero-ℕ N)) + is-inhabited-or-empty-surjection + ( Fin-n↠X) + ( is-inhabited-or-empty-Fin N)) ( is-finitely-enumerable-type-Finitely-Enumerable-Type X) ``` From 0ed637a9bc48e2b2cff1f84bf0de914d3f650716 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 4 Nov 2025 19:50:48 -0800 Subject: [PATCH 08/12] Respond to comments --- src/foundation/surjective-maps.lagda.md | 2 +- src/logic/propositionally-decidable-types.lagda.md | 2 +- src/metric-spaces/approximations-metric-spaces.lagda.md | 1 + src/metric-spaces/nets-metric-spaces.lagda.md | 2 +- src/univalent-combinatorics/inhabited-finite-types.lagda.md | 2 +- 5 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 6362b896c17..0f9dde78f7a 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 @@ -24,7 +25,6 @@ open import foundation.inhabited-types open import foundation.postcomposition-dependent-functions open import foundation.propositional-truncations open import foundation.split-surjective-maps -open import foundation.coinhabited-pairs-of-types open import foundation.structure-identity-principle open import foundation.subtype-identity-principle open import foundation.truncated-types diff --git a/src/logic/propositionally-decidable-types.lagda.md b/src/logic/propositionally-decidable-types.lagda.md index bd199728d6a..62d7e2dc165 100644 --- a/src/logic/propositionally-decidable-types.lagda.md +++ b/src/logic/propositionally-decidable-types.lagda.md @@ -17,9 +17,9 @@ open import foundation.functoriality-coproduct-types open import foundation.functoriality-propositional-truncation open import foundation.logical-equivalences open import foundation.negation -open import foundation.surjective-maps 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 diff --git a/src/metric-spaces/approximations-metric-spaces.lagda.md b/src/metric-spaces/approximations-metric-spaces.lagda.md index b511867dea7..9fd8695105d 100644 --- a/src/metric-spaces/approximations-metric-spaces.lagda.md +++ b/src/metric-spaces/approximations-metric-spaces.lagda.md @@ -253,6 +253,7 @@ module _ ### 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) (ε : ℚ⁺) diff --git a/src/metric-spaces/nets-metric-spaces.lagda.md b/src/metric-spaces/nets-metric-spaces.lagda.md index e0141152a79..ea91bd5dece 100644 --- a/src/metric-spaces/nets-metric-spaces.lagda.md +++ b/src/metric-spaces/nets-metric-spaces.lagda.md @@ -133,7 +133,7 @@ module _ abstract is-inhabited-or-empty-type-is-inhabited-or-empty-net-Metric-Space : is-inhabited-or-empty (type-Metric-Space X) - decide-is-inhabited-or-empty-net-Metric-Space = + 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 diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md index 3aad8f87be4..4128c93abb4 100644 --- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md @@ -11,8 +11,8 @@ open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonzero-natural-numbers open import foundation.coproduct-types -open import foundation.empty-types open import foundation.decidable-types +open import foundation.empty-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-function-types From 6af8910c04ec3c10b7cd4dcfa689e00090f27707 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 4 Nov 2025 20:26:34 -0800 Subject: [PATCH 09/12] Fix build --- ...inhabited-totally-bounded-subspaces-metric-spaces.lagda.md | 4 ++-- .../inhabited-totally-bounded-subsets-real-numbers.lagda.md | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) 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 99a24f44865..04ab52fb2e5 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 @@ -153,11 +153,11 @@ module _ abstract is-inhabited-or-empty-totally-bounded-subspace-Metric-Space : is-inhabited-or-empty (type-totally-bounded-subspace-Metric-Space X S) - decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space = + is-inhabited-or-empty-totally-bounded-subspace-Metric-Space = rec-trunc-Prop ( is-inhabited-or-empty-Prop _) ( λ M → - decide-is-inhabited-or-empty-net-Metric-Space + is-inhabited-or-empty-type-is-inhabited-or-empty-net-Metric-Space ( subspace-totally-bounded-subspace-Metric-Space X S) ( one-ℚ⁺) ( M one-ℚ⁺)) 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 419bf8bd570..ae2f9e14b13 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 @@ -417,8 +417,8 @@ module _ abstract is-inhabited-or-empty-totally-bounded-subset-ℝ : is-inhabited-or-empty (type-totally-bounded-subset-ℝ S) - decide-is-inhabited-or-empty-totally-bounded-subset-ℝ = - decide-is-inhabited-or-empty-totally-bounded-subspace-Metric-Space + is-inhabited-or-empty-totally-bounded-subset-ℝ = + is-inhabited-or-empty-totally-bounded-subspace-Metric-Space ( metric-space-ℝ l2) ( S) ``` From 265f5bfb961dfb85060e9db1f2e1491b97d706c3 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 5 Nov 2025 15:20:06 -0800 Subject: [PATCH 10/12] Update src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md Co-authored-by: Fredrik Bakke --- .../inhabited-finitely-enumerable-types.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md index 58f25e84a96..dc1cf32f097 100644 --- a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md @@ -111,9 +111,9 @@ module _ 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) → + ( λ (n , Fin-n↠X) → is-inhabited-or-empty-surjection ( Fin-n↠X) - ( is-inhabited-or-empty-Fin N)) + ( is-inhabited-or-empty-Fin n)) ( is-finitely-enumerable-type-Finitely-Enumerable-Type X) ``` From 843b40065c9839d416e66b3e57d3d8692d0a3709 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 5 Nov 2025 16:03:53 -0800 Subject: [PATCH 11/12] Respond to review comments --- src/metric-spaces/nets-metric-spaces.lagda.md | 22 ++++++++- ...ally-bounded-subsets-real-numbers.lagda.md | 13 ++--- .../finite-types.lagda.md | 17 +++++++ .../finitely-enumerable-types.lagda.md | 20 ++++++++ .../inhabited-finite-types.lagda.md | 48 ------------------- ...habited-finitely-enumerable-types.lagda.md | 20 -------- .../standard-finite-types.lagda.md | 33 +++++++++++++ 7 files changed, 96 insertions(+), 77 deletions(-) diff --git a/src/metric-spaces/nets-metric-spaces.lagda.md b/src/metric-spaces/nets-metric-spaces.lagda.md index ea91bd5dece..da1b4d01421 100644 --- a/src/metric-spaces/nets-metric-spaces.lagda.md +++ b/src/metric-spaces/nets-metric-spaces.lagda.md @@ -13,6 +13,7 @@ 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 @@ -120,9 +121,28 @@ module _ ( 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-subset-net-is-inhabited-Metric-Space |S| = + ( finitely-enumerable-subset-net-Metric-Space X ε S , + is-inhabited-net-is-inhabited-type-Metric-Space |S|) ``` -### Given any net for a metric space `X`, it is propositionally decidable whether `X` is inhabited +### Given any net for a metric space `X`, `X` is propositionally decidable ```agda module _ 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 ae2f9e14b13..ba28d0da3cd 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 @@ -157,13 +156,11 @@ module _ net δ = im-inhabited-finitely-enumerable-subtype ( inclusion-subset-ℝ S) - ( finitely-enumerable-subset-net-Metric-Space - ( metric-space-subset-ℝ S) - ( δ) - ( M δ) , - backward-implication - ( is-coinhabited-net-Metric-Space (metric-space-subset-ℝ S) δ (M δ)) - ( |S|)) + ( inhabited-finitely-enumerable-subset-net-is-inhabited-Metric-Space + ( metric-space-subset-ℝ S) + ( δ) + ( M δ) + ( |S|)) is-net : (δ : ℚ⁺) → diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index b4bb6e56eda..4dae49548c7 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 7dee369ca06..c042e396b2d 100644 --- a/src/univalent-combinatorics/finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/finitely-enumerable-types.lagda.md @@ -421,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/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md index 4128c93abb4..5417488fdcf 100644 --- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md @@ -27,8 +27,6 @@ open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels -open import logic.propositionally-decidable-types - open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types @@ -189,49 +187,3 @@ pr1 (is-finite-and-inhabited-type-Type-With-Cardinality-ℕ-succ-ℕ n F) = pr2 (is-finite-and-inhabited-type-Type-With-Cardinality-ℕ-succ-ℕ n F) = is-inhabited-type-Type-With-Cardinality-ℕ-succ-ℕ n F ``` - -### 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) -``` - -### 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) -``` diff --git a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md index dc1cf32f097..c43014a0a23 100644 --- a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md @@ -97,23 +97,3 @@ abstract (succ-ℕ n , Fin-sn↠X) → (n , Fin-sn↠X)) ( ∃eX) ``` - -### 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) -``` diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index de4b1c1276c..95b5d6686ca 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), From 81f08a9d9c008a45c4dd9666c116b7665134b291 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 6 Nov 2025 12:46:28 +0100 Subject: [PATCH 12/12] Apply suggestions from code review --- ...inhabited-totally-bounded-subsets-real-numbers.lagda.md | 2 +- .../inhabited-finite-types.lagda.md | 7 ------- .../inhabited-finitely-enumerable-types.lagda.md | 5 ----- 3 files changed, 1 insertion(+), 13 deletions(-) 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 ba28d0da3cd..0549a213163 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 @@ -403,7 +403,7 @@ module _ is-infimum-inf-inhabited-totally-bounded-subset-ℝ) ``` -### It is decidable whether a totally bounded subset of `ℝ` is inhabited +### Any totally bounded subset of `ℝ` is propositionally decidable ```agda module _ diff --git a/src/univalent-combinatorics/inhabited-finite-types.lagda.md b/src/univalent-combinatorics/inhabited-finite-types.lagda.md index 5417488fdcf..62ad690ee5d 100644 --- a/src/univalent-combinatorics/inhabited-finite-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finite-types.lagda.md @@ -8,18 +8,12 @@ module univalent-combinatorics.inhabited-finite-types where ```agda open import elementary-number-theory.natural-numbers -open import elementary-number-theory.nonzero-natural-numbers -open import foundation.coproduct-types -open import foundation.decidable-types -open import foundation.empty-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.identity-types open import foundation.inhabited-types -open import foundation.logical-equivalences -open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.subuniverses @@ -29,7 +23,6 @@ open import foundation.universe-levels open import univalent-combinatorics.dependent-pair-types open import univalent-combinatorics.finite-types -open import univalent-combinatorics.standard-finite-types ```
diff --git a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md index c43014a0a23..d4508201a31 100644 --- a/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md +++ b/src/univalent-combinatorics/inhabited-finitely-enumerable-types.lagda.md @@ -7,10 +7,8 @@ module univalent-combinatorics.inhabited-finitely-enumerable-types where
Imports ```agda -open import elementary-number-theory.equality-natural-numbers open import elementary-number-theory.natural-numbers -open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.existential-quantification @@ -25,10 +23,7 @@ open import foundation.subtypes open import foundation.surjective-maps open import foundation.universe-levels -open import logic.propositionally-decidable-types - open import univalent-combinatorics.finitely-enumerable-types -open import univalent-combinatorics.inhabited-finite-types open import univalent-combinatorics.standard-finite-types ```