edits

src/foundation/decidable-dependent-function-types.lagda.md

@@ -108,7 +108,8 @@ is-decidable-Π-Maybe {B = B} du de =
 
 ### Dependent products of decidable propositions over a π₀-trivial base are decidable propositions
 
-In other words, the base is empty or 0-connected.
+Assuming the base `A` is empty or 0-connected, a dependent product of decidable
+propositions over `A` is again a decidable proposition.
 
 ```agda
 module _

src/foundation/maps-with-hilbert-epsilon-operators.lagda.md

@@ -7,38 +7,10 @@ module foundation.maps-with-hilbert-epsilon-operators where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.natural-numbers
-
-open import foundation.action-on-identifications-functions
-open import foundation.cartesian-morphisms-arrows
-open import foundation.coproduct-types
-open import foundation.decidable-dependent-pair-types
-open import foundation.decidable-equality
-open import foundation.decidable-types
-open import foundation.dependent-pair-types
-open import foundation.functoriality-cartesian-product-types
-open import foundation.functoriality-coproduct-types
 open import foundation.hilberts-epsilon-operators
-open import foundation.identity-types
-open import foundation.mere-equality
-open import foundation.pi-0-trivial-maps
-open import foundation.propositional-truncations
-open import foundation.retracts-of-maps
-open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
-open import foundation-core.contractible-maps
-open import foundation-core.contractible-types
-open import foundation-core.empty-types
-open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
-open import foundation-core.function-types
-open import foundation-core.functoriality-dependent-pair-types
-open import foundation-core.homotopies
-open import foundation-core.injective-maps
-open import foundation-core.iterating-functions
-open import foundation-core.retractions
-open import foundation-core.sections
 ```
 
 </details>

src/foundation/perfect-images.lagda.md

@@ -158,24 +158,25 @@ module _
 
 ## Properties
 
-If `g` is an embedding then being a perfect image for `g` is a property.
+### If `g` is an embedding then being a perfect image for `g` is a property
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A} (is-emb-g : is-emb g)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
   is-prop-is-perfect-image-is-emb :
-    (a : A) → is-prop (is-perfect-image f g a)
-  is-prop-is-perfect-image-is-emb a =
-    is-prop-iterated-Π 3 (λ a₀ n p → is-prop-map-is-emb is-emb-g a₀)
+    is-emb g → (a : A) → is-prop (is-perfect-image f g a)
+  is-prop-is-perfect-image-is-emb G a =
+    is-prop-iterated-Π 3 (λ a₀ n p → is-prop-map-is-emb G a₀)
 
-  is-perfect-image-Prop : A → Prop (l1 ⊔ l2)
-  pr1 (is-perfect-image-Prop a) = is-perfect-image f g a
-  pr2 (is-perfect-image-Prop a) = is-prop-is-perfect-image-is-emb a
+  is-perfect-image-Prop : is-emb g → A → Prop (l1 ⊔ l2)
+  pr1 (is-perfect-image-Prop G a) = is-perfect-image f g a
+  pr2 (is-perfect-image-Prop G a) = is-prop-is-perfect-image-is-emb G a
 ```
 
+### Fibers over perfect images
+
 If `a` is a perfect image for `g`, then `a` has a preimage under `g`. Just take
 `n = zero` in the definition.
 
@@ -206,16 +207,19 @@ module _
   is-section-inverse-of-perfect-image a ρ = pr2 (fiber-is-perfect-image a ρ)
 ```
 
+When `g` is also injective, the map gives a kind of
+[retraction](foundation-core.retractions.md) of `g`.
+
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A} (G : is-injective g)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
   is-retraction-inverse-of-perfect-image :
+    is-injective g →
     (b : B) (ρ : is-perfect-image f g (g b)) →
     inverse-of-perfect-image (g b) ρ ＝ b
-  is-retraction-inverse-of-perfect-image b ρ =
+  is-retraction-inverse-of-perfect-image G b ρ =
     G (is-section-inverse-of-perfect-image (g b) ρ)
 ```
 
@@ -228,8 +232,7 @@ module _
 
   previous-perfect-image-at' :
     (a : A) (n : ℕ) →
-    is-perfect-image-at' f g (g (f a)) (succ-ℕ n) →
-    is-perfect-image-at' f g a n
+    is-perfect-image-at' f g (g (f a)) (succ-ℕ n) → is-perfect-image-at' f g a n
   previous-perfect-image-at' a n γ (a₀ , p) = γ (a₀ , ap (g ∘ f) p)
 
   previous-perfect-image' :
@@ -241,8 +244,8 @@ module _
   previous-perfect-image a γ a₀ n p = γ a₀ (succ-ℕ n) (ap (g ∘ f) p)
 ```
 
-Perfect images goes to a disjoint place under `inverse-of-perfect-image` than
-`f`
+Perfect images of `g` relative to `f` not mapped to the image of `f` under
+`inverse-of-perfect-image`.
 
 ```agda
 module _
@@ -267,7 +270,12 @@ module _
     v = tr (λ a' → ¬ (is-perfect-image f g a')) q s
 ```
 
-### Decidability of being a perfect image at a natural number
+### Decidability of perfect images
+
+Assuming `g` and `f` are decidable embedding, then for every natural number
+`n : ℕ` and every element `a : A` it is decidable whether `a` is a perfect image
+of `g` relative to `f` after `n` iterations. In fact, the map `f` need only be
+propositionally decidable and π₀-trivial.
 
 ```agda
 module _
@@ -306,92 +314,73 @@ module _
       ( is-inhabited-or-empty-map-is-decidable-map F)
 ```
 
-### The constructive story
-
-#### Untruncated double negation elimination on nonperfect fibers
+### Double negation elimination on nonperfect fibers
 
 If we assume that `g` is a double negation eliminating map, we can prove that if
 `is-nonperfect-image a` does not hold, then we have `is-perfect-image a`.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A} (G : is-double-negation-eliminating-map g)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
   double-negation-elim-is-perfect-image :
+    is-double-negation-eliminating-map g →
     (a : A) → ¬ (is-nonperfect-image a) → is-perfect-image f g a
-  double-negation-elim-is-perfect-image a nρ a₀ n p =
+  double-negation-elim-is-perfect-image G a nρ a₀ n p =
     G a₀ (λ a₁ → nρ (a₀ , n , p , a₁))
 ```
 
-The following property states that if `g (b)` is not a perfect image, then `b`
-has an `f` fiber `a` that is not a perfect image for `g`. Again, we need to
-assume law of excluded middle and that both `g` and `f` are embedding.
+If `g(b)` is not a perfect image, then `b` has an `f`-fiber `a` that is not a
+perfect image for `g`.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A}
-  (G : is-double-negation-eliminating-map g)
-  (b : B)
-  (nρ : ¬ (is-perfect-image f g (g b)))
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
   is-irrefutable-is-nonperfect-image-is-not-perfect-image :
+    (G : is-double-negation-eliminating-map g)
+    (b : B) (nρ : ¬ (is-perfect-image f g (g b))) →
     ¬¬ (is-nonperfect-image {f = f} (g b))
-  is-irrefutable-is-nonperfect-image-is-not-perfect-image nμ =
+  is-irrefutable-is-nonperfect-image-is-not-perfect-image G b nρ nμ =
     nρ (double-negation-elim-is-perfect-image G (g b) nμ)
 
-module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
-  (is-injective-g : is-injective g) (b : B)
-  where
-
   has-nonperfect-fiber-is-nonperfect-image :
+    is-injective g → (b : B) →
     is-nonperfect-image {f = f} (g b) → has-nonperfect-fiber f g b
-  has-nonperfect-fiber-is-nonperfect-image (x₀ , zero-ℕ , u) =
+  has-nonperfect-fiber-is-nonperfect-image G b (x₀ , zero-ℕ , u) =
     ex-falso (pr2 u (b , inv (pr1 u)))
-  has-nonperfect-fiber-is-nonperfect-image (x₀ , succ-ℕ n , u) =
-    ( iterate n (g ∘ f) x₀ , is-injective-g (pr1 u)) ,
+  has-nonperfect-fiber-is-nonperfect-image G b (x₀ , succ-ℕ n , u) =
+    ( iterate n (g ∘ f) x₀ , G (pr1 u)) ,
     ( λ s → pr2 u (s x₀ n refl))
 
-module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A}
-  (is-double-negation-eliminating-g : is-double-negation-eliminating-map g)
-  (is-injective-g : is-injective g)
-  (b : B) (nρ : ¬ (is-perfect-image f g (g b)))
-  where
-
   is-irrefutable-has-nonperfect-fiber-is-not-perfect-image :
+    is-double-negation-eliminating-map g → is-injective g →
+    (b : B) (nρ : ¬ (is-perfect-image f g (g b))) →
     ¬¬ (has-nonperfect-fiber f g b)
-  is-irrefutable-has-nonperfect-fiber-is-not-perfect-image t =
-    is-irrefutable-is-nonperfect-image-is-not-perfect-image
-      ( is-double-negation-eliminating-g)
-      ( b)
-      ( nρ)
-      ( λ s → t (has-nonperfect-fiber-is-nonperfect-image is-injective-g b s))
+  is-irrefutable-has-nonperfect-fiber-is-not-perfect-image G G' b nρ t =
+    is-irrefutable-is-nonperfect-image-is-not-perfect-image G b nρ
+      ( λ s → t (has-nonperfect-fiber-is-nonperfect-image G' b s))
+```
 
+If `f` is π₀-trivial and has double negation elimination, then
+
+```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A}
-  (is-double-negation-eliminating-f : is-double-negation-eliminating-map f)
-  (is-π₀-trivial-f : is-π₀-trivial-map' f)
-  (b : B)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
   double-negation-elim-has-nonperfect-fiber :
-    has-double-negation-elim (has-nonperfect-fiber f g b)
-  double-negation-elim-has-nonperfect-fiber =
-    double-negation-elim-Σ-all-elements-merely-equal-base
-      ( is-π₀-trivial-f b)
-      ( is-double-negation-eliminating-f b)
+    is-double-negation-eliminating-map f →
+    is-π₀-trivial-map' f →
+    (b : B) → has-double-negation-elim (has-nonperfect-fiber f g b)
+  double-negation-elim-has-nonperfect-fiber F F' b =
+    double-negation-elim-Σ-all-elements-merely-equal-base (F' b) (F b)
       ( λ p → double-negation-elim-neg (is-perfect-image f g (pr1 p)))
 
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A}
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   (is-double-negation-eliminating-g : is-double-negation-eliminating-map g)
   (is-injective-g : is-injective g)
   (is-double-negation-eliminating-f : is-double-negation-eliminating-map f)

src/logic/propositionally-decidable-maps.lagda.md

@@ -194,128 +194,3 @@ module _
       ( is-inhabited-or-empty-f)
       ( is-inhabited-or-empty-map-iterate-is-π₀-trivial-map' n)
 ```
-
-### Left cancellation for decidable maps
-
-If a composite `g ∘ f` is decidable and `g` is injective then `f` is decidable.
-
-```text
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : A → B} {g : B → C}
-  where
-
-  abstract
-    is-inhabited-or-empty-map-right-factor' :
-      is-inhabited-or-empty-map (g ∘ f) → is-injective g → is-inhabited-or-empty-map f
-    is-inhabited-or-empty-map-right-factor' GF G y =
-      rec-coproduct
-        ( λ q → inl (pr1 q , G (pr2 q)))
-        ( λ q → inr (λ x → q ((pr1 x) , ap g (pr2 x))))
-        ( GF (g y))
-```
-
-### Retracts into types with decidable equality are decidable
-
-```text
-is-inhabited-or-empty-map-retraction :
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} → has-decidable-equality B →
-  (i : A → B) → retraction i → is-inhabited-or-empty-map i
-is-inhabited-or-empty-map-retraction d i (r , R) b =
-  is-decidable-iff
-    ( λ (p : i (r b) ＝ b) → r b , p)
-    ( λ t → ap (i ∘ r) (inv (pr2 t)) ∙ ap i (R (pr1 t)) ∙ pr2 t)
-    ( d (i (r b)) b)
-```
-
-### The map on total spaces induced by a family of decidable maps is decidable
-
-```text
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
-  where
-
-  is-inhabited-or-empty-map-tot :
-    {f : (x : A) → B x → C x} →
-    ((x : A) → is-inhabited-or-empty-map (f x)) → is-inhabited-or-empty-map (tot f)
-  is-inhabited-or-empty-map-tot {f} H x =
-    is-decidable-equiv (compute-fiber-tot f x) (H (pr1 x) (pr2 x))
-```
-
-### The map on total spaces induced by a decidable map on the base is decidable
-
-```text
-module _
-  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : B → UU l3)
-  where
-
-  is-inhabited-or-empty-map-Σ-map-base :
-    {f : A → B} → is-inhabited-or-empty-map f → is-inhabited-or-empty-map (map-Σ-map-base f C)
-  is-inhabited-or-empty-map-Σ-map-base {f} H x =
-    is-decidable-equiv' (compute-fiber-map-Σ-map-base f C x) (H (pr1 x))
-```
-
-### Products of decidable maps are decidable
-
-```text
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  where
-
-  is-inhabited-or-empty-map-product :
-    {f : A → B} {g : C → D} →
-    is-inhabited-or-empty-map f → is-inhabited-or-empty-map g → is-inhabited-or-empty-map (map-product f g)
-  is-inhabited-or-empty-map-product {f} {g} F G x =
-    is-decidable-equiv
-      ( compute-fiber-map-product f g x)
-      ( is-decidable-product (F (pr1 x)) (G (pr2 x)))
-```
-
-### Coproducts of decidable maps are decidable
-
-```text
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  where
-
-  is-inhabited-or-empty-map-coproduct :
-    {f : A → B} {g : C → D} →
-    is-inhabited-or-empty-map f →
-    is-inhabited-or-empty-map g →
-    is-inhabited-or-empty-map (map-coproduct f g)
-  is-inhabited-or-empty-map-coproduct {f} {g} F G (inl x) =
-    is-decidable-equiv' (compute-fiber-inl-map-coproduct f g x) (F x)
-  is-inhabited-or-empty-map-coproduct {f} {g} F G (inr y) =
-    is-decidable-equiv' (compute-fiber-inr-map-coproduct f g y) (G y)
-```
-
-### Propositionally decidable maps are closed under base change
-
-```text
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  {f : A → B} {g : C → D}
-  where
-
-  is-inhabited-or-empty-map-base-change :
-    cartesian-hom-arrow g f → is-inhabited-or-empty-map f → is-inhabited-or-empty-map g
-  is-inhabited-or-empty-map-base-change α F d =
-    is-decidable-equiv
-      ( equiv-fibers-cartesian-hom-arrow g f α d)
-      ( F (map-codomain-cartesian-hom-arrow g f α d))
-```
-
-### Propositionally decidable maps are closed under retracts of maps
-
-```text
-module _
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
-  {f : A → B} {g : X → Y}
-  where
-
-  is-decidable-retract-map :
-    f retract-of-map g → is-inhabited-or-empty-map g → is-inhabited-or-empty-map f
-  is-decidable-retract-map R G x =
-    is-decidable-retract-of
-      ( retract-fiber-retract-map f g R x)
-      ( G (map-codomain-inclusion-retract-map f g R x))
-```