Totally bounded sets are propositionally decidable (#1625)

...and so are lots of other simple types for which that principle wasn't
written down yet?

Author: lowasser

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

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

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
 ```
 

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
 <details><summary>Imports</summary>
 
 ```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)
+```

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
 ```
 
 </details>
@@ -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

src/real-numbers/inhabited-totally-bounded-subsets-real-numbers.lagda.md

@@ -19,14 +19,15 @@ 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
 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

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-ℝ =

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),