diff --git a/src/finite-group-theory/orbits-permutations.lagda.md b/src/finite-group-theory/orbits-permutations.lagda.md index 4b629bb9c1..f3a0833ae6 100644 --- a/src/finite-group-theory/orbits-permutations.lagda.md +++ b/src/finite-group-theory/orbits-permutations.lagda.md @@ -55,6 +55,8 @@ open import foundation.universe-levels open import lists.lists +open import logic.propositionally-decidable-types + open import univalent-combinatorics.2-element-decidable-subtypes open import univalent-combinatorics.2-element-types open import univalent-combinatorics.counting @@ -481,7 +483,6 @@ module _ ( prop-equivalence-relation same-orbits-permutation a b)) ( λ h → is-decidable-trunc-Prop-is-merely-decidable - ( Σ ℕ (λ k → Id (iterate k (map-equiv f) a) b)) ( unit-trunc-Prop ( is-decidable-iterate-is-decidable-bounded h a b ( is-decidable-bounded-Σ-ℕ n diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index 9b9dd2512c..ea01876a8c 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -36,6 +36,7 @@ open import foundation-core.homotopies public open import foundation-core.identity-types public open import foundation-core.injective-maps public open import foundation-core.invertible-maps public +open import foundation-core.iterating-functions public open import foundation-core.negation public open import foundation-core.operations-span-diagrams public open import foundation-core.operations-spans public diff --git a/src/foundation-core/contractible-maps.lagda.md b/src/foundation-core/contractible-maps.lagda.md index 2c2d1e9c41..898e0b2f67 100644 --- a/src/foundation-core/contractible-maps.lagda.md +++ b/src/foundation-core/contractible-maps.lagda.md @@ -20,6 +20,7 @@ open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.retractions open import foundation-core.sections +open import foundation-core.torsorial-type-families ``` @@ -134,6 +135,18 @@ module _ is-contr-map-is-coherently-invertible ∘ is-coherently-invertible-is-equiv ``` +### The identity function is contractible + +```agda +module _ + {l1 : Level} {A : UU l1} + where + + abstract + is-contr-map-id : is-contr-map (id {A = A}) + is-contr-map-id = is-torsorial-Id' +``` + ## See also - For the notion of biinvertible maps see diff --git a/src/foundation-core/decidable-propositions.lagda.md b/src/foundation-core/decidable-propositions.lagda.md index eb48a26b7d..76844c57bf 100644 --- a/src/foundation-core/decidable-propositions.lagda.md +++ b/src/foundation-core/decidable-propositions.lagda.md @@ -12,9 +12,9 @@ open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.double-negation open import foundation.negation -open import foundation.propositional-truncations open import foundation.transport-along-identifications open import foundation.unit-type +open import foundation.universal-property-empty-type open import foundation.universe-levels open import foundation-core.cartesian-product-types @@ -224,6 +224,16 @@ module _ is-decidable-prop-Σ : is-decidable-prop (Σ P Q) is-decidable-prop-Σ = ( is-prop-is-decidable-prop-Σ , is-decidable-is-decidable-prop-Σ) + +Σ-Decidable-Prop : + {l1 l2 : Level} → + (P : Decidable-Prop l1) → + (type-Decidable-Prop P → Decidable-Prop l2) → Decidable-Prop (l1 ⊔ l2) +Σ-Decidable-Prop P Q = + ( Σ (type-Decidable-Prop P) (type-Decidable-Prop ∘ Q) , + is-decidable-prop-Σ + ( is-decidable-prop-type-Decidable-Prop P) + ( is-decidable-prop-type-Decidable-Prop ∘ Q)) ``` ### The negation operation on decidable propositions @@ -251,38 +261,71 @@ type-neg-Decidable-Prop : type-neg-Decidable-Prop P = type-Decidable-Prop (neg-Decidable-Prop P) ``` -### Decidability of a propositional truncation +### Function types between decidable propositions ```agda -abstract - is-prop-is-decidable-trunc-Prop : - {l : Level} (A : UU l) → is-prop (is-decidable (type-trunc-Prop A)) - is-prop-is-decidable-trunc-Prop A = - is-prop-is-decidable is-prop-type-trunc-Prop - -is-decidable-trunc-Prop : {l : Level} → UU l → Prop l -pr1 (is-decidable-trunc-Prop A) = is-decidable (type-trunc-Prop A) -pr2 (is-decidable-trunc-Prop A) = is-prop-is-decidable-trunc-Prop A - -is-decidable-trunc-Prop-is-merely-decidable : - {l : Level} (A : UU l) → - is-merely-decidable A → is-decidable (type-trunc-Prop A) -is-decidable-trunc-Prop-is-merely-decidable A = - map-universal-property-trunc-Prop - ( is-decidable-trunc-Prop A) - ( f) +module _ + {l1 l2 : Level} {P : UU l1} {Q : UU l2} where - f : is-decidable A → type-Prop (is-decidable-trunc-Prop A) - f (inl a) = inl (unit-trunc-Prop a) - f (inr f) = inr (map-universal-property-trunc-Prop empty-Prop f) - -is-merely-decidable-is-decidable-trunc-Prop : - {l : Level} (A : UU l) → - is-decidable (type-trunc-Prop A) → is-merely-decidable A -is-merely-decidable-is-decidable-trunc-Prop A (inl x) = - apply-universal-property-trunc-Prop x - ( is-merely-decidable-Prop A) - ( unit-trunc-Prop ∘ inl) -is-merely-decidable-is-decidable-trunc-Prop A (inr f) = - unit-trunc-Prop (inr (f ∘ unit-trunc-Prop)) + + is-decidable-prop-function-type' : + is-decidable P → (P → is-decidable-prop Q) → is-decidable-prop (P → Q) + is-decidable-prop-function-type' H K = + ( rec-coproduct + ( λ p → is-prop-function-type (is-prop-type-is-decidable-prop (K p))) + ( λ np → is-prop-is-contr (universal-property-empty-is-empty P np Q)) + ( H)) , + ( is-decidable-function-type' H (is-decidable-type-is-decidable-prop ∘ K)) + + is-decidable-prop-function-type : + is-decidable P → is-decidable-prop Q → is-decidable-prop (P → Q) + is-decidable-prop-function-type H K = + ( is-prop-function-type (is-prop-type-is-decidable-prop K)) , + ( is-decidable-function-type H (is-decidable-type-is-decidable-prop K)) + +hom-Decidable-Prop : + {l1 l2 : Level} → + Decidable-Prop l1 → Decidable-Prop l2 → Decidable-Prop (l1 ⊔ l2) +hom-Decidable-Prop P Q = + ( type-Decidable-Prop P → type-Decidable-Prop Q) , + ( is-decidable-prop-function-type + ( is-decidable-Decidable-Prop P) + ( is-decidable-prop-type-Decidable-Prop Q)) +``` + +### Dependent products of decidable propositions + +```agda +module _ + {l1 l2 : Level} {P : UU l1} {Q : P → UU l2} + where + + is-decidable-Π-is-decidable-prop : + is-decidable-prop P → + ((x : P) → is-decidable-prop (Q x)) → + is-decidable ((x : P) → Q x) + is-decidable-Π-is-decidable-prop (H , inl x) K = + rec-coproduct + ( λ y → inl (λ x' → tr Q (eq-is-prop H) y)) + ( λ ny → inr (λ f → ny (f x))) + ( is-decidable-type-is-decidable-prop (K x)) + is-decidable-Π-is-decidable-prop (H , inr nx) K = + inl (λ x' → ex-falso (nx x')) + + is-decidable-prop-Π : + is-decidable-prop P → + ((x : P) → is-decidable-prop (Q x)) → + is-decidable-prop ((x : P) → Q x) + is-decidable-prop-Π H K = + ( is-prop-Π (is-prop-type-is-decidable-prop ∘ K)) , + ( is-decidable-Π-is-decidable-prop H K) + +Π-Decidable-Prop : + {l1 l2 : Level} (P : Decidable-Prop l1) → + (type-Decidable-Prop P → Decidable-Prop l2) → Decidable-Prop (l1 ⊔ l2) +Π-Decidable-Prop P Q = + ( (x : type-Decidable-Prop P) → type-Decidable-Prop (Q x)) , + ( is-decidable-prop-Π + ( is-decidable-prop-type-Decidable-Prop P) + ( is-decidable-prop-type-Decidable-Prop ∘ Q)) ``` diff --git a/src/foundation-core/injective-maps.lagda.md b/src/foundation-core/injective-maps.lagda.md index bf6bc84c72..6692efeaed 100644 --- a/src/foundation-core/injective-maps.lagda.md +++ b/src/foundation-core/injective-maps.lagda.md @@ -127,7 +127,7 @@ module _ where is-equiv-is-injective : {f : A → B} → section f → is-injective f → is-equiv f - is-equiv-is-injective {f} (pair g G) H = + is-equiv-is-injective {f} (g , G) H = is-equiv-is-invertible g G (λ x → H (G (f x))) ``` diff --git a/src/foundation-core/iterating-functions.lagda.md b/src/foundation-core/iterating-functions.lagda.md new file mode 100644 index 0000000000..e17b549215 --- /dev/null +++ b/src/foundation-core/iterating-functions.lagda.md @@ -0,0 +1,123 @@ +# Iterating functions + +```agda +module foundation-core.iterating-functions where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.subtypes +open import foundation.universe-levels + +open import foundation-core.commuting-squares-of-maps +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +``` + +
+ +## Idea + +Any map `f : X → X` can be +{{#concept "iterated" Disambiguation="endo map of types" Agda=iterate Agda=iterate'}} +by repeatedly applying `f`. + +## Definition + +### Iterating functions + +```agda +module _ + {l : Level} {X : UU l} + where + + iterate : ℕ → (X → X) → (X → X) + iterate zero-ℕ f x = x + iterate (succ-ℕ k) f x = f (iterate k f x) + + iterate' : ℕ → (X → X) → (X → X) + iterate' zero-ℕ f x = x + iterate' (succ-ℕ k) f x = iterate' k f (f x) +``` + +### Homotopies of iterating functions + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (s : A → A) (t : B → B) + where + + coherence-square-iterate : + {f : A → B} (H : coherence-square-maps f s t f) → + (n : ℕ) → coherence-square-maps f (iterate n s) (iterate n t) f + coherence-square-iterate {f} H zero-ℕ x = refl + coherence-square-iterate {f} H (succ-ℕ n) = + pasting-vertical-coherence-square-maps + ( f) + ( iterate n s) + ( iterate n t) + ( f) + ( s) + ( t) + ( f) + ( coherence-square-iterate H n) + ( H) +``` + +## Properties + +### The two definitions of iterating are homotopic + +```agda +module _ + {l : Level} {X : UU l} + where + + reassociate-iterate-succ-ℕ : + (k : ℕ) (f : X → X) (x : X) → iterate (succ-ℕ k) f x ＝ iterate k f (f x) + reassociate-iterate-succ-ℕ zero-ℕ f x = refl + reassociate-iterate-succ-ℕ (succ-ℕ k) f x = + ap f (reassociate-iterate-succ-ℕ k f x) + + reassociate-iterate : (k : ℕ) (f : X → X) → iterate k f ~ iterate' k f + reassociate-iterate zero-ℕ f x = refl + reassociate-iterate (succ-ℕ k) f x = + reassociate-iterate-succ-ℕ k f x ∙ reassociate-iterate k f (f x) +``` + +### If `f : X → X` satisfies a property of endofunctions on `X`, and the property is closed under composition then iterates of `f` satisfy the property + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {f : X → X} + (P : subtype l2 (X → X)) + where + + is-in-subtype-iterate-succ-ℕ : + (F : is-in-subtype P f) → + ( (h g : X → X) → + is-in-subtype P h → + is-in-subtype P g → + is-in-subtype P (h ∘ g)) → + (n : ℕ) → is-in-subtype P (iterate (succ-ℕ n) f) + is-in-subtype-iterate-succ-ℕ F H zero-ℕ = F + is-in-subtype-iterate-succ-ℕ F H (succ-ℕ n) = + H f (iterate (succ-ℕ n) f) F (is-in-subtype-iterate-succ-ℕ F H n) + + is-in-subtype-iterate : + (I : is-in-subtype P (id {A = X})) → + (F : is-in-subtype P f) → + ( (h g : X → X) → + is-in-subtype P h → + is-in-subtype P g → + is-in-subtype P (h ∘ g)) → + (n : ℕ) → is-in-subtype P (iterate n f) + is-in-subtype-iterate I F H zero-ℕ = I + is-in-subtype-iterate I F H (succ-ℕ n) = + H f (iterate n f) F (is-in-subtype-iterate I F H n) +``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 4e72fe1c04..47ea7e2c8d 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -270,6 +270,7 @@ open import foundation.locally-small-types public open import foundation.logical-equivalences public open import foundation.maps-in-global-subuniverses public open import foundation.maps-in-subuniverses public +open import foundation.maps-with-hilbert-epsilon-operators public open import foundation.maybe public open import foundation.mere-embeddings public open import foundation.mere-equality public @@ -316,6 +317,7 @@ open import foundation.path-split-maps public open import foundation.path-split-type-families public open import foundation.perfect-images public open import foundation.permutations-spans-families-of-types public +open import foundation.pi-0-trivial-maps public open import foundation.pi-decompositions public open import foundation.pi-decompositions-subuniverse public open import foundation.pointed-torsorial-type-families public diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md index d2bdc9203d..756f782225 100644 --- a/src/foundation/0-connected-types.lagda.md +++ b/src/foundation/0-connected-types.lagda.md @@ -41,8 +41,11 @@ open import foundation-core.truncation-levels ## Idea -A type is said to be connected if its type of connected components, i.e., its -set truncation, is contractible. +A type is said to be +{{#concept "0-connected" Disambiguation="type" Agda=is-0-connected}} if its type +of [connected components](foundation.connected-components.md), i.e., its +[set truncation](foundation.set-truncations.md), is +[contractible](foundation-core.contractible-types.md). ```agda is-0-connected-Prop : {l : Level} → UU l → Prop l @@ -65,7 +68,7 @@ abstract abstract mere-eq-is-0-connected : - {l : Level} {A : UU l} → is-0-connected A → (x y : A) → mere-eq x y + {l : Level} {A : UU l} → is-0-connected A → all-elements-merely-equal A mere-eq-is-0-connected {A = A} H x y = apply-effectiveness-unit-trunc-Set (eq-is-contr H) @@ -83,7 +86,7 @@ abstract abstract is-0-connected-mere-eq-is-inhabited : {l : Level} {A : UU l} → - is-inhabited A → ((x y : A) → mere-eq x y) → is-0-connected A + is-inhabited A → all-elements-merely-equal A → is-0-connected A is-0-connected-mere-eq-is-inhabited H K = apply-universal-property-trunc-Prop H ( is-0-connected-Prop _) diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md index 7f0d889d21..477004c227 100644 --- a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md +++ b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md @@ -1,4 +1,4 @@ -# The Cantor–Schröder–Bernstein–Escardó theorem +# The Cantor–Schröder–Bernstein–Escardó construction ```agda module foundation.cantor-schroder-bernstein-escardo where @@ -7,14 +7,28 @@ module foundation.cantor-schroder-bernstein-escardo where
Imports ```agda +open import elementary-number-theory.natural-numbers + open import foundation.action-on-identifications-functions +open import foundation.decidable-embeddings +open import foundation.decidable-maps +open import foundation.decidable-propositions open import foundation.decidable-types open import foundation.dependent-pair-types +open import foundation.double-negation +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types open import foundation.injective-maps open import foundation.law-of-excluded-middle +open import foundation.maps-with-hilbert-epsilon-operators open import foundation.perfect-images +open import foundation.pi-0-trivial-maps +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sections open import foundation.split-surjective-maps open import foundation.universe-levels +open import foundation.weak-limited-principle-of-omniscience open import foundation-core.coproduct-types open import foundation-core.embeddings @@ -23,7 +37,11 @@ open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.identity-types open import foundation-core.negation +open import foundation-core.propositional-maps open import foundation-core.sets + +open import logic.double-negation-eliminating-maps +open import logic.double-negation-stable-embeddings ```
@@ -38,146 +56,339 @@ Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for [embed](foundation-core.embeddings.md) into each other, then the types are [equivalent](foundation-core.equivalences.md). {{#cite Esc21}} +In this file we give a fine-grained analysis of the construction used in the +proof of this _Cantor–Schröder–Bernstein-Escardó theorem_, and use this +deconstruction to give a series of further generalizations of the theorem. + The Cantor–Schröder–Bernstein theorem is the 25th theorem on [Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. -## Statement +## The Cantor-Schröder-Bernstein-Escardó construction -```agda -type-Cantor-Schröder-Bernstein-Escardó : (l1 l2 : Level) → UU (lsuc (l1 ⊔ l2)) -type-Cantor-Schröder-Bernstein-Escardó l1 l2 = - {X : UU l1} {Y : UU l2} → (X ↪ Y) → (Y ↪ X) → X ≃ Y -``` +Given a pair of mutual maps `f : A → B` and `g : B → A` such that -## Proof +1. the maps `f` and `g` satisfy double negation elimination on their fibers +2. For every element `x : A` it is decidable wheter `x` is a perfect image of + `g` relative to `f` +3. `g` is injective +4. `f` is π₀-trivial -### The law of excluded middle implies Cantor-Schröder-Bernstein-Escardó +Then `B` is a retract of `A`. If `f` moreover is injective, then this retract is +an equivalence. ```agda module _ - {l1 l2 : Level} (lem : LEM (l1 ⊔ l2)) + {l1 l2 : Level} + {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} + (G' : is-injective g) + (G : is-double-negation-eliminating-map g) + (F : is-double-negation-eliminating-map f) where - module _ - {X : UU l1} {Y : UU l2} (f : X ↪ Y) (g : Y ↪ X) - where - - map-Cantor-Schröder-Bernstein-Escardó' : - (x : X) → is-decidable (is-perfect-image (map-emb f) (map-emb g) x) → Y - map-Cantor-Schröder-Bernstein-Escardó' x (inl y) = - inverse-of-perfect-image x y - map-Cantor-Schröder-Bernstein-Escardó' x (inr y) = - map-emb f x - - map-Cantor-Schröder-Bernstein-Escardó : - X → Y - map-Cantor-Schröder-Bernstein-Escardó x = - map-Cantor-Schröder-Bernstein-Escardó' x - ( is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x) - - is-injective-map-Cantor-Schröder-Bernstein-Escardó : - is-injective map-Cantor-Schröder-Bernstein-Escardó - is-injective-map-Cantor-Schröder-Bernstein-Escardó {x} {x'} = - l (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x) - (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x') - where - l : - (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) - (d' : is-decidable (is-perfect-image (map-emb f) (map-emb g) x')) → - ( map-Cantor-Schröder-Bernstein-Escardó' x d) ＝ - ( map-Cantor-Schröder-Bernstein-Escardó' x' d') → - x ＝ x' - l (inl ρ) (inl ρ') p = - inv (is-section-inverse-of-perfect-image x ρ) ∙ - (ap (map-emb g) p ∙ is-section-inverse-of-perfect-image x' ρ') - l (inl ρ) (inr nρ') p = - ex-falso (perfect-image-has-distinct-image x' x nρ' ρ (inv p)) - l (inr nρ) (inl ρ') p = - ex-falso (perfect-image-has-distinct-image x x' nρ ρ' p) - l (inr nρ) (inr nρ') p = - is-injective-is-emb (is-emb-map-emb f) p - - is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó : - is-split-surjective map-Cantor-Schröder-Bernstein-Escardó - is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó y = - pair x p - where - a : - is-decidable - ( is-perfect-image (map-emb f) (map-emb g) (map-emb g y)) → - Σ ( X) - ( λ x → - ( (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) → - map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y)) - a (inl γ) = - pair (map-emb g y) ψ - where - ψ : - ( d : - is-decidable - ( is-perfect-image (map-emb f) (map-emb g) (map-emb g y))) → - map-Cantor-Schröder-Bernstein-Escardó' (map-emb g y) d ＝ y - ψ (inl v') = - is-retraction-inverse-of-perfect-image - { is-emb-g = is-emb-map-emb g} - ( y) - ( v') - ψ (inr v) = ex-falso (v γ) - a (inr γ) = - pair x ψ - where - w : - Σ ( fiber (map-emb f) y) - ( λ s → ¬ (is-perfect-image (map-emb f) (map-emb g) (pr1 s))) - w = - not-perfect-image-has-not-perfect-fiber - ( is-emb-map-emb f) - ( is-emb-map-emb g) - ( lem) - ( y) - ( γ) - x : X - x = pr1 (pr1 w) - p : map-emb f x ＝ y - p = pr2 (pr1 w) - ψ : - ( d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) → - map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y - ψ (inl v) = ex-falso ((pr2 w) v) - ψ (inr v) = p - b : - Σ ( X) - ( λ x → - ( (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) → - map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y)) - b = - a ( is-decidable-is-perfect-image-is-emb - ( is-emb-map-emb g) - ( lem) - ( map-emb g y)) - x : X - x = pr1 b - p : map-Cantor-Schröder-Bernstein-Escardó x ＝ y - p = pr2 b (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x) - - is-equiv-map-Cantor-Schröder-Bernstein-Escardó : - is-equiv map-Cantor-Schröder-Bernstein-Escardó - is-equiv-map-Cantor-Schröder-Bernstein-Escardó = - is-equiv-is-split-surjective-is-injective - map-Cantor-Schröder-Bernstein-Escardó - is-injective-map-Cantor-Schröder-Bernstein-Escardó - is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó - - Cantor-Schröder-Bernstein-Escardó : - type-Cantor-Schröder-Bernstein-Escardó l1 l2 - pr1 (Cantor-Schröder-Bernstein-Escardó f g) = - map-Cantor-Schröder-Bernstein-Escardó f g - pr2 (Cantor-Schröder-Bernstein-Escardó f g) = - is-equiv-map-Cantor-Schröder-Bernstein-Escardó f g + map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó : + (x : A) → is-decidable (is-perfect-image f g x) → B + map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + x (inl γ) = + inverse-of-perfect-image x γ + map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + x (inr nγ) = + f x + + compute-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó : + (y : B) → + (γ : is-perfect-image f g (g y)) → + (d : is-decidable (is-perfect-image f g (g y))) → + map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( g y) d ＝ + y + compute-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + y γ (inl v') = + is-retraction-inverse-of-perfect-image G' y v' + compute-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + y γ (inr v) = + ex-falso (v γ) + + compute-map-construction-is-not-perfect-image-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (y : B) → + (nγ : ¬ (is-perfect-image f g (g y))) → + (d : + is-decidable + ( is-perfect-image f g + ( element-has-nonperfect-fiber-is-not-perfect-image + G G' F F' y nγ))) → + map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( element-has-nonperfect-fiber-is-not-perfect-image G G' F F' y nγ) + ( d) ＝ + y + compute-map-construction-is-not-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y nγ (inl v) = + ex-falso + ( is-not-perfect-image-has-nonperfect-fiber-is-not-perfect-image + G G' F F' y nγ v) + compute-map-construction-is-not-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y nγ (inr _) = + is-in-fiber-element-has-nonperfect-fiber-is-not-perfect-image + G G' F F' y nγ + + map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (y : B) → is-decidable (is-perfect-image f g (g y)) → A + map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y (inl _) = g y + map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y (inr nγ) = + element-has-nonperfect-fiber-is-not-perfect-image G G' F F' y nγ + + is-section-map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (y : B) + (d : is-decidable (is-perfect-image f g (g y))) → + (d' : + is-decidable + ( is-perfect-image f g + ( map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y d))) → + map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y d) + ( d') ＝ + y + is-section-map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y (inl γ) = + compute-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + y γ + is-section-map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y (inr nγ) = + compute-map-construction-is-not-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' y nγ + + map-construction-Cantor-Schröder-Bernstein–Escardó : + (D : (x : A) → is-decidable (is-perfect-image f g x)) → A → B + map-construction-Cantor-Schröder-Bernstein–Escardó D x = + map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( x) + ( D x) + + map-section-construction-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (D : (y : B) → is-decidable (is-perfect-image f g (g y))) → B → A + map-section-construction-Cantor-Schröder-Bernstein–Escardó F' D y = + map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( F') + ( y) + ( D y) + + is-section-map-section-construction-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (D : (x : A) → is-decidable (is-perfect-image f g x)) → + is-section + ( map-construction-Cantor-Schröder-Bernstein–Escardó D) + ( map-section-construction-Cantor-Schröder-Bernstein–Escardó F' (D ∘ g)) + is-section-map-section-construction-Cantor-Schröder-Bernstein–Escardó F' D y = + is-section-map-section-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( F') + ( y) + ( D (g y)) + ( D ( map-section-construction-Cantor-Schröder-Bernstein–Escardó + F' (D ∘ g) y)) + + section-construction-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (D : (x : A) → is-decidable (is-perfect-image f g x)) → + section (map-construction-Cantor-Schröder-Bernstein–Escardó D) + section-construction-Cantor-Schröder-Bernstein–Escardó F' D = + map-section-construction-Cantor-Schröder-Bernstein–Escardó F' (D ∘ g) , + is-section-map-section-construction-Cantor-Schröder-Bernstein–Escardó F' D +``` + +Injectivity of the constructed map. + +```agda + is-injective-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó : + (F' : is-injective f) → + {x x' : A} + (d : is-decidable (is-perfect-image f g x)) + (d' : is-decidable (is-perfect-image f g x')) → + ( map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( x) + ( d)) ＝ + ( map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( x') + ( d')) → + x ＝ x' + is-injective-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' { x} {x'} (inl ρ) (inl ρ') p = + ( inv (is-section-inverse-of-perfect-image x ρ)) ∙ + ( ap g p ∙ + is-section-inverse-of-perfect-image x' ρ') + is-injective-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' {x} {x'} (inl ρ) (inr nρ') p = + ex-falso (perfect-image-has-distinct-image x' x nρ' ρ (inv p)) + is-injective-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' { x} {x'} (inr nρ) (inl ρ') p = + ex-falso (perfect-image-has-distinct-image x x' nρ ρ' p) + is-injective-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + F' {lx} {x'} (inr nρ) (inr nρ') p = F' p -- TODO: look for alternative approach avoiding `is-injective f` +``` + +Piecing it all together. + +```agda + is-equiv-map-construction-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (F'' : is-injective f) → + (D : (x : A) → is-decidable (is-perfect-image f g x)) → + is-equiv (map-construction-Cantor-Schröder-Bernstein–Escardó D) + is-equiv-map-construction-Cantor-Schröder-Bernstein–Escardó + F' F'' D = + is-equiv-is-injective + ( section-construction-Cantor-Schröder-Bernstein–Escardó F' D) + ( λ {x} {x'} → + is-injective-map-construction-is-decidable-is-perfect-image-Cantor-Schröder-Bernstein–Escardó + ( F'') + ( D x) + ( D x')) + + equiv-construction-Cantor-Schröder-Bernstein–Escardó : + (F' : is-π₀-trivial-map' f) → + (F'' : is-injective f) → + (D : (x : A) → is-decidable (is-perfect-image f g x)) → + A ≃ B + equiv-construction-Cantor-Schröder-Bernstein–Escardó F' F'' D = + map-construction-Cantor-Schröder-Bernstein–Escardó D , + is-equiv-map-construction-Cantor-Schröder-Bernstein–Escardó F' F'' D ``` -## Corollaries +## Theorem + +### The Cantor-Schröder-Bernstein theorem assuming the weak limited principle of omniscience + +It follows from the weak limited principle of omniscience that, for every pair +of mutual decidable embeddings `f : A ↪ B` and `g : B ↪ A`, it is decidable for +every element `x : A` whether `x` is a perfect image of `g` relative to `f`. + +Applying this fact to the Cantor-Schröder-Bernstein-Escardó construction, we +conclude that every pair of types that mutually embed into oneanother via +decidable embeddings are equivalent. + +In fact, it suffices to assume that `f` is decidable, π₀-trivial, and injective. + +```agda +abstract + is-decidable-is-perfect-image'-WLPO : + {l1 l2 : Level} (wlpo : level-WLPO (l1 ⊔ l2)) + {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} → + is-decidable-emb g → is-decidable-map f → is-π₀-trivial-map' f → + (a : A) → is-decidable (is-perfect-image' f g a) + is-decidable-is-perfect-image'-WLPO wlpo {f = f} {g} G F F' a = + wlpo + ( λ n → + is-perfect-image-at' f g a n , + is-decidable-prop-is-perfect-image-at' G F F' a n) + +is-decidable-is-perfect-image-WLPO : + {l1 l2 : Level} (wlpo : level-WLPO (l1 ⊔ l2)) + {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} → + is-decidable-emb g → is-decidable-map f → is-π₀-trivial-map' f → + (a : A) → is-decidable (is-perfect-image f g a) +is-decidable-is-perfect-image-WLPO wlpo {f = f} {g} G F F' a = + is-decidable-equiv' + ( compute-is-perfect-image f g a) + ( is-decidable-is-perfect-image'-WLPO wlpo G F F' a) +``` + +```agda +generalized-Cantor-Schröder-Bernstein-WLPO : + {l1 l2 : Level} → level-WLPO (l1 ⊔ l2) → + {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} → + is-decidable-emb g → + is-decidable-map f → is-π₀-trivial-map' f → is-injective f → + A ≃ B +generalized-Cantor-Schröder-Bernstein-WLPO wlpo G F F' F'' = + equiv-construction-Cantor-Schröder-Bernstein–Escardó + ( is-injective-is-decidable-emb G) + ( is-double-negation-eliminating-map-is-decidable-emb G) + ( is-double-negation-eliminating-map-is-decidable-map F) + ( F') + ( F'') + ( is-decidable-is-perfect-image-WLPO wlpo + ( G) + ( F) + ( F')) + +Cantor-Schröder-Bernstein-WLPO' : + {l1 l2 : Level} → level-WLPO (l1 ⊔ l2) → + {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} → + is-decidable-emb g → is-decidable-emb f → + A ≃ B +Cantor-Schröder-Bernstein-WLPO' wlpo G F = + generalized-Cantor-Schröder-Bernstein-WLPO wlpo G + ( is-decidable-map-is-decidable-emb F) + ( is-π₀-trivial-map'-is-emb (is-emb-is-decidable-emb F)) + ( is-injective-is-decidable-emb F) + +Cantor-Schröder-Bernstein-WLPO : + {l1 l2 : Level} → level-WLPO (l1 ⊔ l2) → + {A : UU l1} {B : UU l2} → (A ↪ᵈ B) → (B ↪ᵈ A) → A ≃ B +Cantor-Schröder-Bernstein-WLPO wlpo (f , F) (g , G) = + Cantor-Schröder-Bernstein-WLPO' wlpo G F +``` + +### The ε-generalized Cantor-Schröder-Bernstein-Escardó theorem + +Assuming the [law of exluded middle](foundation.law-of-excluded-middle.md), then +given two types `A` and `B` such that there is a π₀-trivial injection `A → B` +equipped with a Hilbert ε-operator, and an embedding `B ↪ A`, then `A` and `B` +are equivalent. + +```agda +ε-Cantor-Schröder-Bernstein-LEM : + {l1 l2 : Level} → LEM (l1 ⊔ l2) → + {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} + (G : is-emb g) → + (F : is-π₀-trivial-map' f) → + (F' : is-injective f) → + (εF : ε-operator-map-Hilbert f) → + A ≃ B +ε-Cantor-Schröder-Bernstein-LEM lem {f = f} {g} G F F' εF = + equiv-construction-Cantor-Schröder-Bernstein–Escardó + ( is-injective-is-emb G) + ( is-double-negation-eliminating-map-is-decidable-map + ( λ y → lem (fiber g y , is-prop-map-is-emb G y))) + ( λ y → + ( λ nnf → + εF + ( y) + ( double-negation-elim-is-decidable + ( lem (trunc-Prop (fiber f y))) + ( map-double-negation unit-trunc-Prop nnf)))) + ( F) + ( F') + ( lem ∘ is-perfect-image-Prop G) +``` + +### The Cantor-Schröder-Bernstein-Escardó theorem + +```agda +Cantor-Schröder-Bernstein-Escardó' : + {l1 l2 : Level} → LEM (l1 ⊔ l2) → + {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} → + is-emb g → is-emb f → A ≃ B +Cantor-Schröder-Bernstein-Escardó' lem {f = f} {g} G F = + Cantor-Schröder-Bernstein-WLPO' + ( λ P → lem (Π-Prop ℕ (prop-Decidable-Prop ∘ P))) + ( G , λ y → lem (fiber g y , is-prop-map-is-emb G y)) + ( F , λ y → lem (fiber f y , is-prop-map-is-emb F y)) + +Cantor-Schröder-Bernstein-Escardó : + {l1 l2 : Level} → LEM (l1 ⊔ l2) → + {A : UU l1} {B : UU l2} → + A ↪ B → B ↪ A → A ≃ B +Cantor-Schröder-Bernstein-Escardó lem (f , F) (g , G) = + Cantor-Schröder-Bernstein-Escardó' lem G F +``` ### The Cantor–Schröder–Bernstein theorem diff --git a/src/foundation/decidable-dependent-function-types.lagda.md b/src/foundation/decidable-dependent-function-types.lagda.md index c63c6ddeea..36fbf97559 100644 --- a/src/foundation/decidable-dependent-function-types.lagda.md +++ b/src/foundation/decidable-dependent-function-types.lagda.md @@ -7,9 +7,15 @@ module foundation.decidable-dependent-function-types where
Imports ```agda +open import foundation.decidable-propositions open import foundation.decidable-types +open import foundation.dependent-pair-types open import foundation.functoriality-dependent-function-types open import foundation.maybe +open import foundation.mere-equality +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.transport-along-identifications open import foundation.uniformly-decidable-type-families open import foundation.universal-property-coproduct-types open import foundation.universal-property-maybe @@ -20,6 +26,8 @@ open import foundation-core.empty-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.negation + +open import logic.propositionally-decidable-types ```
@@ -46,6 +54,28 @@ is-decidable-Π-uniformly-decidable-family (inl a) (inr b) = inr (λ f → b a (f a)) is-decidable-Π-uniformly-decidable-family (inr na) _ = inl (ex-falso ∘ na) + +is-decidable-prop-Π-uniformly-decidable-family : + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → + is-decidable A → + is-uniformly-decidable-family B → + ((x : A) → is-prop (B x)) → + is-decidable-prop ((a : A) → (B a)) +is-decidable-prop-Π-uniformly-decidable-family dA dB H = + ( is-prop-Π H , is-decidable-Π-uniformly-decidable-family dA dB) + +abstract + is-decidable-prop-Π-uniformly-decidable-family' : + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → + is-inhabited-or-empty A → + is-uniformly-decidable-family B → + ((x : A) → is-prop (B x)) → + is-decidable-prop ((a : A) → (B a)) + is-decidable-prop-Π-uniformly-decidable-family' {A = A} {B} dA dB H = + elim-is-inhabited-or-empty-Prop' + ( is-decidable-prop-Prop ((a : A) → (B a))) + ( λ d → is-decidable-prop-Π-uniformly-decidable-family d dB H) + ( dA) ``` ### Decidablitilty of dependent products over coproducts @@ -76,6 +106,43 @@ is-decidable-Π-Maybe {B = B} du de = ( is-decidable-product du de) ``` +### Dependent products of decidable propositions over a π₀-trivial base are decidable propositions + +Assuming the base `A` is empty or 0-connected, a dependent product of decidable +propositions over `A` is again a decidable proposition. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (B : A → Decidable-Prop l2) + where + + is-decidable-Π-all-elements-merely-equal-base : + all-elements-merely-equal A → + is-decidable A → + is-decidable ((x : A) → type-Decidable-Prop (B x)) + is-decidable-Π-all-elements-merely-equal-base H dA = + is-decidable-Π-uniformly-decidable-family dA + ( is-uniformly-decidable-family-all-elements-merely-equal-base B H dA) + + is-decidable-prop-Π-all-elements-merely-equal-base : + all-elements-merely-equal A → + is-decidable A → + is-decidable-prop ((x : A) → type-Decidable-Prop (B x)) + is-decidable-prop-Π-all-elements-merely-equal-base H dA = + is-decidable-prop-Π-uniformly-decidable-family dA + ( is-uniformly-decidable-family-all-elements-merely-equal-base B H dA) + ( is-prop-type-Decidable-Prop ∘ B) + + is-decidable-prop-Π-all-elements-merely-equal-base' : + all-elements-merely-equal A → + is-inhabited-or-empty A → + is-decidable-prop ((x : A) → type-Decidable-Prop (B x)) + is-decidable-prop-Π-all-elements-merely-equal-base' H dA = + is-decidable-prop-Π-uniformly-decidable-family' dA + ( is-uniformly-decidable-family-all-elements-merely-equal-base' B H dA) + ( is-prop-type-Decidable-Prop ∘ B) +``` + ### Decidability of dependent products over an equivalence ```agda diff --git a/src/foundation/decidable-dependent-pair-types.lagda.md b/src/foundation/decidable-dependent-pair-types.lagda.md index 4af4b5e568..557af60d5f 100644 --- a/src/foundation/decidable-dependent-pair-types.lagda.md +++ b/src/foundation/decidable-dependent-pair-types.lagda.md @@ -9,7 +9,11 @@ module foundation.decidable-dependent-pair-types where ```agda open import foundation.decidable-types open import foundation.dependent-pair-types +open import foundation.empty-types open import foundation.maybe +open import foundation.mere-equality +open import foundation.propositional-truncations +open import foundation.transport-along-identifications open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-unit-type open import foundation.uniformly-decidable-type-families @@ -20,6 +24,8 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.negation + +open import logic.propositionally-decidable-types ``` @@ -32,6 +38,21 @@ We describe conditions under which ## Properites +### Decidability of dependent sums over equivalences + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} {D : B → UU l4} + (e : A ≃ B) (f : (x : A) → C x ≃ D (map-equiv e x)) + where + + is-decidable-Σ-equiv : is-decidable (Σ A C) → is-decidable (Σ B D) + is-decidable-Σ-equiv = is-decidable-equiv' (equiv-Σ D e f) + + is-decidable-Σ-equiv' : is-decidable (Σ B D) → is-decidable (Σ A C) + is-decidable-Σ-equiv' = is-decidable-equiv (equiv-Σ D e f) +``` + ### Dependent sums of a uniformly decidable family of types ```agda @@ -66,24 +87,58 @@ is-decidable-Σ-coproduct {A = A} {B} C dA dB = ```agda is-decidable-Σ-Maybe : {l1 l2 : Level} {A : UU l1} {B : Maybe A → UU l2} → - is-decidable (Σ A (B ∘ unit-Maybe)) → is-decidable (B exception-Maybe) → + is-decidable (Σ A (B ∘ unit-Maybe)) → + is-decidable (B exception-Maybe) → is-decidable (Σ (Maybe A) B) is-decidable-Σ-Maybe {A = A} {B} dA de = is-decidable-Σ-coproduct B dA ( is-decidable-equiv (left-unit-law-Σ (B ∘ inr)) de) ``` -### Decidability of dependent sums over equivalences +### Decidability of dependent sums over π₀-trivial bases ```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} {D : B → UU l4} - (e : A ≃ B) (f : (x : A) → C x ≃ D (map-equiv e x)) - where - - is-decidable-Σ-equiv : is-decidable (Σ A C) → is-decidable (Σ B D) - is-decidable-Σ-equiv = is-decidable-equiv' (equiv-Σ D e f) - - is-decidable-Σ-equiv' : is-decidable (Σ B D) → is-decidable (Σ A C) - is-decidable-Σ-equiv' = is-decidable-equiv (equiv-Σ D e f) +is-decidable-Σ-all-elements-merely-equal-base : + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → + all-elements-merely-equal A → + is-decidable A → + ((x : A) → is-decidable (B x)) → + is-decidable (Σ A B) +is-decidable-Σ-all-elements-merely-equal-base {B = B} H (inl x) K = + rec-coproduct + ( λ y → inl (x , y)) + ( λ ny → + inr + ( λ ab → + rec-trunc-Prop + ( empty-Prop) + ( λ p → ny (tr B p (pr2 ab))) + ( H (pr1 ab) x))) + ( K x) +is-decidable-Σ-all-elements-merely-equal-base H (inr nx) K = + inr (map-neg pr1 nx) + +is-inhabited-or-empty-Σ-all-elements-merely-equal-base : + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → + all-elements-merely-equal A → + is-inhabited-or-empty A → + ((x : A) → is-inhabited-or-empty (B x)) → + is-inhabited-or-empty (Σ A B) +is-inhabited-or-empty-Σ-all-elements-merely-equal-base {A = A} {B} H dA dB = + elim-is-inhabited-or-empty-Prop + ( is-inhabited-or-empty-Prop (Σ A B)) + ( λ a → + elim-is-inhabited-or-empty-Prop + ( is-inhabited-or-empty-Prop (Σ A B)) + ( λ b → inl (unit-trunc-Prop (a , b))) + ( λ nb → + inr + ( λ x → + rec-trunc-Prop + ( empty-Prop) + ( λ p → nb (tr B p (pr2 x))) + ( H (pr1 x) a))) + ( dB a)) + ( λ na → inr (map-neg pr1 na)) + ( dA) ``` diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md index f4780285bd..3d6225f33b 100644 --- a/src/foundation/decidable-embeddings.lagda.md +++ b/src/foundation/decidable-embeddings.lagda.md @@ -54,7 +54,7 @@ if it is an [embedding](foundation-core.embeddings.md) and its Equivalently, a decidable embedding is a map whose fibers are [decidable propositions](foundation-core.decidable-propositions.md). We refer to this condition as being a -{{#concept "decidably propositional map" Disambiguation="of types" Agda=is-decidable-prop-map}}. +{{#concept "decidable propositional map" Disambiguation="of types" Agda=is-decidable-prop-map}}. ## Definitions @@ -81,7 +81,7 @@ is-injective-is-decidable-emb : is-injective-is-decidable-emb = is-injective-is-emb ∘ is-emb-is-decidable-emb ``` -### Decidably propositional maps +### Decidable propositional maps ```agda module _ @@ -140,6 +140,11 @@ module _ is-decidable-map-map-decidable-emb = is-decidable-map-is-decidable-emb is-decidable-emb-map-decidable-emb + is-injective-map-decidable-emb : + is-injective map-decidable-emb + is-injective-map-decidable-emb = + is-injective-is-decidable-emb is-decidable-emb-map-decidable-emb + emb-decidable-emb : X ↪ Y emb-decidable-emb = map-decidable-emb , is-emb-map-decidable-emb ``` diff --git a/src/foundation/decidable-maps.lagda.md b/src/foundation/decidable-maps.lagda.md index 926253c0dc..e1b03edc3c 100644 --- a/src/foundation/decidable-maps.lagda.md +++ b/src/foundation/decidable-maps.lagda.md @@ -7,16 +7,23 @@ module foundation.decidable-maps where
Imports ```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.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 @@ -28,6 +35,7 @@ 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 ``` @@ -41,7 +49,7 @@ A [map](foundation-core.function-types.md) is said to be its [fibers](foundation-core.fibers-of-maps.md) are [decidable types](foundation.decidable-types.md). -## Definition +## Definitions ### The structure on a map of decidability @@ -91,6 +99,43 @@ abstract ( K b) ``` +### Maps with sections are decidable + +```agda +is-decidable-map-section : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + (i : A → B) → section i → is-decidable-map i +is-decidable-map-section i (s , S) b = inl (s b , S b) +``` + +### Any map out of the empty type is decidable + +```agda +abstract + is-decidable-map-ex-falso : + {l : Level} {X : UU l} → is-decidable-map (ex-falso {l} {X}) + is-decidable-map-ex-falso x = inr pr1 +``` + +### The identity map is decidable + +```agda +abstract + is-decidable-map-id : + {l : Level} {X : UU l} → is-decidable-map (id {l} {X}) + is-decidable-map-id y = inl (y , refl) +``` + +### Equivalences are decidable maps + +```agda +abstract + is-decidable-map-is-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → + is-equiv f → is-decidable-map f + is-decidable-map-is-equiv H x = inl (center (is-contr-map-is-equiv H x)) +``` + ### Composition of decidable maps The composite `g ∘ f` of two decidable maps is decidable if `g` is injective. @@ -118,6 +163,41 @@ module _ ( G x) ``` +The composite `g ∘ f` of two decidable maps is decidable if `g` is π₀-trivial. + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {g : B → C} {f : A → B} + where + + abstract + is-decidable-map-comp-is-π₀-trivial-map' : + is-π₀-trivial-map' g → + is-decidable-map g → + is-decidable-map f → + is-decidable-map (g ∘ f) + is-decidable-map-comp-is-π₀-trivial-map' H G F x = + is-decidable-equiv + ( compute-fiber-comp g f x) + ( is-decidable-Σ-all-elements-merely-equal-base (H x) (G x) (F ∘ pr1)) + +module _ + {l1 : Level} {A : UU l1} {f : A → A} + (is-decidable-f : is-decidable-map f) + (is-π₀-trivial-f : is-π₀-trivial-map' f) + where + + is-decidable-map-iterate-is-π₀-trivial-map' : + (n : ℕ) → is-decidable-map (iterate n f) + is-decidable-map-iterate-is-π₀-trivial-map' zero-ℕ = is-decidable-map-id + is-decidable-map-iterate-is-π₀-trivial-map' (succ-ℕ n) = + is-decidable-map-comp-is-π₀-trivial-map' + ( is-π₀-trivial-f) + ( is-decidable-f) + ( is-decidable-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. @@ -150,43 +230,6 @@ is-decidable-map-retraction d i (r , R) b = ( d (i (r b)) b) ``` -### Maps with sections are decidable - -```agda -is-decidable-map-section : - {l1 l2 : Level} {A : UU l1} {B : UU l2} → - (i : A → B) → section i → is-decidable-map i -is-decidable-map-section i (s , S) b = inl (s b , S b) -``` - -### Any map out of the empty type is decidable - -```agda -abstract - is-decidable-map-ex-falso : - {l : Level} {X : UU l} → is-decidable-map (ex-falso {l} {X}) - is-decidable-map-ex-falso x = inr pr1 -``` - -### The identity map is decidable - -```agda -abstract - is-decidable-map-id : - {l : Level} {X : UU l} → is-decidable-map (id {l} {X}) - is-decidable-map-id y = inl (y , refl) -``` - -### Equivalences are decidable maps - -```agda -abstract - is-decidable-map-is-equiv : - {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → - is-equiv f → is-decidable-map f - is-decidable-map-is-equiv H x = inl (center (is-contr-map-is-equiv H x)) -``` - ### The map on total spaces induced by a family of decidable maps is decidable ```agda diff --git a/src/foundation/decidable-propositions.lagda.md b/src/foundation/decidable-propositions.lagda.md index c6c5bfb814..433d00c75d 100644 --- a/src/foundation/decidable-propositions.lagda.md +++ b/src/foundation/decidable-propositions.lagda.md @@ -9,6 +9,7 @@ open import foundation-core.decidable-propositions public
Imports ```agda +open import foundation.0-connected-types open import foundation.action-on-identifications-functions open import foundation.booleans open import foundation.decidable-types diff --git a/src/foundation/decidable-types.lagda.md b/src/foundation/decidable-types.lagda.md index 93bdd1707e..a18f714f17 100644 --- a/src/foundation/decidable-types.lagda.md +++ b/src/foundation/decidable-types.lagda.md @@ -13,6 +13,7 @@ open import foundation.dependent-pair-types open import foundation.double-negation open import foundation.empty-types open import foundation.equivalences +open import foundation.evaluation-functions open import foundation.hilberts-epsilon-operators open import foundation.logical-equivalences open import foundation.negation @@ -45,7 +46,7 @@ of logic into type theory. A related concept is that a type is either type is expressed using the [propositional truncation](foundation.propositional-truncations.md). -## Definition +## Definitions ### The Curry–Howard interpretation of decidability @@ -58,29 +59,6 @@ is-decidable-fam : is-decidable-fam {A = A} P = (x : A) → is-decidable (P x) ``` -### The predicate that a type is inhabited or empty - -```agda -is-inhabited-or-empty : {l1 : Level} → UU l1 → UU l1 -is-inhabited-or-empty A = type-trunc-Prop A + is-empty A -``` - -### Merely decidable types - -A type `A` is said to be -{{#concept "merely decidable" Agda=is-merely-decidable}} if it comes equipped -with an element of `║ is-decidable A ║₋₁`, or equivalently, the -[disjunction](foundation.disjunction.md) `A ∨ ¬ A` holds. - -```agda -is-merely-decidable-Prop : - {l : Level} → UU l → Prop l -is-merely-decidable-Prop A = trunc-Prop (is-decidable A) - -is-merely-decidable : {l : Level} → UU l → UU l -is-merely-decidable A = type-trunc-Prop (is-decidable A) -``` - ## Examples ### The unit type and the empty type are decidable @@ -112,7 +90,7 @@ is-decidable-coproduct (inr na) (inr nb) = inr (rec-coproduct na nb) is-decidable-product : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-decidable A → is-decidable B → is-decidable (A × B) -is-decidable-product (inl a) (inl b) = inl (pair a b) +is-decidable-product (inl a) (inl b) = inl (a , b) is-decidable-product (inl a) (inr g) = inr (g ∘ pr2) is-decidable-product (inr f) (inl b) = inr (f ∘ pr1) is-decidable-product (inr f) (inr g) = inr (f ∘ pr1) @@ -120,22 +98,21 @@ is-decidable-product (inr f) (inr g) = inr (f ∘ pr1) is-decidable-product' : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-decidable A → (A → is-decidable B) → is-decidable (A × B) -is-decidable-product' (inl a) d with d a -... | inl b = inl (pair a b) -... | inr nb = inr (nb ∘ pr2) +is-decidable-product' (inl a) d = + rec-coproduct (λ b → inl (a , b)) (λ nb → inr (nb ∘ pr2)) (d a) is-decidable-product' (inr na) d = inr (na ∘ pr1) is-decidable-left-factor : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-decidable (A × B) → B → is-decidable A -is-decidable-left-factor (inl (pair x y)) b = inl x -is-decidable-left-factor (inr f) b = inr (λ a → f (pair a b)) +is-decidable-left-factor (inl (x , y)) b = inl x +is-decidable-left-factor (inr f) b = inr (λ a → f (a , b)) is-decidable-right-factor : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-decidable (A × B) → A → is-decidable B -is-decidable-right-factor (inl (pair x y)) a = inl y -is-decidable-right-factor (inr f) a = inr (λ b → f (pair a b)) +is-decidable-right-factor (inl (x , y)) a = inl y +is-decidable-right-factor (inr f) a = inr (λ b → f (a , b)) ``` ### Function types of decidable types are decidable @@ -144,16 +121,15 @@ is-decidable-right-factor (inr f) a = inr (λ b → f (pair a b)) is-decidable-function-type : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-decidable A → is-decidable B → is-decidable (A → B) -is-decidable-function-type (inl a) (inl b) = inl (λ x → b) -is-decidable-function-type (inl a) (inr g) = inr (λ h → g (h a)) +is-decidable-function-type (inl a) (inl b) = inl (λ _ → b) +is-decidable-function-type (inl a) (inr nb) = inr (map-neg (ev a) nb) is-decidable-function-type (inr f) _ = inl (ex-falso ∘ f) is-decidable-function-type' : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-decidable A → (A → is-decidable B) → is-decidable (A → B) -is-decidable-function-type' (inl a) d with d a -... | inl b = inl (λ x → b) -... | inr nb = inr (λ f → nb (f a)) +is-decidable-function-type' (inl a) d = + rec-coproduct (λ b → inl (λ _ → b)) (λ nb → inr (map-neg (ev a) nb)) (d a) is-decidable-function-type' (inr na) d = inl (ex-falso ∘ na) ``` @@ -296,23 +272,6 @@ idempotent-is-decidable P (inl (inr np)) = inr np idempotent-is-decidable P (inr np) = inr (λ p → np (inl p)) ``` -### Being inhabited or empty is a proposition - -```agda -abstract - is-property-is-inhabited-or-empty : - {l1 : Level} (A : UU l1) → is-prop (is-inhabited-or-empty A) - is-property-is-inhabited-or-empty A = - is-prop-coproduct - ( λ t → apply-universal-property-trunc-Prop t empty-Prop) - ( is-prop-type-trunc-Prop) - ( is-prop-neg) - -is-inhabited-or-empty-Prop : {l1 : Level} → UU l1 → Prop l1 -pr1 (is-inhabited-or-empty-Prop A) = is-inhabited-or-empty A -pr2 (is-inhabited-or-empty-Prop A) = is-property-is-inhabited-or-empty A -``` - ### Any inhabited type is a fixed point for `is-decidable` ```agda @@ -333,51 +292,6 @@ module _ is-decidable-raise = is-decidable-equiv' (compute-raise l A) ``` -### Decidable types are inhabited or empty - -```agda -is-inhabited-or-empty-is-decidable : - {l : Level} {A : UU l} → is-decidable A → is-inhabited-or-empty A -is-inhabited-or-empty-is-decidable (inl x) = inl (unit-trunc-Prop x) -is-inhabited-or-empty-is-decidable (inr y) = inr y -``` - -### Decidable types are merely decidable - -```agda -is-merely-decidable-is-decidable : - {l : Level} {A : UU l} → is-decidable A → is-merely-decidable A -is-merely-decidable-is-decidable = unit-trunc-Prop -``` - -### Types are inhabited or empty if and only if they are merely decidable - -```agda -module _ - {l : Level} {A : UU l} - where - - is-inhabited-or-empty-is-merely-decidable : - is-merely-decidable A → is-inhabited-or-empty A - is-inhabited-or-empty-is-merely-decidable = - rec-trunc-Prop - ( is-inhabited-or-empty-Prop A) - ( is-inhabited-or-empty-is-decidable) - - is-merely-decidable-is-inhabited-or-empty : - is-inhabited-or-empty A → is-merely-decidable A - is-merely-decidable-is-inhabited-or-empty (inl |x|) = - rec-trunc-Prop (is-merely-decidable-Prop A) (unit-trunc-Prop ∘ inl) |x| - is-merely-decidable-is-inhabited-or-empty (inr y) = - unit-trunc-Prop (inr y) - - iff-is-inhabited-or-empty-is-merely-decidable : - is-merely-decidable A ↔ is-inhabited-or-empty A - iff-is-inhabited-or-empty-is-merely-decidable = - ( is-inhabited-or-empty-is-merely-decidable , - is-merely-decidable-is-inhabited-or-empty) -``` - ## See also - That decidablity is irrefutable is shown in diff --git a/src/foundation/disjunction.lagda.md b/src/foundation/disjunction.lagda.md index 21a764be49..136e6d62f9 100644 --- a/src/foundation/disjunction.lagda.md +++ b/src/foundation/disjunction.lagda.md @@ -22,6 +22,8 @@ open import foundation-core.empty-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.propositions + +open import logic.propositionally-decidable-types ```
@@ -308,7 +310,6 @@ module _ is-decidable A → is-decidable B → is-decidable (disjunction-type A B) is-decidable-disjunction is-decidable-A is-decidable-B = is-decidable-trunc-Prop-is-merely-decidable - ( A + B) ( unit-trunc-Prop (is-decidable-coproduct is-decidable-A is-decidable-B)) module _ diff --git a/src/foundation/functoriality-truncation.lagda.md b/src/foundation/functoriality-truncation.lagda.md index 92e1760616..3708abf21b 100644 --- a/src/foundation/functoriality-truncation.lagda.md +++ b/src/foundation/functoriality-truncation.lagda.md @@ -131,7 +131,7 @@ module _ ( preserves-comp-map-trunc k (map-inv-equiv e) (map-equiv e)) ∙h ( htpy-trunc (is-retraction-map-inv-equiv e) ∙h id-map-trunc k)) - equiv-trunc : (type-trunc k A ≃ type-trunc k B) + equiv-trunc : type-trunc k A ≃ type-trunc k B pr1 equiv-trunc = map-equiv-trunc pr2 equiv-trunc = is-equiv-map-equiv-trunc ``` diff --git a/src/foundation/iterating-functions.lagda.md b/src/foundation/iterating-functions.lagda.md index 339d4eed0c..3898565cd9 100644 --- a/src/foundation/iterating-functions.lagda.md +++ b/src/foundation/iterating-functions.lagda.md @@ -2,6 +2,8 @@ ```agda module foundation.iterating-functions where + +open import foundation-core.iterating-functions public ```
Imports @@ -17,10 +19,12 @@ open import foundation.action-on-higher-identifications-functions open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.function-extensionality +open import foundation.subtypes open import foundation.universe-levels open import foundation-core.commuting-squares-of-maps open import foundation-core.endomorphisms +open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.sets @@ -32,71 +36,12 @@ open import group-theory.monoid-actions ## Idea -Any map `f : X → X` can be iterated by repeatedly applying `f` - -## Definition - -### Iterating functions - -```agda -module _ - {l : Level} {X : UU l} - where - - iterate : ℕ → (X → X) → (X → X) - iterate zero-ℕ f x = x - iterate (succ-ℕ k) f x = f (iterate k f x) - - iterate' : ℕ → (X → X) → (X → X) - iterate' zero-ℕ f x = x - iterate' (succ-ℕ k) f x = iterate' k f (f x) -``` - -### Homotopies of iterating functions - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (s : A → A) (t : B → B) - where - - coherence-square-iterate : - {f : A → B} (H : coherence-square-maps f s t f) → - (n : ℕ) → coherence-square-maps f (iterate n s) (iterate n t) f - coherence-square-iterate {f} H zero-ℕ x = refl - coherence-square-iterate {f} H (succ-ℕ n) = - pasting-vertical-coherence-square-maps - ( f) - ( iterate n s) - ( iterate n t) - ( f) - ( s) - ( t) - ( f) - ( coherence-square-iterate H n) - ( H) -``` +Any map `f : X → X` can be +{{#concept "iterated" Disambiguation="endo map of types"}} by repeatedly +applying `f`. ## Properties -### The two definitions of iterating are homotopic - -```agda -module _ - {l : Level} {X : UU l} - where - - reassociate-iterate-succ-ℕ : - (k : ℕ) (f : X → X) (x : X) → iterate (succ-ℕ k) f x ＝ iterate k f (f x) - reassociate-iterate-succ-ℕ zero-ℕ f x = refl - reassociate-iterate-succ-ℕ (succ-ℕ k) f x = - ap f (reassociate-iterate-succ-ℕ k f x) - - reassociate-iterate : (k : ℕ) (f : X → X) → iterate k f ~ iterate' k f - reassociate-iterate zero-ℕ f x = refl - reassociate-iterate (succ-ℕ k) f x = - reassociate-iterate-succ-ℕ k f x ∙ reassociate-iterate k f (f x) -``` - ### For any map `f : X → X`, iterating `f` defines a monoid action of ℕ on `X` ```agda diff --git a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md index 242c9b27b6..e0ef1ebe49 100644 --- a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md +++ b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md @@ -13,17 +13,20 @@ open import elementary-number-theory.parity-natural-numbers open import foundation.booleans open import foundation.dependent-pair-types open import foundation.disjunction +open import foundation.negation open import foundation.universal-quantification open import foundation.universe-levels +open import foundation-core.decidable-propositions open import foundation-core.fibers-of-maps +open import foundation-core.function-types open import foundation-core.propositions open import foundation-core.sets ```
-## Statement +## Idea The {{#concept "lesser limited principle of omniscience" Agda=LLPO}} (LLPO) asserts that for any [sequence](foundation.sequences.md) of @@ -31,9 +34,13 @@ asserts that for any [sequence](foundation.sequences.md) of [at most one](foundation-core.propositions.md) `n`, then either `f n` is false for all even `n` or `f n` is false for all odd `n`. +## Definitions + +### The small lesser limited principle of omniscience + ```agda -prop-LLPO : Prop lzero -prop-LLPO = +prop-bool-LLPO : Prop lzero +prop-bool-LLPO = ∀' ( ℕ → bool) ( λ f → @@ -43,11 +50,47 @@ prop-LLPO = ( ∀' ℕ (λ n → function-Prop (is-even-ℕ n) (is-false-Prop (f n)))) ( ∀' ℕ (λ n → function-Prop (is-odd-ℕ n) (is-false-Prop (f n)))))) -LLPO : UU lzero -LLPO = type-Prop prop-LLPO +bool-LLPO : UU lzero +bool-LLPO = type-Prop prop-bool-LLPO + +is-prop-bool-LLPO : is-prop bool-LLPO +is-prop-bool-LLPO = is-prop-type-Prop prop-bool-LLPO +``` + +### The lesser limited principle of omniscience with respect to a universe level + +```agda +prop-level-LLPO : (l : Level) → Prop (lsuc l) +prop-level-LLPO l = + ∀' + ( ℕ → Decidable-Prop l) + ( λ f → + function-Prop + ( is-prop (Σ ℕ (type-Decidable-Prop ∘ f))) + ( disjunction-Prop + ( ∀' ℕ + ( λ n → + function-Prop + ( is-even-ℕ n) + ( neg-Prop (prop-Decidable-Prop (f n))))) + ( ∀' ℕ + ( λ n → + function-Prop + ( is-odd-ℕ n) + ( neg-Prop (prop-Decidable-Prop (f n))))))) + +level-LLPO : (l : Level) → UU (lsuc l) +level-LLPO l = type-Prop (prop-level-LLPO l) -is-prop-LLPO : is-prop LLPO -is-prop-LLPO = is-prop-type-Prop prop-LLPO +is-prop-level-LLPO : {l : Level} → is-prop (level-LLPO l) +is-prop-level-LLPO {l} = is-prop-type-Prop (prop-level-LLPO l) +``` + +### The lesser limited principle of omniscience + +```agda +LLPO : UUω +LLPO = {l : Level} → level-LLPO l ``` ## See also diff --git a/src/foundation/maps-with-hilbert-epsilon-operators.lagda.md b/src/foundation/maps-with-hilbert-epsilon-operators.lagda.md new file mode 100644 index 0000000000..2d83b0d4ef --- /dev/null +++ b/src/foundation/maps-with-hilbert-epsilon-operators.lagda.md @@ -0,0 +1,37 @@ +# Maps with Hilbert ε-operators + +```agda +module foundation.maps-with-hilbert-epsilon-operators where +``` + +
Imports + +```agda +open import foundation.hilberts-epsilon-operators +open import foundation.universe-levels + +open import foundation-core.fibers-of-maps +``` + +
+ +## Idea + +We consider maps `f : A → B` [equippes](foundation.structure.md) with +[Hilbert ε-operators](foundation.hilberts-epsilon-operators.md) on its +[fibers](foundation-core.fibers-of-maps.md). I.e., for every `y : B` there is an +operator + +```text + ε_y : ║ fiber f y ║₋₁ → fiber f y +``` + +## Definitions + +### The structure of an Hilbert ε-operator on a map + +```agda +ε-operator-map-Hilbert : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) +ε-operator-map-Hilbert {B = B} f = (y : B) → ε-operator-Hilbert (fiber f y) +``` diff --git a/src/foundation/mere-equality.lagda.md b/src/foundation/mere-equality.lagda.md index c36b3c92e0..44b9848f13 100644 --- a/src/foundation/mere-equality.lagda.md +++ b/src/foundation/mere-equality.lagda.md @@ -10,9 +10,13 @@ module foundation.mere-equality where open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences open import foundation.functoriality-propositional-truncation open import foundation.propositional-truncations open import foundation.reflecting-maps-equivalence-relations +open import foundation.retracts-of-types +open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.equivalence-relations @@ -28,7 +32,7 @@ open import foundation-core.sets Two elements in a type are said to be merely equal if there is an element of the propositionally truncated identity type between them. -## Definition +## Definitions ```agda module _ @@ -45,6 +49,13 @@ module _ is-prop-mere-eq x y = is-prop-type-trunc-Prop ``` +### Types whose elements are merely equal + +```agda +all-elements-merely-equal : {l : Level} → UU l → UU l +all-elements-merely-equal A = (x y : A) → mere-eq x y +``` + ## Properties ### Reflexivity @@ -54,6 +65,10 @@ abstract refl-mere-eq : {l : Level} {A : UU l} → is-reflexive (mere-eq {l} {A}) refl-mere-eq _ = unit-trunc-Prop refl + +mere-eq-eq : + {l : Level} {A : UU l} {x y : A} → x ＝ y → mere-eq x y +mere-eq-eq = unit-trunc-Prop ``` ### Symmetry @@ -121,3 +136,50 @@ is-set-mere-eq-in-id = ( is-prop-mere-eq) ( refl-mere-eq) ``` + +### Retracts of types with mere equality + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + all-elements-merely-equal-retract-of : + B retract-of A → all-elements-merely-equal A → all-elements-merely-equal B + all-elements-merely-equal-retract-of (i , r , R) H x y = + rec-trunc-Prop + ( mere-eq-Prop x y) + ( λ p → unit-trunc-Prop (inv (R x) ∙ ap r p ∙ R y)) + ( H (i x) (i y)) + + all-elements-merely-equal-equiv : + B ≃ A → all-elements-merely-equal A → all-elements-merely-equal B + all-elements-merely-equal-equiv e = + all-elements-merely-equal-retract-of (retract-equiv e) + + all-elements-merely-equal-equiv' : + A ≃ B → all-elements-merely-equal A → all-elements-merely-equal B + all-elements-merely-equal-equiv' e = + all-elements-merely-equal-retract-of (retract-inv-equiv e) +``` + +### Dependent sums of types with mere equality + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + (mA : all-elements-merely-equal A) + (mB : (x : A) → all-elements-merely-equal (B x)) + where + + all-elements-merely-equal-Σ : all-elements-merely-equal (Σ A B) + all-elements-merely-equal-Σ x y = + rec-trunc-Prop + ( mere-eq-Prop x y) + ( λ p → + rec-trunc-Prop + ( mere-eq-Prop x y) + ( λ q → unit-trunc-Prop (eq-pair-Σ p q)) + ( mB (pr1 y) (tr B p (pr2 x)) (pr2 y))) + ( mA (pr1 x) (pr1 y)) +``` diff --git a/src/foundation/perfect-images.lagda.md b/src/foundation/perfect-images.lagda.md index 73b8c53e54..121b422985 100644 --- a/src/foundation/perfect-images.lagda.md +++ b/src/foundation/perfect-images.lagda.md @@ -10,20 +10,35 @@ module foundation.perfect-images where open import elementary-number-theory.natural-numbers open import foundation.action-on-identifications-functions +open import foundation.connected-maps +open import foundation.coproduct-types +open import foundation.decidable-dependent-function-types +open import foundation.decidable-embeddings +open import foundation.decidable-maps +open import foundation.decidable-propositions open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.double-negation +open import foundation.double-negation-stable-propositions +open import foundation.functoriality-dependent-function-types +open import foundation.inhabited-types open import foundation.iterated-dependent-product-types open import foundation.iterating-functions open import foundation.law-of-excluded-middle +open import foundation.mere-equality open import foundation.negated-equality open import foundation.negation +open import foundation.pi-0-trivial-maps +open import foundation.propositional-truncations +open import foundation.type-arithmetic-dependent-function-types +open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels +open import foundation.weak-limited-principle-of-omniscience open import foundation-core.cartesian-product-types -open import foundation-core.coproduct-types open import foundation-core.embeddings 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.identity-types @@ -31,6 +46,12 @@ open import foundation-core.injective-maps open import foundation-core.propositional-maps open import foundation-core.propositions open import foundation-core.transport-along-identifications + +open import logic.double-negation-eliminating-maps +open import logic.double-negation-elimination +open import logic.double-negation-stable-embeddings +open import logic.propositionally-decidable-maps +open import logic.propositionally-double-negation-eliminating-maps ```
@@ -45,11 +66,14 @@ also the following chain a₀ --> f (a₀) --> g(f(a₀)) --> f(g(f(a₀))) --> ... --> (g ◦ f)ⁿ(a₀) ＝ a ``` -We say `a₀` is an {{#concept "origin"}} for `a`, and `a` is a -{{#concept "perfect image" Agda=is-perfect-image}} for `g` if any origin of `a` -is in the [image](foundation.images.md) of `g`. +We say `a₀` is an {{#concept "origin" Disambiguation="perfect image"}} for `a`, +and `a` is a {{#concept "perfect image" Agda=is-perfect-image}} for `g` +_relative to `f`_ if any origin of `a` is in the [image](foundation.images.md) +of `g`. + +## Definitions -## Definition +### Perfect images ```agda module _ @@ -58,88 +82,145 @@ module _ is-perfect-image : (a : A) → UU (l1 ⊔ l2) is-perfect-image a = - (a₀ : A) (n : ℕ) → (iterate n (g ∘ f)) a₀ ＝ a → fiber g a₀ + (a₀ : A) (n : ℕ) → iterate n (g ∘ f) a₀ ＝ a → fiber g a₀ ``` -## Properties +An alternative but equivalent definition. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + is-perfect-image-at' : A → ℕ → UU (l1 ⊔ l2) + is-perfect-image-at' a n = (p : fiber (iterate n (g ∘ f)) a) → fiber g (pr1 p) + + is-perfect-image' : (a : A) → UU (l1 ⊔ l2) + is-perfect-image' a = (n : ℕ) → is-perfect-image-at' a n + + compute-is-perfect-image : + (a : A) → is-perfect-image' a ≃ is-perfect-image f g a + compute-is-perfect-image a = + equivalence-reasoning + ((n : ℕ) (p : fiber (iterate n (g ∘ f)) a) → fiber g (pr1 p)) + ≃ ((n : ℕ) (a₀ : A) → iterate n (g ∘ f) a₀ ＝ a → fiber g a₀) + by equiv-Π-equiv-family (λ n → equiv-ev-pair) + ≃ ((a₀ : A) (n : ℕ) → iterate n (g ∘ f) a₀ ＝ a → fiber g a₀) + by equiv-swap-Π +``` + +### Nonperfect images + +We can talk about origins of `a` which are not perfect images of `g` relative to +`f`. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} + where + + is-nonperfect-image : (a : A) → UU (l1 ⊔ l2) + is-nonperfect-image a = + Σ A (λ a₀ → Σ ℕ (λ n → (iterate n (g ∘ f) a₀ ＝ a) × ¬ (fiber g a₀))) +``` -If `g` is an [embedding](foundation-core.embeddings.md), then -`is-perfect-image a` is a [proposition](foundation-core.propositions.md). In -this case, if we assume the -[law of exluded middle](foundation.law-of-excluded-middle.md), we can show -`is-perfect-image a` is a [decidable type](foundation.decidable-types.md) for -any `a : A`. +### Nonperfect fibers over an element ```agda module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} - {f : A → B} {g : B → A} (is-emb-g : is-emb g) + (f : A → B) (g : B → A) + where + + has-nonperfect-fiber : (b : B) → UU (l1 ⊔ l2) + has-nonperfect-fiber b = + Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))) + + is-prop-has-nonperfect-fiber' : + is-prop-map f → (b : B) → is-prop (has-nonperfect-fiber b) + is-prop-has-nonperfect-fiber' F b = is-prop-Σ (F b) (λ _ → is-prop-neg) + + is-prop-has-nonperfect-fiber : + is-emb f → (b : B) → is-prop (has-nonperfect-fiber b) + is-prop-has-nonperfect-fiber F = + is-prop-has-nonperfect-fiber' (is-prop-map-is-emb F) + + has-nonperfect-fiber-Prop' : + is-prop-map f → (b : B) → Prop (l1 ⊔ l2) + has-nonperfect-fiber-Prop' F b = + ( has-nonperfect-fiber b , is-prop-has-nonperfect-fiber' F b) + + has-nonperfect-fiber-Prop : + is-emb f → (b : B) → Prop (l1 ⊔ l2) + has-nonperfect-fiber-Prop F b = + ( has-nonperfect-fiber b , is-prop-has-nonperfect-fiber F b) +``` + +## Properties + +### 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} 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-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-decidable-is-perfect-image-is-emb : - LEM (l1 ⊔ l2) → (a : A) → is-decidable (is-perfect-image f g a) - is-decidable-is-perfect-image-is-emb lem a = - lem (is-perfect-image-Prop 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 : 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. ```agda module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} where - is-perfect-image-is-fiber : - {f : A → B} {g : B → A} → (a : A) → - is-perfect-image f g a → fiber g a - is-perfect-image-is-fiber a ρ = ρ a 0 refl + fiber-is-perfect-image : (a : A) → is-perfect-image f g a → fiber g a + fiber-is-perfect-image a ρ = ρ a 0 refl ``` One can define a map from `A` to `B` restricting the domain to the perfect -images of `g`. This gives a kind of [section](foundation-core.sections.md) of g. -When g is also an embedding, the map gives a kind of -[retraction](foundation-core.retractions.md) of g. +images of `g`. This gives a kind of [section](foundation-core.sections.md) of +`g`. When `g` is also an embedding, 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} where - inverse-of-perfect-image : - (a : A) → (is-perfect-image f g a) → B - inverse-of-perfect-image a ρ = - pr1 (is-perfect-image-is-fiber a ρ) + inverse-of-perfect-image : (a : A) → is-perfect-image f g a → B + inverse-of-perfect-image a ρ = pr1 (fiber-is-perfect-image a ρ) is-section-inverse-of-perfect-image : - (a : A) (ρ : is-perfect-image f g a) → - g (inverse-of-perfect-image a ρ) ＝ a - is-section-inverse-of-perfect-image a ρ = - pr2 (is-perfect-image-is-fiber a ρ) + (a : A) (ρ : is-perfect-image f g a) → g (inverse-of-perfect-image a ρ) ＝ a + 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} {is-emb-g : is-emb 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-injective-is-emb - is-emb-g - (is-section-inverse-of-perfect-image (g b) ρ) + is-retraction-inverse-of-perfect-image G b ρ = + G (is-section-inverse-of-perfect-image (g b) ρ) ``` If `g(f(a))` is a perfect image for `g`, so is `a`. @@ -149,15 +230,22 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} where + 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 + previous-perfect-image-at' a n γ (a₀ , p) = γ (a₀ , ap (g ∘ f) p) + + previous-perfect-image' : + (a : A) → is-perfect-image' f g (g (f a)) → is-perfect-image' f g a + previous-perfect-image' a γ n = previous-perfect-image-at' a n (γ (succ-ℕ n)) + previous-perfect-image : - (a : A) → - is-perfect-image f g (g (f (a))) → - is-perfect-image f g a + (a : A) → is-perfect-image f g (g (f a)) → is-perfect-image f g a 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 _ @@ -165,7 +253,9 @@ module _ where perfect-image-has-distinct-image : - (a a₀ : A) → ¬ (is-perfect-image f g a) → (ρ : is-perfect-image f g a₀) → + (a a₀ : A) → + ¬ (is-perfect-image f g a) → + (ρ : is-perfect-image f g a₀) → f a ≠ inverse-of-perfect-image a₀ ρ perfect-image-has-distinct-image a a₀ nρ ρ p = v ρ @@ -177,88 +267,155 @@ module _ s = λ η → nρ (previous-perfect-image a η) v : ¬ (is-perfect-image f g a₀) - v = tr (λ _ → ¬ (is-perfect-image f g _)) q s + v = tr (λ a' → ¬ (is-perfect-image f g a')) q s ``` -Using the property above, we can talk about origins of `a` which are not images -of `g`. +### 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 _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} where - is-not-perfect-image : (a : A) → UU (l1 ⊔ l2) - is-not-perfect-image a = - Σ A (λ a₀ → (Σ ℕ (λ n → ((iterate n (g ∘ f)) a₀ ＝ a) × ¬ (fiber g a₀)))) + is-decidable-prop-is-perfect-image-at'' : + is-decidable-emb g → is-inhabited-or-empty-map f → is-π₀-trivial-map' f → + (a : A) (n : ℕ) → is-decidable-prop (is-perfect-image-at' f g a n) + is-decidable-prop-is-perfect-image-at'' G F F' a n = + is-decidable-prop-Π-all-elements-merely-equal-base' + ( λ x → fiber g (pr1 x) , is-decidable-prop-map-is-decidable-emb G (pr1 x)) + ( is-π₀-trivial-map'-iterate + ( is-π₀-trivial-map'-comp + ( is-π₀-trivial-map'-is-emb (is-emb-is-decidable-emb G)) + ( F')) + ( n) + ( a)) + ( is-inhabited-or-empty-map-iterate-is-π₀-trivial-map' + ( is-inhabited-or-empty-map-comp-is-π₀-trivial-map' + ( is-π₀-trivial-map'-is-emb (is-emb-is-decidable-emb G)) + ( is-inhabited-or-empty-map-is-decidable-map + ( is-decidable-map-is-decidable-emb G)) + ( F)) + ( is-π₀-trivial-map'-comp + ( is-π₀-trivial-map'-is-emb (is-emb-is-decidable-emb G)) + ( F')) + ( n) + ( a)) + + is-decidable-prop-is-perfect-image-at' : + is-decidable-emb g → is-decidable-map f → is-π₀-trivial-map' f → + (a : A) (n : ℕ) → is-decidable-prop (is-perfect-image-at' f g a n) + is-decidable-prop-is-perfect-image-at' G F = + is-decidable-prop-is-perfect-image-at'' G + ( is-inhabited-or-empty-map-is-decidable-map F) ``` -If we assume the law of excluded middle and `g` is an embedding, we can prove -that if `is-not-perfect-image a` does not hold, we have `is-perfect-image a`. +### 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} (is-emb-g : is-emb g) - (lem : LEM (l1 ⊔ l2)) + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} where - is-perfect-not-not-is-perfect-image : - (a : A) → ¬ (is-not-perfect-image a) → is-perfect-image f g a - is-perfect-not-not-is-perfect-image a nρ a₀ n p = - rec-coproduct - ( id) - ( λ a₁ → ex-falso (nρ (a₀ , n , p , a₁))) - ( lem (fiber g a₀ , is-prop-map-is-emb is-emb-g a₀)) + 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 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} - (is-emb-f : is-emb f) (is-emb-g : is-emb g) - (lem : LEM (l1 ⊔ l2)) + {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 G b nρ nμ = + nρ (double-negation-elim-is-perfect-image G (g b) nμ) + + 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 G b (x₀ , zero-ℕ , u) = + ex-falso (pr2 u (b , inv (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)) + + 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 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} + where + + double-negation-elim-has-nonperfect-fiber : + 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} + (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) + (is-π₀-trivial-f : is-π₀-trivial-map' f) + (b : B) (nρ : ¬ (is-perfect-image f g (g b))) where - not-perfect-image-has-not-perfect-fiber : - (b : B) → - ¬ (is-perfect-image f g (g b)) → - Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))) - not-perfect-image-has-not-perfect-fiber b nρ = v - where - i : ¬¬ (is-not-perfect-image {f = f} (g b)) - i = λ nμ → nρ (is-perfect-not-not-is-perfect-image is-emb-g lem (g b) nμ) - - ii : - is-not-perfect-image (g b) → - Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))) - ii (x₀ , 0 , u) = - ex-falso (pr2 u (b , inv (pr1 u))) - ii (x₀ , succ-ℕ n , u) = - a , w - where - q : f (iterate n (g ∘ f) x₀) ＝ b - q = is-injective-is-emb is-emb-g (pr1 u) - - a : fiber f b - a = iterate n (g ∘ f) x₀ , q - - w : ¬ (is-perfect-image f g ((iterate n (g ∘ f)) x₀)) - w = λ s → pr2 u (s x₀ n refl) - - iii : ¬¬ (Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))) - iii = λ t → i (λ s → t (ii s)) - - iv : is-prop (Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))) - iv = - is-prop-Σ - (is-prop-map-is-emb is-emb-f b) - (λ s → is-prop-neg {A = is-perfect-image f g (pr1 s)}) - - v : Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))) - v = double-negation-elim-is-decidable (lem (_ , iv)) iii + has-nonperfect-fiber-is-not-perfect-image : + has-nonperfect-fiber f g b + has-nonperfect-fiber-is-not-perfect-image = + double-negation-elim-has-nonperfect-fiber + ( is-double-negation-eliminating-f) + ( is-π₀-trivial-f) + ( b) + ( is-irrefutable-has-nonperfect-fiber-is-not-perfect-image + ( is-double-negation-eliminating-g) + ( is-injective-g) + ( b) + ( nρ)) + + fiber-has-nonperfect-fiber-is-not-perfect-image : fiber f b + fiber-has-nonperfect-fiber-is-not-perfect-image = + pr1 has-nonperfect-fiber-is-not-perfect-image + + element-has-nonperfect-fiber-is-not-perfect-image : A + element-has-nonperfect-fiber-is-not-perfect-image = + pr1 fiber-has-nonperfect-fiber-is-not-perfect-image + + is-in-fiber-element-has-nonperfect-fiber-is-not-perfect-image : + f element-has-nonperfect-fiber-is-not-perfect-image ＝ b + is-in-fiber-element-has-nonperfect-fiber-is-not-perfect-image = + pr2 fiber-has-nonperfect-fiber-is-not-perfect-image + + is-not-perfect-image-has-nonperfect-fiber-is-not-perfect-image : + ¬ (is-perfect-image f g element-has-nonperfect-fiber-is-not-perfect-image) + is-not-perfect-image-has-nonperfect-fiber-is-not-perfect-image = + pr2 has-nonperfect-fiber-is-not-perfect-image ``` diff --git a/src/foundation/pi-0-trivial-maps.lagda.md b/src/foundation/pi-0-trivial-maps.lagda.md new file mode 100644 index 0000000000..52a95b2dec --- /dev/null +++ b/src/foundation/pi-0-trivial-maps.lagda.md @@ -0,0 +1,111 @@ +# π₀-trivial maps + +```agda +module foundation.pi-0-trivial-maps where +``` + +
Imports + +```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-types +open import foundation.dependent-pair-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.mere-equality +open import foundation.retracts-of-maps +open import foundation.universe-levels + +open import foundation-core.contractible-maps +open import foundation-core.contractible-types +open import foundation-core.embeddings +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.propositional-maps +open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sections +``` + +
+ +## Idea + +A [map](foundation-core.function-types.md) is said to be +{{#concept "π₀-trivial" Disambiguation="map of types" Agda=is-π₀-trivial-map'}} +if its [fibers](foundation-core.fibers-of-maps.md) are π₀-trivial. I.e., that +their [set of connected components](foundation.connected-components.md) is a +[proposition](foundation-core.propositions.md). Equivalently, a type is +π₀-trivial if all its elements are [merely equal](foundation.mere-equality.md). + +## Definitions + +### π₀-trivial maps as maps whose fibers are types with mere equality + +```agda +is-π₀-trivial-map' : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) +is-π₀-trivial-map' {B = B} f = + (y : B) → all-elements-merely-equal (fiber f y) +``` + +## Properties + +### Embeddings are π₀-trivial + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + abstract + is-π₀-trivial-map'-is-prop-map : is-prop-map f → is-π₀-trivial-map' f + is-π₀-trivial-map'-is-prop-map H b x y = mere-eq-eq (eq-is-prop (H b)) + + abstract + is-π₀-trivial-map'-is-emb : is-emb f → is-π₀-trivial-map' f + is-π₀-trivial-map'-is-emb H = + is-π₀-trivial-map'-is-prop-map (is-prop-map-is-emb H) + +is-π₀-trivial-map'-id : {l : Level} {A : UU l} → is-π₀-trivial-map' (id {A = A}) +is-π₀-trivial-map'-id = is-π₀-trivial-map'-is-emb is-emb-id +``` + +### Composition of π₀-trivial maps + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {g : B → C} {f : A → B} + where + + abstract + is-π₀-trivial-map'-comp : + is-π₀-trivial-map' g → is-π₀-trivial-map' f → is-π₀-trivial-map' (g ∘ f) + is-π₀-trivial-map'-comp G F y = + all-elements-merely-equal-equiv + ( compute-fiber-comp g f y) + ( all-elements-merely-equal-Σ (G y) (F ∘ pr1)) + +module _ + {l1 : Level} {A : UU l1} {f : A → A} + (is-π₀-trivial-f : is-π₀-trivial-map' f) + where + + is-π₀-trivial-map'-iterate : + (n : ℕ) → is-π₀-trivial-map' (iterate n f) + is-π₀-trivial-map'-iterate zero-ℕ = is-π₀-trivial-map'-id + is-π₀-trivial-map'-iterate (succ-ℕ n) = + is-π₀-trivial-map'-comp is-π₀-trivial-f (is-π₀-trivial-map'-iterate n) +``` diff --git a/src/foundation/truncations.lagda.md b/src/foundation/truncations.lagda.md index 9523e78045..c6a01e227b 100644 --- a/src/foundation/truncations.lagda.md +++ b/src/foundation/truncations.lagda.md @@ -361,6 +361,10 @@ module _ is-equiv-unit-trunc-is-contr : is-contr A → is-equiv unit-trunc is-equiv-unit-trunc-is-contr c = is-equiv-unit-trunc (A , is-trunc-is-contr k c) + + is-contr-type-trunc : is-contr A → is-contr (type-trunc k A) + is-contr-type-trunc H = + is-contr-is-equiv' A unit-trunc (is-equiv-unit-trunc-is-contr H) H ``` ### Truncation is idempotent diff --git a/src/foundation/uniformly-decidable-type-families.lagda.md b/src/foundation/uniformly-decidable-type-families.lagda.md index 01904ea182..16e6fcc810 100644 --- a/src/foundation/uniformly-decidable-type-families.lagda.md +++ b/src/foundation/uniformly-decidable-type-families.lagda.md @@ -9,13 +9,17 @@ module foundation.uniformly-decidable-type-families where ```agda open import foundation.contractible-types open import foundation.coproduct-types +open import foundation.decidable-propositions open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.equality-coproduct-types +open import foundation.functoriality-coproduct-types open import foundation.inhabited-types +open import foundation.mere-equality open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions +open import foundation.transport-along-identifications open import foundation.truncated-types open import foundation.truncation-levels open import foundation.type-arithmetic-empty-type @@ -28,6 +32,8 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types + +open import logic.propositionally-decidable-types ``` @@ -63,7 +69,7 @@ is-decidable-is-uniformly-decidable-family (inl f) x = inl (f x) is-decidable-is-uniformly-decidable-family (inr g) x = inr (g x) ``` -### The uniform decidability predicate on a family of truncated types +### The uniform decidability predicate on a family of contractible types ```agda module _ @@ -173,3 +179,51 @@ module _ ( succ-𝕋 (succ-𝕋 k)) H _ = is-trunc-succ-succ-is-uniformly-decidable-family k H ``` + +### A family of decidable propositions over a π₀-trivial decidable base are uniformly decidable + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (B : A → Decidable-Prop l2) + (H : all-elements-merely-equal A) + where + + abstract + is-uniformly-decidable-family-all-elements-merely-equal-base : + is-decidable A → + is-uniformly-decidable-family (type-Decidable-Prop ∘ B) + is-uniformly-decidable-family-all-elements-merely-equal-base (inl a) = + rec-coproduct + ( λ b → + inl + ( λ x → + rec-trunc-Prop + ( prop-Decidable-Prop (B x)) + ( λ p → tr (type-Decidable-Prop ∘ B) p b) + ( H a x))) + ( λ nb → + inr + ( λ x b → + rec-trunc-Prop + ( empty-Prop) + ( λ p → nb (tr (type-Decidable-Prop ∘ B) p b)) + ( H x a))) + ( is-decidable-Decidable-Prop (B a)) + is-uniformly-decidable-family-all-elements-merely-equal-base (inr na) = + inr (ex-falso ∘ na) + + abstract + is-uniformly-decidable-family-all-elements-merely-equal-base' : + is-inhabited-or-empty A → + is-uniformly-decidable-family (type-Decidable-Prop ∘ B) + is-uniformly-decidable-family-all-elements-merely-equal-base' (inl |a|) = + rec-trunc-Prop + ( is-uniformly-decidable-family (type-Decidable-Prop ∘ B) , + is-prop-is-uniformly-decidable-family-is-inhabited-base + ( is-prop-type-Decidable-Prop ∘ B) + ( |a|)) + ( is-uniformly-decidable-family-all-elements-merely-equal-base ∘ inl) + ( |a|) + is-uniformly-decidable-family-all-elements-merely-equal-base' (inr na) = + is-uniformly-decidable-family-all-elements-merely-equal-base (inr na) +``` diff --git a/src/foundation/weak-limited-principle-of-omniscience.lagda.md b/src/foundation/weak-limited-principle-of-omniscience.lagda.md index bc9b213e06..4522874d47 100644 --- a/src/foundation/weak-limited-principle-of-omniscience.lagda.md +++ b/src/foundation/weak-limited-principle-of-omniscience.lagda.md @@ -31,15 +31,34 @@ restricted form of the [law of excluded middle](foundation.law-of-excluded-middle.md). ```agda -prop-WLPO : Prop lzero -prop-WLPO = +prop-bool-WLPO : Prop lzero +prop-bool-WLPO = ∀' (ℕ → bool) (λ f → is-decidable-Prop (∀' ℕ (λ n → is-true-Prop (f n)))) -WLPO : UU lzero -WLPO = type-Prop prop-WLPO +bool-WLPO : UU lzero +bool-WLPO = type-Prop prop-bool-WLPO -is-prop-WLPO : is-prop WLPO -is-prop-WLPO = is-prop-type-Prop prop-WLPO +is-prop-bool-WLPO : is-prop bool-WLPO +is-prop-bool-WLPO = is-prop-type-Prop prop-bool-WLPO +``` + +```agda +prop-level-WLPO : (l : Level) → Prop (lsuc l) +prop-level-WLPO l = + ∀' + ( ℕ → Decidable-Prop l) + ( λ f → is-decidable-Prop (∀' ℕ (λ n → prop-Decidable-Prop (f n)))) + +level-WLPO : (l : Level) → UU (lsuc l) +level-WLPO l = type-Prop (prop-level-WLPO l) + +is-prop-level-WLPO : {l : Level} → is-prop (level-WLPO l) +is-prop-level-WLPO {l} = is-prop-type-Prop (prop-level-WLPO l) +``` + +```agda +WLPO : UUω +WLPO = {l : Level} → level-WLPO l ``` ## See also diff --git a/src/logic.lagda.md b/src/logic.lagda.md index 4f76bcf78b..15dbbafcf5 100644 --- a/src/logic.lagda.md +++ b/src/logic.lagda.md @@ -20,4 +20,8 @@ open import logic.double-negation-stable-embeddings public open import logic.double-negation-stable-subtypes public open import logic.markovian-types public open import logic.markovs-principle public +open import logic.propositional-double-negation-elimination public +open import logic.propositionally-decidable-maps public +open import logic.propositionally-decidable-types public +open import logic.propositionally-double-negation-eliminating-maps public ``` diff --git a/src/logic/de-morgan-types.lagda.md b/src/logic/de-morgan-types.lagda.md index a87cd18593..30df2f4874 100644 --- a/src/logic/de-morgan-types.lagda.md +++ b/src/logic/de-morgan-types.lagda.md @@ -35,6 +35,7 @@ open import foundation-core.equivalences open import foundation-core.propositions open import logic.de-morgans-law +open import logic.propositionally-decidable-types ``` diff --git a/src/logic/double-negation-elimination.lagda.md b/src/logic/double-negation-elimination.lagda.md index 6fd70fe6e7..17d99c5022 100644 --- a/src/logic/double-negation-elimination.lagda.md +++ b/src/logic/double-negation-elimination.lagda.md @@ -17,7 +17,9 @@ open import foundation.empty-types open import foundation.evaluation-functions open import foundation.hilberts-epsilon-operators open import foundation.logical-equivalences +open import foundation.mere-equality open import foundation.negation +open import foundation.propositional-truncations open import foundation.retracts-of-types open import foundation.transport-along-identifications open import foundation.unit-type @@ -188,7 +190,7 @@ module _ double-negation-elim-for-all : ((p : P) → has-double-negation-elim (Q p)) → has-double-negation-elim ((p : P) → Q p) - double-negation-elim-for-all H f p = H p (λ nq → f (λ g → nq (g p))) + double-negation-elim-for-all H f p = H p (map-double-negation (ev p) f) ``` ### Double negation elimination for function types into double negations @@ -220,45 +222,82 @@ double-negation-elim-is-decidable = double-negation-elim-is-decidable ### Double negation elimination for dependent sums of types with double negation elimination over a double negation stable proposition ```agda -double-negation-elim-Σ-is-prop-base : - {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → - is-prop A → - has-double-negation-elim A → - ((a : A) → has-double-negation-elim (B a)) → - has-double-negation-elim (Σ A B) -double-negation-elim-Σ-is-prop-base {B = B} is-prop-A f g h = - ( f (λ na → h (na ∘ pr1))) , - ( g ( f (λ na → h (na ∘ pr1))) - ( λ nb → h (λ y → nb (tr B (eq-is-prop is-prop-A) (pr2 y))))) - -double-negation-elim-Σ-is-decidable-prop-base : - {l1 l2 : Level} {P : UU l1} {B : P → UU l2} → - is-decidable-prop P → - ((x : P) → has-double-negation-elim (B x)) → - has-double-negation-elim (Σ P B) -double-negation-elim-Σ-is-decidable-prop-base (H , d) = - double-negation-elim-Σ-is-prop-base H (double-negation-elim-is-decidable d) +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + double-negation-elim-Σ-all-elements-merely-equal-base : + all-elements-merely-equal A → + has-double-negation-elim A → + ((x : A) → has-double-negation-elim (B x)) → + has-double-negation-elim (Σ A B) + double-negation-elim-Σ-all-elements-merely-equal-base H f g h = + ( f ( map-double-negation pr1 h)) , + ( g ( f ( map-double-negation pr1 h)) + ( λ nb → + h ( λ x → + rec-trunc-Prop + ( empty-Prop) + ( λ p → nb (tr B p (pr2 x))) + ( H (pr1 x) (f ( map-double-negation pr1 h)))))) + + double-negation-elim-Σ-is-prop-base : + is-prop A → has-double-negation-elim A → + ((x : A) → has-double-negation-elim (B x)) → + has-double-negation-elim (Σ A B) + double-negation-elim-Σ-is-prop-base is-prop-A f g h = + ( f ( map-double-negation pr1 h)) , + ( g ( f ( map-double-negation pr1 h)) + ( map-double-negation (tr B (eq-is-prop is-prop-A) ∘ pr2) h)) + + double-negation-elim-Σ-is-decidable-prop-base : + is-decidable-prop A → + ((x : A) → has-double-negation-elim (B x)) → + has-double-negation-elim (Σ A B) + double-negation-elim-Σ-is-decidable-prop-base (H , d) = + double-negation-elim-Σ-is-prop-base H (double-negation-elim-is-decidable d) + + double-negation-elim-base-Σ-section' : + has-double-negation-elim (Σ A B) → (A → Σ A B) → + has-double-negation-elim A + double-negation-elim-base-Σ-section' H f nna = + pr1 (H (map-double-negation f nna)) + + double-negation-elim-base-Σ-section : + has-double-negation-elim (Σ A B) → + ((x : A) → B x) → + has-double-negation-elim A + double-negation-elim-base-Σ-section H f = + double-negation-elim-base-Σ-section' H (λ x → x , f x) + + double-negation-elim-family-Σ-is-prop-base : + has-double-negation-elim (Σ A B) → + is-prop A → + (x : A) → has-double-negation-elim (B x) + double-negation-elim-family-Σ-is-prop-base K is-prop-A x nnb = + tr B (eq-is-prop is-prop-A) (pr2 (K (λ nab → nnb (λ y → nab (x , y))))) ``` ### Double negation elimination for products of types with double negation elimination ```agda -double-negation-elim-product : - {l1 l2 : Level} {A : UU l1} {B : UU l2} → - has-double-negation-elim A → - has-double-negation-elim B → - has-double-negation-elim (A × B) -double-negation-elim-product f g h = - f (λ na → h (na ∘ pr1)) , g (λ nb → h (nb ∘ pr2)) +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + double-negation-elim-product : + has-double-negation-elim A → + has-double-negation-elim B → + has-double-negation-elim (A × B) + double-negation-elim-product f g h = + ( f (map-double-negation pr1 h) , g (map-double-negation pr2 h)) ``` ### If a type satisfies untruncated double negation elimination then it has a Hilbert ε-operator ```agda ε-operator-Hilbert-has-double-negation-elim : - {l1 : Level} {A : UU l1} → - has-double-negation-elim A → - ε-operator-Hilbert A + {l1 : Level} {A : UU l1} → has-double-negation-elim A → ε-operator-Hilbert A ε-operator-Hilbert-has-double-negation-elim {A = A} H = H ∘ double-negation-double-negation-type-trunc-Prop A ∘ intro-double-negation ``` diff --git a/src/logic/propositional-double-negation-elimination.lagda.md b/src/logic/propositional-double-negation-elimination.lagda.md new file mode 100644 index 0000000000..0255a374e8 --- /dev/null +++ b/src/logic/propositional-double-negation-elimination.lagda.md @@ -0,0 +1,267 @@ +# Propositional double negation elimination + +```agda +module logic.propositional-double-negation-elimination where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.coproduct-types +open import foundation.decidable-propositions +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.double-negation +open import foundation.empty-types +open import foundation.evaluation-functions +open import foundation.functoriality-propositional-truncation +open import foundation.hilberts-epsilon-operators +open import foundation.logical-equivalences +open import foundation.mere-equality +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.retracts-of-types +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels + +open import foundation-core.contractible-types +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.propositions + +open import logic.double-negation-elimination +open import logic.propositionally-decidable-types +``` + +
+ +## Idea + +We say a type `A` satisfies +{{#concept "propositional double negation elimination" Disambiguation="on a type" Agda=has-prop-double-negation-elim}} +if there is a map + +```text + ¬¬A → ║A║₋₁. +``` + +## Definitions + +### Untruncated double negation elimination + +```agda +module _ + {l : Level} (A : UU l) + where + + has-prop-double-negation-elim : UU l + has-prop-double-negation-elim = ¬¬ A → ║ A ║₋₁ + + is-prop-has-prop-double-negation-elim : is-prop has-prop-double-negation-elim + is-prop-has-prop-double-negation-elim = + is-prop-function-type is-prop-type-trunc-Prop + + has-prop-double-negation-elim-Prop : Prop l + has-prop-double-negation-elim-Prop = + ( has-prop-double-negation-elim , is-prop-has-prop-double-negation-elim) +``` + +## Properties + +### Propositional double negation elimination is preserved by logical equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + has-prop-double-negation-elim-iff : + A ↔ B → has-prop-double-negation-elim B → has-prop-double-negation-elim A + has-prop-double-negation-elim-iff e H = + map-trunc-Prop (backward-implication e) ∘ + H ∘ + map-double-negation (forward-implication e) + + has-prop-double-negation-elim-iff' : + B ↔ A → has-prop-double-negation-elim B → has-prop-double-negation-elim A + has-prop-double-negation-elim-iff' e = + has-prop-double-negation-elim-iff (inv-iff e) +``` + +### Propositional double negation elimination is preserved by equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + has-prop-double-negation-elim-equiv : + A ≃ B → has-prop-double-negation-elim B → has-prop-double-negation-elim A + has-prop-double-negation-elim-equiv e = + has-prop-double-negation-elim-iff (iff-equiv e) + + has-prop-double-negation-elim-equiv' : + B ≃ A → has-prop-double-negation-elim B → has-prop-double-negation-elim A + has-prop-double-negation-elim-equiv' e = + has-prop-double-negation-elim-iff' (iff-equiv e) +``` + +### Propositional double negation elimination is preserved by retracts + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + has-prop-double-negation-elim-retract : + A retract-of B → + has-prop-double-negation-elim B → has-prop-double-negation-elim A + has-prop-double-negation-elim-retract e = + has-prop-double-negation-elim-iff (iff-retract e) + + has-prop-double-negation-elim-retract' : + B retract-of A → + has-prop-double-negation-elim B → has-prop-double-negation-elim A + has-prop-double-negation-elim-retract' e = + has-prop-double-negation-elim-iff' (iff-retract e) +``` + +### If the negation of a type with double negation elimination is decidable, then the type is merely decidable + +```agda +module _ + {l1 : Level} {A : UU l1} + where + + is-inhabited-or-empty-is-decidable-neg-has-prop-double-negation-elim : + has-prop-double-negation-elim A → + is-decidable (¬ A) → + is-inhabited-or-empty A + is-inhabited-or-empty-is-decidable-neg-has-prop-double-negation-elim f + ( inl nx) = + inr nx + is-inhabited-or-empty-is-decidable-neg-has-prop-double-negation-elim f + ( inr nnx) = + inl (f nnx) +``` + +**Remark.** It is an established fact that both the property of satisfying +double negation elimination, and the property of having decidable negation, are +strictly weaker conditions than being decidable. Therefore, this result +demonstrates that they are independent too. + +### Types with double negation elimination satisfy propositional double negation elimination + +```agda +has-prop-double-negation-elim-has-double-negation-elim : + {l : Level} {A : UU l} → + has-double-negation-elim A → + has-prop-double-negation-elim A +has-prop-double-negation-elim-has-double-negation-elim H = unit-trunc-Prop ∘ H +``` + +### Propositional double negation elimination for merely decidable types + +```agda +prop-double-negation-elim-is-inhabited-or-empty : + {l : Level} {A : UU l} → + is-inhabited-or-empty A → has-prop-double-negation-elim A +prop-double-negation-elim-is-inhabited-or-empty (inl |a|) _ = |a| +prop-double-negation-elim-is-inhabited-or-empty (inr na) nna = ex-falso (nna na) +``` + +### Propositional double negation elimination for dependent sums + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + has-prop-double-negation-elim-Σ-all-elements-merely-equal-base : + all-elements-merely-equal A → + has-prop-double-negation-elim A → + ((x : A) → has-prop-double-negation-elim (B x)) → + has-prop-double-negation-elim (Σ A B) + has-prop-double-negation-elim-Σ-all-elements-merely-equal-base H f g nnab = + rec-trunc-Prop + ( trunc-Prop (Σ A B)) + ( λ a → + rec-trunc-Prop + ( trunc-Prop (Σ A B)) + ( λ b → unit-trunc-Prop (a , b)) + ( g + ( a) + ( λ nb → + nnab + ( λ x → + rec-trunc-Prop + ( empty-Prop) + ( λ p → nb (tr B p (pr2 x))) + ( H (pr1 x) a))))) + ( f (map-double-negation pr1 nnab)) + + has-prop-double-negation-elim-Σ-is-prop-base : + is-prop A → + has-prop-double-negation-elim A → + ((x : A) → has-prop-double-negation-elim (B x)) → + has-prop-double-negation-elim (Σ A B) + has-prop-double-negation-elim-Σ-is-prop-base is-prop-A = + has-prop-double-negation-elim-Σ-all-elements-merely-equal-base + ( λ x y → unit-trunc-Prop (eq-is-prop is-prop-A)) + + has-prop-double-negation-elim-base-Σ-section' : + has-prop-double-negation-elim (Σ A B) → + (A → Σ A B) → + has-prop-double-negation-elim A + has-prop-double-negation-elim-base-Σ-section' H f nna = + map-trunc-Prop pr1 (H (λ nab → nna (λ x → nab (f x)))) + + has-prop-double-negation-elim-base-Σ-section : + has-prop-double-negation-elim (Σ A B) → + ((x : A) → B x) → + has-prop-double-negation-elim A + has-prop-double-negation-elim-base-Σ-section H f = + has-prop-double-negation-elim-base-Σ-section' H (λ x → x , f x) + + has-prop-double-negation-elim-family-Σ-all-elements-merely-equal-base : + has-prop-double-negation-elim (Σ A B) → + all-elements-merely-equal A → + (x : A) → has-prop-double-negation-elim (B x) + has-prop-double-negation-elim-family-Σ-all-elements-merely-equal-base + K q x nnb = + rec-trunc-Prop + ( trunc-Prop (B x)) + ( λ xy → + rec-trunc-Prop + ( trunc-Prop (B x)) + ( λ p → unit-trunc-Prop (tr B p (pr2 xy))) + ( q (pr1 xy) x)) + ( K (λ nab → nnb (λ y → nab (x , y)))) +``` + +### Double negation elimination for products of types with double negation elimination + +```agda +has-prop-double-negation-elim-product : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + has-prop-double-negation-elim A → + has-prop-double-negation-elim B → + has-prop-double-negation-elim (A × B) +has-prop-double-negation-elim-product {A = A} {B} f g nnab = + rec-trunc-Prop + ( trunc-Prop (A × B)) + ( λ a → + rec-trunc-Prop + ( trunc-Prop (A × B)) + ( λ b → unit-trunc-Prop (a , b)) + ( g (map-double-negation pr2 nnab))) + ( f (map-double-negation pr1 nnab)) +``` + +## See also + +- [The double negation modality](foundation.double-negation-modality.md) +- [Irrefutable propositions](foundation.irrefutable-propositions.md) are double + negation connected types. diff --git a/src/logic/propositionally-decidable-maps.lagda.md b/src/logic/propositionally-decidable-maps.lagda.md new file mode 100644 index 0000000000..e81148285d --- /dev/null +++ b/src/logic/propositionally-decidable-maps.lagda.md @@ -0,0 +1,196 @@ +# Propositionally decidable maps + +```agda +module logic.propositionally-decidable-maps where +``` + +
Imports + +```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-maps +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.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 + +open import logic.propositionally-decidable-types +``` + +
+ +## Idea + +A [map](foundation-core.function-types.md) is said to be +{{#concept "propositionally decidable" Disambiguation="map of types" Agda=is-inhabited-or-empty-map}} +if its [fibers](foundation-core.fibers-of-maps.md) are +[propositionally decidable types](logic.propositionally-decidable-types.md). + +## Definitions + +### The structure on a map of decidability + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-inhabited-or-empty-map : (A → B) → UU (l1 ⊔ l2) + is-inhabited-or-empty-map f = (y : B) → is-inhabited-or-empty (fiber f y) +``` + +### The type of decidable maps + +```agda +inhabited-or-empty-map : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2) +inhabited-or-empty-map A B = Σ (A → B) (is-inhabited-or-empty-map) + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : inhabited-or-empty-map A B) + where + + map-inhabited-or-empty-map : A → B + map-inhabited-or-empty-map = pr1 f + + is-decidable-inhabited-or-empty-map : + is-inhabited-or-empty-map map-inhabited-or-empty-map + is-decidable-inhabited-or-empty-map = pr2 f +``` + +## Properties + +### Propositionally decidable maps are closed under homotopy + +```agda +abstract + is-inhabited-or-empty-map-htpy : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} → + f ~ g → is-inhabited-or-empty-map g → is-inhabited-or-empty-map f + is-inhabited-or-empty-map-htpy H K b = + is-inhabited-or-empty-equiv + ( equiv-tot (λ a → equiv-concat (inv (H a)) b)) + ( K b) +``` + +### Decidable maps are propositionally decidable + +```agda +is-inhabited-or-empty-map-is-decidable-map : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → + is-decidable-map f → is-inhabited-or-empty-map f +is-inhabited-or-empty-map-is-decidable-map H x = + is-inhabited-or-empty-is-decidable (H x) +``` + +### The identity map is decidable + +```agda +abstract + is-inhabited-or-empty-map-id : + {l : Level} {X : UU l} → is-inhabited-or-empty-map (id {l} {X}) + is-inhabited-or-empty-map-id y = inl (unit-trunc-Prop (y , refl)) +``` + +### Composition of propositionally decidable maps + +The composite `g ∘ f` of two propositionally decidable maps is propositionally +decidable if `g` is injective. + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {g : B → C} {f : A → B} + where + + abstract + is-inhabited-or-empty-map-comp : + is-injective g → + is-inhabited-or-empty-map g → + is-inhabited-or-empty-map f → + is-inhabited-or-empty-map (g ∘ f) + is-inhabited-or-empty-map-comp H G F x = + is-inhabited-or-empty-equiv + ( compute-fiber-comp g f x) + ( elim-is-inhabited-or-empty-Prop + ( is-inhabited-or-empty-Prop + ( Σ (fiber g x) (fiber f ∘ pr1))) + ( λ t → + elim-is-inhabited-or-empty-Prop + ( is-inhabited-or-empty-Prop (Σ (fiber g x) (fiber f ∘ pr1))) + ( λ s → inl (unit-trunc-Prop (t , s))) + ( λ ns → + inr + ( λ ts → + ns + ( pr1 (pr2 ts) , + pr2 (pr2 ts) ∙ H ((pr2 (pr1 ts)) ∙ inv (pr2 t))))) + ( F (pr1 t))) + ( λ nt → inr (λ ts → nt (pr1 ts))) + ( G x)) +``` + +The composite `g ∘ f` of two propositionally decidable maps is propositionally +decidable if `g` is π₀-trivial. + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {g : B → C} {f : A → B} + where + + abstract + is-inhabited-or-empty-map-comp-is-π₀-trivial-map' : + is-π₀-trivial-map' g → + is-inhabited-or-empty-map g → + is-inhabited-or-empty-map f → + is-inhabited-or-empty-map (g ∘ f) + is-inhabited-or-empty-map-comp-is-π₀-trivial-map' H G F x = + is-inhabited-or-empty-equiv + ( compute-fiber-comp g f x) + ( is-inhabited-or-empty-Σ-all-elements-merely-equal-base + ( H x) + ( G x) + ( F ∘ pr1)) + +module _ + {l1 : Level} {A : UU l1} {f : A → A} + (is-inhabited-or-empty-f : is-inhabited-or-empty-map f) + (is-π₀-trivial-f : is-π₀-trivial-map' f) + where + + is-inhabited-or-empty-map-iterate-is-π₀-trivial-map' : + (n : ℕ) → is-inhabited-or-empty-map (iterate n f) + is-inhabited-or-empty-map-iterate-is-π₀-trivial-map' zero-ℕ = + is-inhabited-or-empty-map-id + is-inhabited-or-empty-map-iterate-is-π₀-trivial-map' (succ-ℕ n) = + is-inhabited-or-empty-map-comp-is-π₀-trivial-map' + ( is-π₀-trivial-f) + ( is-inhabited-or-empty-f) + ( is-inhabited-or-empty-map-iterate-is-π₀-trivial-map' n) +``` diff --git a/src/logic/propositionally-decidable-types.lagda.md b/src/logic/propositionally-decidable-types.lagda.md new file mode 100644 index 0000000000..c40898a893 --- /dev/null +++ b/src/logic/propositionally-decidable-types.lagda.md @@ -0,0 +1,370 @@ +# Propositionally decidable types + +```agda +module logic.propositionally-decidable-types where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.coinhabited-pairs-of-types +open import foundation.coproduct-types +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.double-negation +open import foundation.empty-types +open import foundation.equivalences +open import foundation.functoriality-coproduct-types +open import foundation.hilberts-epsilon-operators +open import foundation.logical-equivalences +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.raising-universe-levels +open import foundation.retracts-of-types +open import foundation.type-arithmetic-empty-type +open import foundation.unit-type +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.decidable-propositions +open import foundation-core.function-types +open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sections +``` + +
+ +## Idea + +A type is said to be +{{#concept "propositionally decidable" Disambiguation="type" Agda=is-inhabited-or-empty}} +if we can either deduce that it is [inhabited](foundation.inhabited-types.md), +or we can deduce that it is [empty](foundation-core.empty-types.md), where +inhabitedness of a type is expressed using the +[propositional truncation](foundation.propositional-truncations.md). + +## Definitions + +### The predicate that a type is inhabited or empty + +```agda +is-inhabited-or-empty : {l1 : Level} → UU l1 → UU l1 +is-inhabited-or-empty A = type-trunc-Prop A + is-empty A +``` + +### Merely decidable types + +A type `A` is said to be +{{#concept "merely decidable" Agda=is-merely-decidable}} if it comes equipped +with an element of `║ is-decidable A ║₋₁`, or equivalently, the +[disjunction](foundation.disjunction.md) `A ∨ ¬ A` holds. + +```agda +is-merely-decidable-Prop : + {l : Level} → UU l → Prop l +is-merely-decidable-Prop A = trunc-Prop (is-decidable A) + +is-merely-decidable : {l : Level} → UU l → UU l +is-merely-decidable A = type-trunc-Prop (is-decidable A) +``` + +## Properties + +### Decidable types are inhabited or empty + +```agda +is-inhabited-or-empty-is-decidable : + {l : Level} {A : UU l} → is-decidable A → is-inhabited-or-empty A +is-inhabited-or-empty-is-decidable (inl x) = inl (unit-trunc-Prop x) +is-inhabited-or-empty-is-decidable (inr y) = inr y +``` + +### Decidable types are merely decidable + +```agda +is-merely-decidable-is-decidable : + {l : Level} {A : UU l} → is-decidable A → is-merely-decidable A +is-merely-decidable-is-decidable = unit-trunc-Prop +``` + +### Being inhabited or empty is a proposition + +```agda +abstract + is-property-is-inhabited-or-empty : + {l1 : Level} (A : UU l1) → is-prop (is-inhabited-or-empty A) + is-property-is-inhabited-or-empty A = + is-prop-coproduct + ( λ t → apply-universal-property-trunc-Prop t empty-Prop) + ( is-prop-type-trunc-Prop) + ( is-prop-neg) + +is-inhabited-or-empty-Prop : {l1 : Level} → UU l1 → Prop l1 +pr1 (is-inhabited-or-empty-Prop A) = is-inhabited-or-empty A +pr2 (is-inhabited-or-empty-Prop A) = is-property-is-inhabited-or-empty A +``` + +### Types are inhabited or empty if and only if they are merely decidable + +```agda +module _ + {l : Level} {A : UU l} + where + + is-inhabited-or-empty-is-merely-decidable : + is-merely-decidable A → is-inhabited-or-empty A + is-inhabited-or-empty-is-merely-decidable = + rec-trunc-Prop + ( is-inhabited-or-empty-Prop A) + ( is-inhabited-or-empty-is-decidable) + + is-merely-decidable-is-inhabited-or-empty : + is-inhabited-or-empty A → is-merely-decidable A + is-merely-decidable-is-inhabited-or-empty (inl |x|) = + rec-trunc-Prop (is-merely-decidable-Prop A) (unit-trunc-Prop ∘ inl) |x| + is-merely-decidable-is-inhabited-or-empty (inr y) = + unit-trunc-Prop (inr y) + + iff-is-inhabited-or-empty-is-merely-decidable : + is-merely-decidable A ↔ is-inhabited-or-empty A + iff-is-inhabited-or-empty-is-merely-decidable = + ( is-inhabited-or-empty-is-merely-decidable , + is-merely-decidable-is-inhabited-or-empty) +``` + +### Propositionally decidable types are closed under coinhabited types + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-inhabited-or-empty-is-coinhabited : + is-coinhabited A B → is-inhabited-or-empty A → is-inhabited-or-empty B + is-inhabited-or-empty-is-coinhabited (f , b) = + map-coproduct + ( f) + ( is-empty-type-trunc-Prop' ∘ map-neg b ∘ is-empty-type-trunc-Prop) +``` + +### Propositionally decidable types are closed under logical equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-inhabited-or-empty-iff : + (A → B) → (B → A) → is-inhabited-or-empty A → is-inhabited-or-empty B + is-inhabited-or-empty-iff f g (inl |a|) = + inl (rec-trunc-Prop (trunc-Prop B) (unit-trunc-Prop ∘ f) |a|) + is-inhabited-or-empty-iff f g (inr na) = inr (na ∘ g) + + is-inhabited-or-empty-iff' : + A ↔ B → is-inhabited-or-empty A → is-inhabited-or-empty B + is-inhabited-or-empty-iff' (f , g) = is-inhabited-or-empty-iff f g + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + iff-is-inhabited-or-empty : + A ↔ B → is-inhabited-or-empty A ↔ is-inhabited-or-empty B + iff-is-inhabited-or-empty e = + is-inhabited-or-empty-iff' e , is-inhabited-or-empty-iff' (inv-iff e) +``` + +### Propositionally decidable types are closed under retracts + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-inhabited-or-empty-retract-of : + A retract-of B → is-inhabited-or-empty B → is-inhabited-or-empty A + is-inhabited-or-empty-retract-of R = + is-inhabited-or-empty-iff' (iff-retract' R) + + is-inhabited-or-empty-retract-of' : + A retract-of B → is-inhabited-or-empty A → is-inhabited-or-empty B + is-inhabited-or-empty-retract-of' R = + is-inhabited-or-empty-iff' (inv-iff (iff-retract' R)) +``` + +### Propositionally decidable types are closed under equivalences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-inhabited-or-empty-is-equiv : + {f : A → B} → is-equiv f → is-inhabited-or-empty B → is-inhabited-or-empty A + is-inhabited-or-empty-is-equiv {f} H = + is-inhabited-or-empty-retract-of (retract-equiv (f , H)) + + is-inhabited-or-empty-equiv : + A ≃ B → is-inhabited-or-empty B → is-inhabited-or-empty A + is-inhabited-or-empty-equiv e = + is-inhabited-or-empty-iff (map-inv-equiv e) (map-equiv e) + + is-inhabited-or-empty-equiv' : + A ≃ B → is-inhabited-or-empty A → is-inhabited-or-empty B + is-inhabited-or-empty-equiv' e = + is-inhabited-or-empty-iff (map-equiv e) (map-inv-equiv e) +``` + +### Elimination for propositional decidability + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (B : Prop l2) + where + + elim-is-inhabited-or-empty-Prop : + (A → type-Prop B) → (¬ A → type-Prop B) → + is-inhabited-or-empty A → type-Prop B + elim-is-inhabited-or-empty-Prop b nb (inl |a|) = rec-trunc-Prop B b |a| + elim-is-inhabited-or-empty-Prop b nb (inr na) = nb na + + elim-is-inhabited-or-empty-Prop' : + (is-decidable A → type-Prop B) → is-inhabited-or-empty A → type-Prop B + elim-is-inhabited-or-empty-Prop' f = + elim-is-inhabited-or-empty-Prop (f ∘ inl) (f ∘ inr) +``` + +### Coproducts of propositionally decidable types are propositionally decidable + +```agda +is-inhabited-or-empty-coproduct : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-inhabited-or-empty A → + is-inhabited-or-empty B → + is-inhabited-or-empty (A + B) +is-inhabited-or-empty-coproduct (inl a) dB = + rec-trunc-Prop (is-inhabited-or-empty-Prop _) (inl ∘ unit-trunc-Prop ∘ inl) a +is-inhabited-or-empty-coproduct (inr na) (inl b) = + rec-trunc-Prop (is-inhabited-or-empty-Prop _) (inl ∘ unit-trunc-Prop ∘ inr) b +is-inhabited-or-empty-coproduct (inr na) (inr nb) = inr (rec-coproduct na nb) +``` + +### Cartesian products of propositionally decidable types are propositionally decidable + +```agda +is-inhabited-or-empty-product : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-inhabited-or-empty A → + is-inhabited-or-empty B → + is-inhabited-or-empty (A × B) +is-inhabited-or-empty-product (inl a) (inl b) = + inl (map-inv-distributive-trunc-product-Prop (a , b)) +is-inhabited-or-empty-product (inl a) (inr nb) = inr (nb ∘ pr2) +is-inhabited-or-empty-product (inr na) dB = inr (na ∘ pr1) + +is-inhabited-or-empty-product' : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-inhabited-or-empty A → (A → is-inhabited-or-empty B) → + is-inhabited-or-empty (A × B) +is-inhabited-or-empty-product' (inl a) dB = + rec-trunc-Prop + ( is-inhabited-or-empty-Prop _) + ( rec-coproduct + ( λ b → inl (map-inv-distributive-trunc-product-Prop (a , b))) + ( λ nb → inr (nb ∘ pr2)) ∘ + dB) + ( a) +is-inhabited-or-empty-product' (inr na) dB = inr (na ∘ pr1) + +is-inhabited-or-empty-left-factor : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-inhabited-or-empty (A × B) → B → is-inhabited-or-empty A +is-inhabited-or-empty-left-factor (inl x) b = + inl (pr1 (map-distributive-trunc-product-Prop x)) +is-inhabited-or-empty-left-factor (inr nx) b = inr (λ a → nx (a , b)) + +is-inhabited-or-empty-right-factor : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-inhabited-or-empty (A × B) → A → is-inhabited-or-empty B +is-inhabited-or-empty-right-factor (inl x) a = + inl (pr2 (map-distributive-trunc-product-Prop x)) +is-inhabited-or-empty-right-factor (inr nx) a = inr (λ b → nx (a , b)) +``` + +### Function types of propositionally decidable types are propositionally decidable + +```agda +is-inhabited-or-empty-function-type : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-inhabited-or-empty A → + is-inhabited-or-empty B → + is-inhabited-or-empty (A → B) +is-inhabited-or-empty-function-type (inl a) (inl b) = + inl (rec-trunc-Prop (trunc-Prop _) (λ y → unit-trunc-Prop (λ _ → y)) b) +is-inhabited-or-empty-function-type (inl a) (inr nb) = + inr (λ f → rec-trunc-Prop empty-Prop (λ x → nb (f x)) a) +is-inhabited-or-empty-function-type (inr na) dB = + inl (unit-trunc-Prop (ex-falso ∘ na)) + +is-inhabited-or-empty-function-type' : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → + is-inhabited-or-empty A → (A → is-inhabited-or-empty B) → + is-inhabited-or-empty (A → B) +is-inhabited-or-empty-function-type' (inl a) dB = + rec-trunc-Prop (is-inhabited-or-empty-Prop _) + ( λ x → + rec-coproduct + ( inl ∘ rec-trunc-Prop (trunc-Prop _) (λ y → unit-trunc-Prop (λ _ → y))) + ( λ nb → inr (λ f → nb (f x))) + ( dB x)) + ( a) +is-inhabited-or-empty-function-type' (inr na) dB = + inl (unit-trunc-Prop (ex-falso ∘ na)) +``` + +### Decidability of a propositional truncation + +```agda +abstract + is-prop-is-decidable-trunc-Prop : + {l : Level} (A : UU l) → is-prop (is-decidable (type-trunc-Prop A)) + is-prop-is-decidable-trunc-Prop A = + is-prop-is-decidable is-prop-type-trunc-Prop + +is-decidable-trunc-Prop : {l : Level} → UU l → Prop l +pr1 (is-decidable-trunc-Prop A) = is-decidable (type-trunc-Prop A) +pr2 (is-decidable-trunc-Prop A) = is-prop-is-decidable-trunc-Prop A + +is-decidable-trunc-Prop-is-decidable : + {l : Level} {A : UU l} → + is-decidable A → type-Prop (is-decidable-trunc-Prop A) +is-decidable-trunc-Prop-is-decidable (inl a) = + inl (unit-trunc-Prop a) +is-decidable-trunc-Prop-is-decidable (inr f) = + inr (map-universal-property-trunc-Prop empty-Prop f) + +is-decidable-trunc-Prop-is-merely-decidable : + {l : Level} {A : UU l} → + is-merely-decidable A → is-decidable (type-trunc-Prop A) +is-decidable-trunc-Prop-is-merely-decidable {A = A} = + map-universal-property-trunc-Prop + ( is-decidable-trunc-Prop A) + ( is-decidable-trunc-Prop-is-decidable) + +is-merely-decidable-is-decidable-trunc-Prop : + {l : Level} (A : UU l) → + is-decidable (type-trunc-Prop A) → is-merely-decidable A +is-merely-decidable-is-decidable-trunc-Prop A (inl x) = + apply-universal-property-trunc-Prop x + ( is-merely-decidable-Prop A) + ( unit-trunc-Prop ∘ inl) +is-merely-decidable-is-decidable-trunc-Prop A (inr f) = + unit-trunc-Prop (inr (f ∘ unit-trunc-Prop)) +``` + +## See also + +- That decidablity is irrefutable is shown in + [`foundation.irrefutable-propositions`](foundation.irrefutable-propositions.md). diff --git a/src/logic/propositionally-double-negation-eliminating-maps.lagda.md b/src/logic/propositionally-double-negation-eliminating-maps.lagda.md new file mode 100644 index 0000000000..633ea49a3b --- /dev/null +++ b/src/logic/propositionally-double-negation-eliminating-maps.lagda.md @@ -0,0 +1,143 @@ +# Propositionally double negation eliminating maps + +```agda +module logic.propositionally-double-negation-eliminating-maps where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cartesian-morphisms-arrows +open import foundation.coproduct-types +open import foundation.decidable-equality +open import foundation.decidable-maps +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.double-negation +open import foundation.empty-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.propositions +open import foundation.retractions +open import foundation.retracts-of-maps +open import foundation.retracts-of-types +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import foundation-core.contractible-maps +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 logic.double-negation-eliminating-maps +open import logic.double-negation-elimination +open import logic.propositional-double-negation-elimination +open import logic.propositionally-decidable-maps +``` + +
+ +## Idea + +A [map](foundation-core.function-types.md) is said to be +{{#concept "propositionally double negation eliminating" Disambiguation="map of types" Agda=is-prop-double-negation-eliminating-map}} +if its [fibers](foundation-core.fibers-of-maps.md) satisfy +[propositional double negation elimination](logic.propositional-double-negation-elimination.md). +I.e., for every `y : B`, if `fiber f y` is +[irrefutable](foundation.irrefutable-propositions.md), then we do in fact have +then the fiber is in fact inhabited. In other words, double negation eliminating +maps come [equipped](foundation.structure.md) with a map + +```text + (y : B) → ¬¬ (fiber f y) → ║ fiber f y ║₋₁. +``` + +## Definintion + +### Double negation elimination structure on a map + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-prop-double-negation-eliminating-map : (A → B) → UU (l1 ⊔ l2) + is-prop-double-negation-eliminating-map f = + (y : B) → has-prop-double-negation-elim (fiber f y) + + is-property-is-prop-double-negation-eliminating-map : + {f : A → B} → is-prop (is-prop-double-negation-eliminating-map f) + is-property-is-prop-double-negation-eliminating-map {f} = + is-prop-Π (λ y → is-prop-has-prop-double-negation-elim (fiber f y)) + + is-prop-double-negation-eliminating-map-Prop : (A → B) → Prop (l1 ⊔ l2) + is-prop-double-negation-eliminating-map-Prop f = + is-prop-double-negation-eliminating-map f , + is-property-is-prop-double-negation-eliminating-map +``` + +### The type of propositionally double negation eliminating maps + +```agda +prop-double-negation-eliminating-map : + {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2) +prop-double-negation-eliminating-map A B = + Σ (A → B) (is-prop-double-negation-eliminating-map) + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + (f : prop-double-negation-eliminating-map A B) + where + + map-prop-double-negation-eliminating-map : A → B + map-prop-double-negation-eliminating-map = pr1 f + + is-prop-double-negation-eliminating-prop-double-negation-eliminating-map : + is-prop-double-negation-eliminating-map + map-prop-double-negation-eliminating-map + is-prop-double-negation-eliminating-prop-double-negation-eliminating-map = + pr2 f +``` + +## Properties + +### Double negation eliminating maps are closed under homotopy + +```agda +abstract + is-prop-double-negation-eliminating-map-htpy : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} → + f ~ g → + is-prop-double-negation-eliminating-map g → + is-prop-double-negation-eliminating-map f + is-prop-double-negation-eliminating-map-htpy H K b = + has-prop-double-negation-elim-equiv + ( equiv-tot (λ a → equiv-concat (inv (H a)) b)) + ( K b) +``` + +### Double negation eliminating maps are propositionally double negation eliminating + +```agda +is-prop-double-negation-eliminating-map-is-double-negation-eliminating-map : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → + is-double-negation-eliminating-map f → + is-prop-double-negation-eliminating-map f +is-prop-double-negation-eliminating-map-is-double-negation-eliminating-map H y = + has-prop-double-negation-elim-has-double-negation-elim (H y) +``` + +### Propositionally decidable maps are propositionally double negation eliminating + +```agda +is-prop-double-negation-eliminating-map-is-inhabited-or-empty-map : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → + is-inhabited-or-empty-map f → is-prop-double-negation-eliminating-map f +is-prop-double-negation-eliminating-map-is-inhabited-or-empty-map H y = + prop-double-negation-elim-is-inhabited-or-empty (H y) +``` diff --git a/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md b/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md index eb2cbcdba9..f173a260c6 100644 --- a/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md +++ b/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md @@ -83,7 +83,7 @@ is-double-negation-sheaf-is-contr is-contr-A P = module _ {l : Level} {A : UU l} (is-prop-A : is-prop A) - (is-¬¬sheaf-A : is-double-negation-sheaf l A) + (is-¬¬-sheaf-A : is-double-negation-sheaf l A) where compute-is-double-negation-sheaf-is-prop : A ≃ (¬ A → A) @@ -91,12 +91,12 @@ module _ ( left-unit-law-product-is-contr ( is-proof-irrelevant-is-prop (is-prop-function-type is-prop-A) id)) ∘e ( equiv-universal-property-coproduct A) ∘e - ( _ , is-¬¬sheaf-A (is-decidable-prop-Irrefutable-Prop (A , is-prop-A))) + ( _ , is-¬¬-sheaf-A (is-decidable-prop-Irrefutable-Prop (A , is-prop-A))) is-double-negation-stable-is-double-negation-sheaf-is-prop : is-double-negation-stable (A , is-prop-A) is-double-negation-stable-is-double-negation-sheaf-is-prop ¬¬a = - map-inv-is-equiv (is-¬¬sheaf-A (A , is-prop-A , ¬¬a)) id + map-inv-is-equiv (is-¬¬-sheaf-A (A , is-prop-A , ¬¬a)) id ``` ### Double negation stable propositions are double negation sheaves diff --git a/src/set-theory/cantors-diagonal-argument.lagda.md b/src/set-theory/cantors-diagonal-argument.lagda.md index b573aa9ab7..083b3aff85 100644 --- a/src/set-theory/cantors-diagonal-argument.lagda.md +++ b/src/set-theory/cantors-diagonal-argument.lagda.md @@ -33,6 +33,8 @@ open import foundation-core.empty-types open import foundation-core.fibers-of-maps open import foundation-core.propositions +open import logic.propositionally-decidable-types + open import set-theory.countable-sets open import set-theory.infinite-sets open import set-theory.uncountable-sets diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index 1b5112681f..668726e90b 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -175,7 +175,20 @@ module _ ( c) ( compute-inl-dependent-cogap) ( compute-inr-dependent-cogap) +``` + +For reference, the unfolded type signature for `compute-glue-dependent-cogap` is +as follows: + +```text + (s : S) → + ( apd dependent-cogap (glue-pushout f g s) ∙ + compute-inr-dependent-cogap (g s)) ＝ + ( ap (tr P (glue-pushout f g s)) (compute-inl-dependent-cogap (f s)) ∙ + coherence-square-dependent-cocone f g (cocone-pushout f g) P c s) +``` +```agda htpy-compute-dependent-cogap : htpy-dependent-cocone f g ( cocone-pushout f g) diff --git a/src/univalent-combinatorics/counting.lagda.md b/src/univalent-combinatorics/counting.lagda.md index aec4b66b23..b03f64c4e2 100644 --- a/src/univalent-combinatorics/counting.lagda.md +++ b/src/univalent-combinatorics/counting.lagda.md @@ -26,6 +26,8 @@ open import foundation.sets open import foundation.unit-type open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import univalent-combinatorics.equality-standard-finite-types open import univalent-combinatorics.standard-finite-types ``` diff --git a/src/univalent-combinatorics/dependent-pair-types.lagda.md b/src/univalent-combinatorics/dependent-pair-types.lagda.md index 932efc1d7a..843cd79854 100644 --- a/src/univalent-combinatorics/dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/dependent-pair-types.lagda.md @@ -31,6 +31,8 @@ open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels +open import logic.propositionally-decidable-types + open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.counting open import univalent-combinatorics.counting-dependent-pair-types diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index e92ae82979..29ff3b2a18 100644 --- a/src/univalent-combinatorics/finite-types.lagda.md +++ b/src/univalent-combinatorics/finite-types.lagda.md @@ -42,6 +42,8 @@ open import foundation.universe-levels open import foundation-core.torsorial-type-families +open import logic.propositionally-decidable-types + open import univalent-combinatorics.counting open import univalent-combinatorics.double-counting open import univalent-combinatorics.standard-finite-types