diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 931de9244e3..5839931dd0c 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -79,6 +79,7 @@ open import foundation.commuting-triangles-of-identifications public open import foundation.commuting-triangles-of-maps public open import foundation.commuting-triangles-of-morphisms-arrows public open import foundation.complements public +open import foundation.complements-images public open import foundation.complements-subtypes public open import foundation.composite-maps-in-inverse-sequential-diagrams public open import foundation.composition-algebra public @@ -114,6 +115,7 @@ open import foundation.decidable-equivalence-relations public open import foundation.decidable-maps public open import foundation.decidable-propositions public open import foundation.decidable-relations public +open import foundation.decidable-retracts-of-types public open import foundation.decidable-subtypes public open import foundation.decidable-type-families public open import foundation.decidable-types public diff --git a/src/foundation/complements-images.lagda.md b/src/foundation/complements-images.lagda.md new file mode 100644 index 00000000000..0bcfb61b56d --- /dev/null +++ b/src/foundation/complements-images.lagda.md @@ -0,0 +1,180 @@ +# The complement of the image of a map + +```agda +module foundation.complements-images where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.fundamental-theorem-of-identity-types +open import foundation.negation +open import foundation.subtype-identity-principle +open import foundation.universe-levels + +open import foundation-core.1-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 +open import foundation-core.injective-maps +open import foundation-core.propositions +open import foundation-core.sets +open import foundation-core.subtypes +open import foundation-core.torsorial-type-families +open import foundation-core.truncated-types +open import foundation-core.truncation-levels +``` + +
+ +## Idea + +The {{#concept "complement" Disambiguation="of the image of a map" Agda=nonim}} +of the [image](foundation.images.md) of a map `f : A → B` is the collection of +elements `y` in `B` such that the fiber of `f` over `y` is +[empty](foundation.empty-types.md). + +## Definitions + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) + where + + subtype-nonim : subtype (l1 ⊔ l2) X + subtype-nonim x = neg-type-Prop (fiber f x) + + is-in-nonim : X → UU (l1 ⊔ l2) + is-in-nonim = is-in-subtype subtype-nonim + + nonim : UU (l1 ⊔ l2) + nonim = type-subtype subtype-nonim + + inclusion-nonim : nonim → X + inclusion-nonim = inclusion-subtype subtype-nonim +``` + +## Properties + +### We characterize the identity type of `nonim f` + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) + where + + Eq-nonim : nonim f → nonim f → UU l1 + Eq-nonim x y = (pr1 x ＝ pr1 y) + + refl-Eq-nonim : (x : nonim f) → Eq-nonim x x + refl-Eq-nonim x = refl + + Eq-eq-nonim : (x y : nonim f) → x ＝ y → Eq-nonim x y + Eq-eq-nonim x .x refl = refl-Eq-nonim x + + abstract + is-torsorial-Eq-nonim : + (x : nonim f) → is-torsorial (Eq-nonim x) + is-torsorial-Eq-nonim (x , p) = + is-torsorial-Eq-subtype (is-torsorial-Id x) (λ x → is-prop-neg) x refl p + + abstract + is-equiv-Eq-eq-nonim : (x y : nonim f) → is-equiv (Eq-eq-nonim x y) + is-equiv-Eq-eq-nonim x = + fundamental-theorem-id (is-torsorial-Eq-nonim x) (Eq-eq-nonim x) + + equiv-Eq-eq-nonim : (x y : nonim f) → (x ＝ y) ≃ Eq-nonim x y + equiv-Eq-eq-nonim x y = (Eq-eq-nonim x y , is-equiv-Eq-eq-nonim x y) + + eq-Eq-nonim : (x y : nonim f) → Eq-nonim x y → x ＝ y + eq-Eq-nonim x y = map-inv-is-equiv (is-equiv-Eq-eq-nonim x y) +``` + +### The nonimage inclusion is an embedding + +```agda +abstract + is-emb-inclusion-nonim : + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → + is-emb (inclusion-nonim f) + is-emb-inclusion-nonim f = is-emb-inclusion-subtype (neg-type-Prop ∘ fiber f) + +emb-nonim : + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → nonim f ↪ X +emb-nonim f = (inclusion-nonim f , is-emb-inclusion-nonim f) +``` + +### The nonimage inclusion is injective + +```agda +abstract + is-injective-inclusion-nonim : + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → + is-injective (inclusion-nonim f) + is-injective-inclusion-nonim f = + is-injective-is-emb (is-emb-inclusion-nonim f) +``` + +### The nonimage of a map into a truncated type is truncated + +```agda +abstract + is-trunc-nonim : + {l1 l2 : Level} (k : 𝕋) {X : UU l1} {A : UU l2} (f : A → X) → + is-trunc (succ-𝕋 k) X → is-trunc (succ-𝕋 k) (nonim f) + is-trunc-nonim k f = is-trunc-emb k (emb-nonim f) + +nonim-Truncated-Type : + {l1 l2 : Level} (k : 𝕋) (X : Truncated-Type l1 (succ-𝕋 k)) {A : UU l2} + (f : A → type-Truncated-Type X) → Truncated-Type (l1 ⊔ l2) (succ-𝕋 k) +nonim-Truncated-Type k X f = + ( nonim f , is-trunc-nonim k f (is-trunc-type-Truncated-Type X)) +``` + +### The nonimage of a map into a proposition is a proposition + +```agda +abstract + is-prop-nonim : + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → + is-prop X → is-prop (nonim f) + is-prop-nonim = is-trunc-nonim neg-two-𝕋 + +nonim-Prop : + {l1 l2 : Level} (X : Prop l1) {A : UU l2} + (f : A → type-Prop X) → Prop (l1 ⊔ l2) +nonim-Prop X f = nonim-Truncated-Type neg-two-𝕋 X f +``` + +### The nonimage of a map into a set is a set + +```agda +abstract + is-set-nonim : + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → + is-set X → is-set (nonim f) + is-set-nonim = is-trunc-nonim neg-one-𝕋 + +nonim-Set : + {l1 l2 : Level} (X : Set l1) {A : UU l2} + (f : A → type-Set X) → Set (l1 ⊔ l2) +nonim-Set X f = nonim-Truncated-Type (neg-one-𝕋) X f +``` + +### The nonimage of a map into a 1-type is a 1-type + +```agda +abstract + is-1-type-nonim : + {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → + is-1-type X → is-1-type (nonim f) + is-1-type-nonim = is-trunc-nonim zero-𝕋 + +nonim-1-Type : + {l1 l2 : Level} (X : 1-Type l1) {A : UU l2} + (f : A → type-1-Type X) → 1-Type (l1 ⊔ l2) +nonim-1-Type X f = nonim-Truncated-Type zero-𝕋 X f +``` diff --git a/src/foundation/coproduct-decompositions-subuniverse.lagda.md b/src/foundation/coproduct-decompositions-subuniverse.lagda.md index 494082f5804..14e33ddbaf6 100644 --- a/src/foundation/coproduct-decompositions-subuniverse.lagda.md +++ b/src/foundation/coproduct-decompositions-subuniverse.lagda.md @@ -82,10 +82,25 @@ module _ matching-correspondence-binary-coproduct-Decomposition-subuniverse : inclusion-subuniverse P X ≃ - ( type-left-summand-binary-coproduct-Decomposition-subuniverse + - type-right-summand-binary-coproduct-Decomposition-subuniverse) + type-left-summand-binary-coproduct-Decomposition-subuniverse + + type-right-summand-binary-coproduct-Decomposition-subuniverse matching-correspondence-binary-coproduct-Decomposition-subuniverse = pr2 (pr2 d) + + map-matching-correspondence-binary-coproduct-Decomposition-subuniverse : + inclusion-subuniverse P X → + type-left-summand-binary-coproduct-Decomposition-subuniverse + + type-right-summand-binary-coproduct-Decomposition-subuniverse + map-matching-correspondence-binary-coproduct-Decomposition-subuniverse = + map-equiv matching-correspondence-binary-coproduct-Decomposition-subuniverse + + map-inv-matching-correspondence-binary-coproduct-Decomposition-subuniverse : + type-left-summand-binary-coproduct-Decomposition-subuniverse + + type-right-summand-binary-coproduct-Decomposition-subuniverse → + inclusion-subuniverse P X + map-inv-matching-correspondence-binary-coproduct-Decomposition-subuniverse = + map-inv-equiv + ( matching-correspondence-binary-coproduct-Decomposition-subuniverse) ``` ### Iterated binary coproduct decompositions @@ -179,12 +194,10 @@ equiv-binary-coproduct-Decomposition-subuniverse P A X Y = type-right-summand-binary-coproduct-Decomposition-subuniverse P A Y) ( λ er → ( map-coproduct (map-equiv el) (map-equiv er) ∘ - map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-subuniverse - P A X)) ~ - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-subuniverse - P A Y)))) + map-matching-correspondence-binary-coproduct-Decomposition-subuniverse + P A X) ~ + ( map-matching-correspondence-binary-coproduct-Decomposition-subuniverse + P A Y))) module _ {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) @@ -231,10 +244,8 @@ module _ id-map-coproduct ( type-left-summand-binary-coproduct-Decomposition-subuniverse P A X) ( type-right-summand-binary-coproduct-Decomposition-subuniverse P A X) - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-subuniverse - P A X) - ( x)) + ( map-matching-correspondence-binary-coproduct-Decomposition-subuniverse + P A X x) is-torsorial-equiv-binary-coproduct-Decomposition-subuniverse : is-torsorial (equiv-binary-coproduct-Decomposition-subuniverse P A X) diff --git a/src/foundation/coproduct-decompositions.lagda.md b/src/foundation/coproduct-decompositions.lagda.md index 081d474d3f1..75b65408fd7 100644 --- a/src/foundation/coproduct-decompositions.lagda.md +++ b/src/foundation/coproduct-decompositions.lagda.md @@ -34,6 +34,8 @@ open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sections open import foundation-core.torsorial-type-families open import foundation-core.transport-along-identifications @@ -45,7 +47,7 @@ open import univalent-combinatorics.standard-finite-types ## Definitions -### Binary coproduct decomposition +### Binary coproduct decompositions ```agda module _ @@ -54,7 +56,7 @@ module _ binary-coproduct-Decomposition : UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) binary-coproduct-Decomposition = - Σ ( UU l2) ( λ A → Σ ( UU l3) ( λ B → (X ≃ (A + B)))) + Σ (UU l2) (λ A → Σ (UU l3) (λ B → X ≃ A + B)) module _ {l1 l2 l3 : Level} {X : UU l1} @@ -69,9 +71,23 @@ module _ matching-correspondence-binary-coproduct-Decomposition : X ≃ - ( left-summand-binary-coproduct-Decomposition + - right-summand-binary-coproduct-Decomposition) + left-summand-binary-coproduct-Decomposition + + right-summand-binary-coproduct-Decomposition matching-correspondence-binary-coproduct-Decomposition = pr2 (pr2 d) + + map-matching-correspondence-binary-coproduct-Decomposition : + X → + left-summand-binary-coproduct-Decomposition + + right-summand-binary-coproduct-Decomposition + map-matching-correspondence-binary-coproduct-Decomposition = + map-equiv matching-correspondence-binary-coproduct-Decomposition + + map-inv-matching-correspondence-binary-coproduct-Decomposition : + left-summand-binary-coproduct-Decomposition + + right-summand-binary-coproduct-Decomposition → + X + map-inv-matching-correspondence-binary-coproduct-Decomposition = + map-inv-equiv matching-correspondence-binary-coproduct-Decomposition ``` ## Propositions @@ -112,15 +128,14 @@ pr2 (equiv-coproduct-Decomposition-full-subuniverse X) = ( id-equiv , right-whisker-comp ( id-map-coproduct _ _) - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-subuniverse - ( λ _ → unit-Prop) - ( X , star) - ( d)))))) + ( map-matching-correspondence-binary-coproduct-Decomposition-subuniverse + ( λ _ → unit-Prop) + ( X , star) + ( d))))) ( refl-htpy) ``` -### Characterization of equality of binary coproduct Decomposition +### Characterization of equality of binary coproduct decompositions ```agda equiv-binary-coproduct-Decomposition : @@ -136,10 +151,8 @@ equiv-binary-coproduct-Decomposition X Y = right-summand-binary-coproduct-Decomposition Y) ( λ er → ( map-coproduct (map-equiv el) (map-equiv er) ∘ - map-equiv - ( matching-correspondence-binary-coproduct-Decomposition X)) ~ - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition Y)))) + map-matching-correspondence-binary-coproduct-Decomposition X) ~ + ( map-matching-correspondence-binary-coproduct-Decomposition Y))) module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} @@ -176,42 +189,46 @@ module _ id-equiv-binary-coproduct-Decomposition : equiv-binary-coproduct-Decomposition X X - pr1 id-equiv-binary-coproduct-Decomposition = id-equiv - pr1 (pr2 id-equiv-binary-coproduct-Decomposition) = id-equiv + pr1 id-equiv-binary-coproduct-Decomposition = + id-equiv + pr1 (pr2 id-equiv-binary-coproduct-Decomposition) = + id-equiv pr2 (pr2 id-equiv-binary-coproduct-Decomposition) x = id-map-coproduct ( left-summand-binary-coproduct-Decomposition X) ( right-summand-binary-coproduct-Decomposition X) - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition X) - ( x)) - - is-torsorial-equiv-binary-coproduct-Decomposition : - is-torsorial (equiv-binary-coproduct-Decomposition X) - is-torsorial-equiv-binary-coproduct-Decomposition = - is-torsorial-Eq-structure - ( is-torsorial-equiv ( left-summand-binary-coproduct-Decomposition X)) - ( left-summand-binary-coproduct-Decomposition X , id-equiv) - ( is-torsorial-Eq-structure - ( is-torsorial-equiv (right-summand-binary-coproduct-Decomposition X)) - ( right-summand-binary-coproduct-Decomposition X , id-equiv) - ( is-torsorial-htpy-equiv - ( equiv-coproduct id-equiv id-equiv ∘e - matching-correspondence-binary-coproduct-Decomposition X))) + ( map-matching-correspondence-binary-coproduct-Decomposition X x) + + abstract + is-torsorial-equiv-binary-coproduct-Decomposition : + is-torsorial + ( equiv-binary-coproduct-Decomposition {l1} {l2} {l3} {l2} {l3} X) + is-torsorial-equiv-binary-coproduct-Decomposition = + is-torsorial-Eq-structure + ( is-torsorial-equiv (left-summand-binary-coproduct-Decomposition X)) + ( left-summand-binary-coproduct-Decomposition X , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-equiv (right-summand-binary-coproduct-Decomposition X)) + ( right-summand-binary-coproduct-Decomposition X , id-equiv) + ( is-torsorial-htpy-equiv + ( equiv-coproduct id-equiv id-equiv ∘e + matching-correspondence-binary-coproduct-Decomposition X))) equiv-eq-binary-coproduct-Decomposition : - (Y : binary-coproduct-Decomposition l2 l3 A) → (X ＝ Y) → + (Y : binary-coproduct-Decomposition l2 l3 A) → + (X ＝ Y) → equiv-binary-coproduct-Decomposition X Y equiv-eq-binary-coproduct-Decomposition .X refl = id-equiv-binary-coproduct-Decomposition - is-equiv-equiv-eq-binary-coproduct-Decomposition : - (Y : binary-coproduct-Decomposition l2 l3 A) → - is-equiv (equiv-eq-binary-coproduct-Decomposition Y) - is-equiv-equiv-eq-binary-coproduct-Decomposition = - fundamental-theorem-id - is-torsorial-equiv-binary-coproduct-Decomposition - equiv-eq-binary-coproduct-Decomposition + abstract + is-equiv-equiv-eq-binary-coproduct-Decomposition : + (Y : binary-coproduct-Decomposition l2 l3 A) → + is-equiv (equiv-eq-binary-coproduct-Decomposition Y) + is-equiv-equiv-eq-binary-coproduct-Decomposition = + fundamental-theorem-id + ( is-torsorial-equiv-binary-coproduct-Decomposition) + ( equiv-eq-binary-coproduct-Decomposition) extensionality-binary-coproduct-Decomposition : (Y : binary-coproduct-Decomposition l2 l3 A) → @@ -232,38 +249,44 @@ module _ ```agda module _ - {l1 : Level} - (X : UU l1) + {l1 : Level} {X : UU l1} (f : X → Fin 2) where - module _ - (f : X → Fin 2) - where - - matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - (X ≃ ((fiber f (inl (inr star))) + (fiber f (inr star)))) - matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ = - ( ( equiv-coproduct - ( left-unit-law-Σ-is-contr ( is-contr-Fin-1) ( inr star)) - ( left-unit-law-Σ-is-contr is-contr-unit star)) ∘e - ( ( right-distributive-Σ-coproduct (λ x → fiber f x) ∘e - ( inv-equiv-total-fiber f)))) - - compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - (x : X) → - (inl (inr star) ＝ f x) → - Σ ( Σ ( fiber f (inl (inr star))) - ( λ y → - inl y ＝ - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) - ( x)))) - ( λ z → pr1 (pr1 z) ＝ x) - compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - x p = - tr - ( λ a → - Σ ( Σ ( fiber f (inl (inr star))) + matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 : + X ≃ fiber f (inl (inr star)) + fiber f (inr star) + matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 = + ( equiv-coproduct + ( left-unit-law-Σ-is-contr (is-contr-Fin-1) (inr star)) + ( left-unit-law-Σ-is-contr is-contr-unit star)) ∘e + ( right-distributive-Σ-coproduct (λ x → fiber f x)) ∘e + ( inv-equiv-total-fiber f) + + map-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 : + X → fiber f (inl (inr star)) + fiber f (inr star) + map-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 = + map-equiv + ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2) + + map-inv-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 : + fiber f (inl (inr star)) + fiber f (inr star) → X + map-inv-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 = + map-inv-equiv + ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2) + + compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 : + (x : X) → + (inl (inr star) ＝ f x) → + Σ ( Σ ( fiber f (inl (inr star))) + ( λ y → + inl y ＝ + map-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( x))) + ( λ z → pr1 (pr1 z) ＝ x) + compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + x p = + tr + ( λ a → + Σ ( Σ ( fiber f (inl (inr star))) ( λ y → inl y ＝ ( map-coproduct @@ -274,241 +297,239 @@ module _ ( map-right-distributive-Σ-coproduct ( λ x → fiber f x) ( pr1 a , x , pr2 a)))) - ( λ z → pr1 (pr1 z) ＝ x)) - ( eq-pair-Σ p ( tr-Id-right p (inv p) ∙ left-inv p)) - ( ( ( x , (inv p)) , - ( ap - ( inl) - ( inv - ( map-inv-eq-transpose-equiv - ( left-unit-law-Σ-is-contr is-contr-Fin-1 (inr star)) - ( refl))))) , - refl) - - compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ : - (y : fiber f (inl (inr star))) → - pr1 y ＝ - map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) - ( inl y) - compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ - y = - map-eq-transpose-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) - ( inv + ( λ z → pr1 (pr1 z) ＝ x)) + ( eq-pair-Σ p (tr-Id-right p (inv p) ∙ left-inv p)) + ( ( ( x , inv p) , + ( ap + ( inl) + ( inv + ( map-inv-eq-transpose-equiv + ( left-unit-law-Σ-is-contr is-contr-Fin-1 (inr star)) + ( refl))))) , + ( refl)) + + compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-2 : + (y : fiber f (inl (inr star))) → + pr1 y ＝ + map-inv-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( inl y) + compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-2 + y = + map-eq-transpose-equiv + ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2) + ( ( inv ( pr2 ( pr1 - ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 ( pr1 y) - ( inv (pr2 y))))) ∙ - ap - inl + ( inv (pr2 y)))))) ∙ + ( ap + ( inl) ( eq-pair-Σ ( pr2 - ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 ( pr1 y) ( inv (pr2 y)))) - ( eq-is-prop (is-set-Fin 2 _ _)))) - - compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - (x : X) → - (inr star ＝ f x) → - Σ ( Σ ( fiber f (inr star)) - ( λ y → - inr y ＝ - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) - ( x)))) - ( λ z → pr1 (pr1 z) ＝ x) - compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - x p = - tr - ( λ a → - Σ ( Σ ( fiber f (inr star)) - ( λ y → - inr y ＝ - ( map-coproduct - ( map-left-unit-law-Σ-is-contr - ( is-contr-Fin-1) - ( inr star)) - ( map-left-unit-law-Σ-is-contr is-contr-unit star)) - ( map-right-distributive-Σ-coproduct - ( λ x → fiber f x) - ( pr1 a , x , pr2 a)))) - ( λ z → pr1 (pr1 z) ＝ x)) - ( eq-pair-Σ p ( tr-Id-right p (inv p) ∙ left-inv p)) - ( ( ( x , (inv p)) , - ( ap - ( inr) - ( inv - ( map-inv-eq-transpose-equiv - ( left-unit-law-Σ-is-contr is-contr-unit star) - ( refl))))) , - refl) - - compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ : - (y : fiber f (inr star)) → - pr1 y ＝ - map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) - ( inr y) - compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ - y = - map-eq-transpose-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) - ( inv - ( pr2 - ( pr1 - ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( eq-is-prop (is-set-Fin 2 _ _))))) + + compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 : + (x : X) → + (inr star ＝ f x) → + Σ ( Σ ( fiber f (inr star)) + ( λ y → + inr y ＝ + map-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( x))) + ( λ z → pr1 (pr1 z) ＝ x) + compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + x p = + tr + ( λ a → + Σ ( Σ ( fiber f (inr star)) + ( λ y → + inr y ＝ + ( map-coproduct + ( map-left-unit-law-Σ-is-contr + ( is-contr-Fin-1) + ( inr star)) + ( map-left-unit-law-Σ-is-contr is-contr-unit star)) + ( map-right-distributive-Σ-coproduct + ( λ x → fiber f x) + ( pr1 a , x , pr2 a)))) + ( λ z → pr1 (pr1 z) ＝ x)) + ( eq-pair-Σ p (tr-Id-right p (inv p) ∙ left-inv p)) + ( ( ( x , (inv p)) , + ( ap + ( inr) + ( inv + ( map-inv-eq-transpose-equiv + ( left-unit-law-Σ-is-contr is-contr-unit star) + ( refl))))) , + ( refl)) + + compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-2 : + (y : fiber f (inr star)) → + pr1 y ＝ + map-inv-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( inr y) + compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-2 + y = + map-eq-transpose-equiv + ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2) + ( inv + ( pr2 + ( pr1 + ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( pr1 y) + ( inv (pr2 y))))) ∙ + ap + inr + ( eq-pair-Σ + ( pr2 + ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 ( pr1 y) - ( inv (pr2 y))))) ∙ - ap - inr - ( eq-pair-Σ - ( pr2 - ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( pr1 y) - ( inv (pr2 y)))) - ( eq-is-prop (is-set-Fin 2 _ _)))) - - map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - binary-coproduct-Decomposition l1 l1 X - pr1 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) = - fiber f (inl (inr star)) - pr1 (pr2 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)) = - fiber f (inr star) - pr2 (pr2 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ)) = - matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper : + ( inv (pr2 y)))) + ( eq-is-prop (is-set-Fin 2 (f (pr1 y)) (inr star))))) + + map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : + binary-coproduct-Decomposition l1 l1 X + pr1 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-2) = + fiber f (inl (inr star)) + pr1 (pr2 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-2)) = + fiber f (inr star) + pr2 (pr2 (map-equiv-binary-coproduct-Decomposition-map-into-Fin-2)) = + matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + +module _ + {l1 : Level} {X : UU l1} + where + + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper : (d : binary-coproduct-Decomposition l1 l1 X) → - ( left-summand-binary-coproduct-Decomposition d + - right-summand-binary-coproduct-Decomposition d) → + left-summand-binary-coproduct-Decomposition d + + right-summand-binary-coproduct-Decomposition d → Fin 2 - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d (inl _) = inl (inr star) - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d (inr _) = inr star - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - (d : binary-coproduct-Decomposition l1 l1 X) → - X → Fin 2 - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d x = - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : + binary-coproduct-Decomposition l1 l1 X → X → Fin 2 + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d x = + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper ( d) - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition d) - ( x)) + ( map-matching-correspondence-binary-coproduct-Decomposition d x) - compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper : + compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper : (d : binary-coproduct-Decomposition l1 l1 X) → (t : ( left-summand-binary-coproduct-Decomposition d) + ( right-summand-binary-coproduct-Decomposition d)) → ( inl (inr star) ＝ - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper ( d) ( t)) → Σ ( left-summand-binary-coproduct-Decomposition d) ( λ a → inl a ＝ t) - compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d (inl y) x = y , refl - compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : (d : binary-coproduct-Decomposition l1 l1 X) → (x : X) → ( inl (inr star) ＝ - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d x) → + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d x) → Σ ( left-summand-binary-coproduct-Decomposition d) ( λ a → inl a ＝ - map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x) - compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + map-matching-correspondence-binary-coproduct-Decomposition d x) + compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d x p = - compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper ( d) - ( map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x) + ( map-matching-correspondence-binary-coproduct-Decomposition d x) ( p) - compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper : + compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper : (d : binary-coproduct-Decomposition l1 l1 X) → (t : ( left-summand-binary-coproduct-Decomposition d) + ( right-summand-binary-coproduct-Decomposition d)) → ( inr star ＝ - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper ( d) ( t)) → Σ ( right-summand-binary-coproduct-Decomposition d) ( λ a → inr a ＝ t) - compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d (inr y) x = y , refl - compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : (d : binary-coproduct-Decomposition l1 l1 X) → (x : X) → ( inr star ＝ - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d x) → + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d x) → Σ ( right-summand-binary-coproduct-Decomposition d) ( λ a → inr a ＝ - map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x) - compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + map-matching-correspondence-binary-coproduct-Decomposition d x) + compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d x p = - compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper ( d) - ( map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x) + ( map-matching-correspondence-binary-coproduct-Decomposition d x) ( p) - is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper : + is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper : (f : X → Fin 2) → (x : X) → (v : (inl (inr star) ＝ f x) + (inr star ＝ f x)) → - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ f) x ＝ + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 f) x ＝ f x) - is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper f x (inl y) = ( inv ( ap - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper - ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ f)) + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 f)) ( pr2 ( pr1 - ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - f - x - y)))) ∙ - y) - is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( f) + ( x) + ( y))))) ∙ + ( y)) + is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper f x (inr y) = ( inv ( ap ( λ p → - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper - ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ f) + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 f) ( p)) ( pr2 ( pr1 - ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - f - x - y)))) ∙ - y) - - is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ ∘ - map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) ~ - id - is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( f) + ( x) + ( y))))) ∙ + ( y)) + + is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : + is-retraction + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2) + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2) + is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 f = eq-htpy ( λ x → - is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper ( f) ( x) ( map-coproduct @@ -518,72 +539,90 @@ module _ ( λ y → y ＝ f x) ( f x , refl)))) - equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : (d : binary-coproduct-Decomposition l1 l1 X) → left-summand-binary-coproduct-Decomposition - ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d)) ≃ + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d)) ≃ left-summand-binary-coproduct-Decomposition d - equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + d = + ( right-unit-law-coproduct + ( left-summand-binary-coproduct-Decomposition d)) ∘e + ( equiv-coproduct + ( right-unit-law-Σ-is-contr (λ _ → is-contr-unit) ∘e + equiv-tot + ( λ _ → extensionality-Fin 2 (inl (inr star)) (inl (inr star)))) + ( right-absorption-Σ (right-summand-binary-coproduct-Decomposition d) ∘e + equiv-tot (λ _ → extensionality-Fin 2 (inr star) (inl (inr star))))) ∘e + ( right-distributive-Σ-coproduct + ( λ y → + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper + d y ＝ inl (inr star))) ∘e + ( equiv-Σ-equiv-base + ( λ y → + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper + d y ＝ + inl (inr star)) + ( matching-correspondence-binary-coproduct-Decomposition d)) + + map-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : + (d : binary-coproduct-Decomposition l1 l1 X) → + left-summand-binary-coproduct-Decomposition + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d)) → + left-summand-binary-coproduct-Decomposition d + map-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + d = + map-equiv + ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) + + equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : + (d : binary-coproduct-Decomposition l1 l1 X) → + right-summand-binary-coproduct-Decomposition + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d)) ≃ + right-summand-binary-coproduct-Decomposition d + equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d = - ( ( right-unit-law-coproduct - ( left-summand-binary-coproduct-Decomposition d)) ∘e - ( ( equiv-coproduct - ( right-unit-law-Σ-is-contr (λ _ → is-contr-unit) ∘e - equiv-tot - ( λ _ → extensionality-Fin 2 (inl (inr star)) (inl (inr star)))) - ( right-absorption-Σ - (right-summand-binary-coproduct-Decomposition d) ∘e - equiv-tot - ( λ _ → extensionality-Fin 2 (inr star) (inl (inr star))))) ∘e - ( ( right-distributive-Σ-coproduct - ( λ y → - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper - d y ＝ inl (inr star))) ∘e - ( equiv-Σ-equiv-base - ( λ y → - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper - d y ＝ inl (inr star)) - ( matching-correspondence-binary-coproduct-Decomposition d))))) - - equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + ( left-unit-law-coproduct + ( right-summand-binary-coproduct-Decomposition d)) ∘e + ( equiv-coproduct + ( right-absorption-Σ (left-summand-binary-coproduct-Decomposition d) ∘e + equiv-tot (λ _ → extensionality-Fin 2 (inl (inr star)) (inr star))) + ( right-unit-law-Σ-is-contr (λ _ → is-contr-unit) ∘e + equiv-tot (λ _ → extensionality-Fin 2 (inr star) (inr star)))) ∘e + ( ( right-distributive-Σ-coproduct + ( λ y → + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper + d y ＝ inr star)) ∘e + ( equiv-Σ-equiv-base + ( λ y → + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper + d y) ＝ + ( inr star)) + ( matching-correspondence-binary-coproduct-Decomposition d))) + + map-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : (d : binary-coproduct-Decomposition l1 l1 X) → right-summand-binary-coproduct-Decomposition - ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d)) ≃ + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d)) → right-summand-binary-coproduct-Decomposition d - equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + map-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d = - ( ( left-unit-law-coproduct - ( right-summand-binary-coproduct-Decomposition d)) ∘e - ( ( equiv-coproduct - ( right-absorption-Σ - ( left-summand-binary-coproduct-Decomposition d) ∘e - equiv-tot - ( λ _ → extensionality-Fin 2 (inl (inr star)) (inr star))) - ( right-unit-law-Σ-is-contr (λ _ → is-contr-unit) ∘e - equiv-tot - ( λ _ → extensionality-Fin 2 (inr star) (inr star)))) ∘e - ( ( right-distributive-Σ-coproduct - ( λ y → - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper - d y ＝ inr star)) ∘e - ( equiv-Σ-equiv-base - ( λ y → - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper - d y) ＝ - ( inr star)) - ( matching-correspondence-binary-coproduct-Decomposition d))))) - - compute-equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + map-equiv + ( equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) + + compute-equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : ( d : binary-coproduct-Decomposition l1 l1 X) → ( inl ∘ - ( map-equiv - ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d)))) ~ - ( ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition d)) ∘ pr1) - compute-equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( map-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d))) ~ + ( map-matching-correspondence-binary-coproduct-Decomposition d ∘ pr1) + compute-equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d (x , p) = ap ( λ x → @@ -603,7 +642,7 @@ module _ extensionality-Fin 2 (inr star) (inl (inr star))))) ∘e ( ( right-distributive-Σ-coproduct ( λ y → - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d y ＝ inl (inr star)))))) ( x))) @@ -612,32 +651,30 @@ module _ pair ( inl ( pr1 - ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d x (inv p)))) ( refl)} ( inv ( pr2 - ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( x) ( inv p)))) ( eq-is-prop ( is-set-Fin 2 _ _))) ∙ ( pr2 - ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( x) ( inv p))) - compute-equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + compute-equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : ( d : binary-coproduct-Decomposition l1 l1 X) → ( inr ∘ - ( map-equiv - ( equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d)))) ~ - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition d) ∘ pr1) - compute-equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( map-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d))) ~ + ( map-matching-correspondence-binary-coproduct-Decomposition d ∘ pr1) + compute-equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d (x , p) = ap ( λ x → @@ -656,212 +693,200 @@ module _ ( λ _ → extensionality-Fin 2 (inr star) (inr star)))) ∘e ( ( right-distributive-Σ-coproduct ( λ y → - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d y ＝ inr star))))) ( x))) ( eq-pair-Σ { t = ( inr ( pr1 - ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( x) ( inv p))) , refl)} ( inv ( pr2 - ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( x) ( inv p)))) ( eq-is-prop ( is-set-Fin 2 _ _))) ∙ ( pr2 - ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-right-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( x) ( inv p))) - matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper : + matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper : ( d : binary-coproduct-Decomposition l1 l1 X) → ( x : X) → ( ( inl (inr star) ＝ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( x))) + ( inr star ＝ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( x)))) → ( map-coproduct - ( map-equiv - ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d))) - ( map-equiv - ( equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d))) ∘ - map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d))) + ( map-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) + ( map-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) ∘ + map-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d)) ( x) ＝ - map-equiv (matching-correspondence-binary-coproduct-Decomposition d) x - matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + map-matching-correspondence-binary-coproduct-Decomposition d x + matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d x (inl p) = - ap + ( ap ( map-coproduct - ( map-equiv - ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d))) - ( map-equiv - ( equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d)))) + ( map-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) + ( map-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d))) ( inv ( pr2 ( pr1 - ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d)) ( x) - ( p))))) ∙ - ( compute-equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( p)))))) ∙ + ( compute-equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) ( pr1 ( pr1 ( pr1 - ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d)) ( x) ( p)))) , ( pr2 ( pr1 ( pr1 - ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d)) ( x) - ( p)))))) ∙ - ap - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition d)) + ( p))))))) ∙ + ( ap + ( map-matching-correspondence-binary-coproduct-Decomposition d) ( pr2 - ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d)) ( x) ( p)))) - matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper d x (inr p) = - ap + ( ap ( map-coproduct - ( map-equiv - ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d))) - ( map-equiv - ( equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d)))) + ( map-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) + ( map-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d))) ( inv ( pr2 ( pr1 - ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d)) ( x) - ( p))))) ∙ - ( compute-equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d) - ( pr1 + ( p)))))) ∙ + ( compute-equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d) ( pr1 - ( pr1 - ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d)) - ( x) - ( p)))) , - pr2 ( pr1 ( pr1 - ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d)) ( x) - ( p))))) ∙ - ap - ( map-equiv - ( matching-correspondence-binary-coproduct-Decomposition d)) + ( p)))) , + pr2 + ( pr1 + ( pr1 + ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) + ( x) + ( p)))))) ∙ + ( ap + ( map-matching-correspondence-binary-coproduct-Decomposition d) ( pr2 - ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d)) - ( x) - ( p)))) + ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) + ( x) + ( p)))) - value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper : + value-map-into-Fin-2-eq-zero-or-one-helper : (y : Fin 2) → (inl (inr star) ＝ y) + (inr star ＝ y) - value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper (inl x) = + value-map-into-Fin-2-eq-zero-or-one-helper (inl x) = inl (ap inl (eq-is-contr is-contr-Fin-1)) - value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper (inr x) = + value-map-into-Fin-2-eq-zero-or-one-helper (inr x) = inr (ap inr (eq-is-contr is-contr-unit)) - value-map-into-Fin-Two-ℕ-eq-zero-or-one : + value-map-into-Fin-2-eq-zero-or-one : (f : X → Fin 2) → (x : X) → (inl (inr star) ＝ f x) + (inr star ＝ f x) - value-map-into-Fin-Two-ℕ-eq-zero-or-one f x = - value-map-into-Fin-Two-ℕ-eq-zero-or-one-helper (f x) + value-map-into-Fin-2-eq-zero-or-one f x = + value-map-into-Fin-2-eq-zero-or-one-helper (f x) - matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : ( d : binary-coproduct-Decomposition l1 l1 X) → ( map-coproduct - ( map-equiv - ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d))) - ( map-equiv - ( equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d))) ∘ - map-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - (map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( d)))) ~ - map-equiv (matching-correspondence-binary-coproduct-Decomposition d) - matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( map-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d))) + ( map-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d)) ∘ + ( map-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-2 + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + ( d))) ~ + map-matching-correspondence-binary-coproduct-Decomposition d + matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d x = - matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ-helper + matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2-helper ( d) ( x) - ( value-map-into-Fin-Two-ℕ-eq-zero-or-one - ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d) + ( value-map-into-Fin-2-eq-zero-or-one + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d) ( x)) - is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ ∘ - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) ~ - id - is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ d = + is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : + is-section + ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2) + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2) + is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 d = eq-equiv-binary-coproduct-Decomposition - ( ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ ∘ - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) + ( ( map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ∘ + map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2) ( d)) ( d) - ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + ( equiv-left-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) , - equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + equiv-right-summand-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d) , - matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + matching-correspondence-htpy-is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ( d)) - is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : - is-equiv map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ = + is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 : + is-equiv map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 = is-equiv-is-invertible - map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) - ( is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ) + ( map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2) + ( is-section-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2) + ( is-retraction-map-inv-equiv-binary-coproduct-Decomposition-map-into-Fin-2) - equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ : + equiv-binary-coproduct-Decomposition-map-into-Fin-2 : (X → Fin 2) ≃ binary-coproduct-Decomposition l1 l1 X - pr1 equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ = - map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - pr2 equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ = - is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ + pr1 equiv-binary-coproduct-Decomposition-map-into-Fin-2 = + map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 + pr2 equiv-binary-coproduct-Decomposition-map-into-Fin-2 = + is-equiv-map-equiv-binary-coproduct-Decomposition-map-into-Fin-2 ``` diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md index 70856d62e23..a71085432f8 100644 --- a/src/foundation/decidable-embeddings.lagda.md +++ b/src/foundation/decidable-embeddings.lagda.md @@ -9,12 +9,15 @@ module foundation.decidable-embeddings where ```agda open import foundation.action-on-identifications-functions open import foundation.cartesian-morphisms-arrows +open import foundation.complements-images open import foundation.decidable-maps open import foundation.decidable-propositions open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.embeddings +open import foundation.equality-coproduct-types open import foundation.fibers-of-maps +open import foundation.full-subtypes open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-coproduct-types open import foundation.fundamental-theorem-of-identity-types @@ -26,6 +29,7 @@ open import foundation.propositions open import foundation.retracts-of-maps open import foundation.small-maps open import foundation.subtype-identity-principle +open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universal-property-equivalences @@ -544,10 +548,6 @@ module _ ### Coproducts of decidable embeddings are decidable embeddings ```agda -module _ - {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'} - where - abstract is-decidable-emb-map-coproduct : {l1 l2 l3 l4 : Level} @@ -560,6 +560,20 @@ abstract ( is-emb-map-coproduct eF eG , is-decidable-map-coproduct dF dG) ``` +### The inclusion maps of coproducts are decidable embeddings + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-decidable-emb-inl : is-decidable-emb (inl {A = A} {B = B}) + is-decidable-emb-inl = (is-emb-inl , is-decidable-map-inl) + + is-decidable-emb-inr : is-decidable-emb (inr {A = A} {B = B}) + is-decidable-emb-inr = (is-emb-inr , is-decidable-map-inr) +``` + ### Decidable embeddings are closed under base change ```agda @@ -670,6 +684,30 @@ module _ is-small-map-decidable-emb (f , H) = is-small-map-is-decidable-emb H ``` +## The coproduct decomposition of the codomain of a decidable embedding + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + coproduct-decomposition-codomain-decidable-emb : + (f'@(f , F) : decidable-emb A B) → + B ≃ A + nonim f + coproduct-decomposition-codomain-decidable-emb (f , F) = + equivalence-reasoning + B + ≃ Σ B (λ y → is-decidable (fiber f y)) + by inv-equiv-inclusion-is-full-subtype + ( λ y → + is-decidable-Prop (fiber f y , (is-prop-map-is-decidable-emb F y))) + ( is-decidable-map-is-decidable-emb F) + ≃ Σ B (fiber f) + nonim f + by left-distributive-Σ-coproduct + ≃ A + nonim f + by equiv-coproduct (equiv-total-fiber f) id-equiv +``` + ## References Decidable embeddings are discussed in {{#cite Warn24}} under the name diff --git a/src/foundation/decidable-maps.lagda.md b/src/foundation/decidable-maps.lagda.md index 89cb4cd7183..5a10451cc4c 100644 --- a/src/foundation/decidable-maps.lagda.md +++ b/src/foundation/decidable-maps.lagda.md @@ -296,6 +296,24 @@ module _ is-decidable-equiv' (compute-fiber-inr-map-coproduct f g y) (G y) ``` +### The inclusion maps of coproducts are decidable + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-decidable-map-inl : + is-decidable-map (inl {A = A} {B = B}) + is-decidable-map-inl (inl x) = inl (x , refl) + is-decidable-map-inl (inr x) = inr (λ (y , p) → neq-inl-inr p) + + is-decidable-map-inr : + is-decidable-map (inr {A = A} {B = B}) + is-decidable-map-inr (inl x) = inr (λ (y , p) → neq-inr-inl p) + is-decidable-map-inr (inr x) = inl (x , refl) +``` + ### Decidable maps are closed under base change ```agda diff --git a/src/foundation/decidable-retracts-of-types.lagda.md b/src/foundation/decidable-retracts-of-types.lagda.md new file mode 100644 index 00000000000..2634601db3d --- /dev/null +++ b/src/foundation/decidable-retracts-of-types.lagda.md @@ -0,0 +1,272 @@ +# Decidable retracts of types + +```agda +module foundation.decidable-retracts-of-types where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.complements-images +open import foundation.coproduct-types +open import foundation.decidable-embeddings +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.fundamental-theorem-of-identity-types +open import foundation.logical-equivalences +open import foundation.retracts-of-types +open import foundation.subtype-identity-principle +open import foundation.torsorial-type-families +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.injective-maps +open import foundation-core.postcomposition-functions +open import foundation-core.precomposition-functions +open import foundation-core.retractions +open import foundation-core.sections +``` + +
+ +## Idea + +A {{#concept "decidable retract" Disambiguation="of types"}} `A` of a type `B` +is the data of pair of maps + +```text + i r + A ----> B ----> A +``` + +such that `r ∘ i ~ id`, where `i` is a +[decidable embedding](foundation.decidable-embeddings.md). Equivalently, it is a +decomposition of `B` as a [coproduct](foundation.coproduct-types.md) `A + C` +together with a map `C → A`. + +## Definitions + +### The type of witnesses that `A` is a decidable retract of `B` + +```agda +decidable-retract : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +decidable-retract B A = + Σ (retract B A) (λ R → is-decidable-emb (inclusion-retract R)) + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (R : decidable-retract B A) + where + + retract-decidable-retract : retract B A + retract-decidable-retract = pr1 R + + inclusion-decidable-retract : A → B + inclusion-decidable-retract = inclusion-retract retract-decidable-retract + + retraction-decidable-retract : retraction inclusion-decidable-retract + retraction-decidable-retract = retraction-retract retract-decidable-retract + + map-retraction-decidable-retract : B → A + map-retraction-decidable-retract = + map-retraction-retract retract-decidable-retract + + is-retraction-map-retraction-decidable-retract : + is-section map-retraction-decidable-retract inclusion-decidable-retract + is-retraction-map-retraction-decidable-retract = + is-retraction-map-retraction-retract retract-decidable-retract + + section-decidable-retract : section map-retraction-decidable-retract + section-decidable-retract = section-retract retract-decidable-retract + + is-decidable-emb-inclusion-decidable-retract : + is-decidable-emb inclusion-decidable-retract + is-decidable-emb-inclusion-decidable-retract = pr2 R + + decidable-emb-inclusion-decidable-retract : A ↪ᵈ B + decidable-emb-inclusion-decidable-retract = + ( inclusion-decidable-retract , + is-decidable-emb-inclusion-decidable-retract) + + iff-decidable-retract : A ↔ B + iff-decidable-retract = iff-retract retract-decidable-retract + + iff-decidable-retract' : B ↔ A + iff-decidable-retract' = iff-retract' retract-decidable-retract +``` + +### The type of decidable retracts of a type + +```agda +decidable-retracts : {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) +decidable-retracts l2 A = Σ (UU l2) (decidable-retract A) + +module _ + {l1 l2 : Level} {A : UU l1} (R : decidable-retracts l2 A) + where + + type-decidable-retracts : UU l2 + type-decidable-retracts = pr1 R + + decidable-retract-decidable-retracts : + decidable-retract A type-decidable-retracts + decidable-retract-decidable-retracts = pr2 R + + retract-decidable-retracts : type-decidable-retracts retract-of A + retract-decidable-retracts = + retract-decidable-retract decidable-retract-decidable-retracts + + inclusion-decidable-retracts : type-decidable-retracts → A + inclusion-decidable-retracts = + inclusion-retract retract-decidable-retracts + + retraction-decidable-retracts : retraction inclusion-decidable-retracts + retraction-decidable-retracts = + retraction-retract retract-decidable-retracts + + map-retraction-decidable-retracts : A → type-decidable-retracts + map-retraction-decidable-retracts = + map-retraction-retract retract-decidable-retracts + + is-retraction-map-retraction-decidable-retracts : + is-section map-retraction-decidable-retracts inclusion-decidable-retracts + is-retraction-map-retraction-decidable-retracts = + is-retraction-map-retraction-retract retract-decidable-retracts + + section-decidable-retracts : section map-retraction-decidable-retracts + section-decidable-retracts = + section-retract retract-decidable-retracts +``` + +### The identity decidable retract + +```agda +module _ + {l : Level} {A : UU l} + where + + id-decidable-retract : decidable-retract A A + id-decidable-retract = (id-retract , is-decidable-emb-id) +``` + +### Composition of decidable retracts + +```agda +comp-decidable-retract : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} → + decidable-retract C B → decidable-retract B A → decidable-retract C A +comp-decidable-retract (r , H) (r' , H') = + ( comp-retract r r' , is-decidable-emb-comp H H') +``` + +## Properties + +### Characterization of equality of decidable retracts + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + htpy-decidable-retract : + (R S : decidable-retract B A) → UU (l1 ⊔ l2) + htpy-decidable-retract R S = + htpy-retract (retract-decidable-retract R) (retract-decidable-retract S) + + refl-htpy-decidable-retract : + (R : decidable-retract B A) → htpy-decidable-retract R R + refl-htpy-decidable-retract R = + refl-htpy-retract (retract-decidable-retract R) + + htpy-eq-decidable-retract : + (R S : decidable-retract B A) → R ＝ S → htpy-decidable-retract R S + htpy-eq-decidable-retract R S p = + htpy-eq-retract + ( retract-decidable-retract R) + ( retract-decidable-retract S) + ( ap retract-decidable-retract p) + + abstract + is-torsorial-htpy-decidable-retract : + (R : decidable-retract B A) → is-torsorial (htpy-decidable-retract R) + is-torsorial-htpy-decidable-retract R = + is-torsorial-Eq-subtype + ( is-torsorial-htpy-retract (retract-decidable-retract R)) + ( λ S → is-prop-is-decidable-emb (inclusion-retract S)) + ( retract-decidable-retract R) + ( refl-htpy-decidable-retract R) + ( is-decidable-emb-inclusion-decidable-retract R) + + abstract + is-equiv-htpy-eq-decidable-retract : + (R S : decidable-retract B A) → is-equiv (htpy-eq-decidable-retract R S) + is-equiv-htpy-eq-decidable-retract R = + fundamental-theorem-id + ( is-torsorial-htpy-decidable-retract R) + ( htpy-eq-decidable-retract R) + + extensionality-decidable-retract : + (R S : decidable-retract B A) → (R ＝ S) ≃ htpy-decidable-retract R S + extensionality-decidable-retract R S = + ( htpy-eq-decidable-retract R S , is-equiv-htpy-eq-decidable-retract R S) + + eq-htpy-decidable-retract : + (R S : decidable-retract B A) → htpy-decidable-retract R S → R ＝ S + eq-htpy-decidable-retract R S = + map-inv-is-equiv (is-equiv-htpy-eq-decidable-retract R S) +``` + +### The associated coproduct decomposition of a decidable retract + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + coproduct-decomposition-nonim-decidable-retract : + (R : decidable-retract A B) → A ≃ B + nonim (inclusion-decidable-retract R) + coproduct-decomposition-nonim-decidable-retract R = + coproduct-decomposition-codomain-decidable-emb + ( decidable-emb-inclusion-decidable-retract R) +``` + +### The coproduct decomposition characterization of decidable retracts + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + map-coproduct-decomposition-decidable-retract : + decidable-retract A B → + Σ (UU (l1 ⊔ l2)) (λ C → (A ≃ B + C) × (C → B)) + map-coproduct-decomposition-decidable-retract R = + ( nonim (inclusion-decidable-retract R) , + coproduct-decomposition-nonim-decidable-retract R , + ( map-retraction-decidable-retract R ∘ + inclusion-nonim (inclusion-decidable-retract R))) + + map-inv-coproduct-decomposition-decidable-retract : + Σ (UU (l1 ⊔ l2)) (λ C → (A ≃ B + C) × (C → B)) → + decidable-retract A B + map-inv-coproduct-decomposition-decidable-retract (C , e , f) = + ( map-inv-equiv e ∘ inl , + rec-coproduct id f ∘ map-equiv e , + is-retraction-map-retraction-comp + ( map-inv-equiv e) + ( inl) + ( map-equiv e , is-section-map-inv-equiv e) + ( rec-coproduct id f , refl-htpy)) , + is-decidable-emb-comp + ( is-decidable-emb-is-equiv (is-equiv-map-inv-equiv e)) + ( is-decidable-emb-inl) +``` + +> It remains to show that these two constructions form mutual inverses. diff --git a/src/foundation/decidable-subtypes.lagda.md b/src/foundation/decidable-subtypes.lagda.md index d54451386b6..b8f704e6b10 100644 --- a/src/foundation/decidable-subtypes.lagda.md +++ b/src/foundation/decidable-subtypes.lagda.md @@ -31,6 +31,7 @@ open import foundation.postcomposition-functions open import foundation.propositional-maps open import foundation.raising-universe-levels open import foundation.sets +open import foundation.split-surjective-maps open import foundation.structured-type-duality open import foundation.subtypes open import foundation.surjective-maps @@ -518,20 +519,32 @@ module _ map-maybe-decidable-subtype (x , inl x∈S) = unit-Maybe (x , x∈S) map-maybe-decidable-subtype (x , inr x∉S) = exception-Maybe + is-split-surjective-extend-map-maybe-decidable-subtype : + is-split-surjective (extend-Maybe map-maybe-decidable-subtype) + is-split-surjective-extend-map-maybe-decidable-subtype (inr star) = + ( exception-Maybe , refl) + is-split-surjective-extend-map-maybe-decidable-subtype (inl (x , x∈S)) = + ( unit-Maybe (x , inl x∈S) , refl) + abstract is-surjective-extend-map-maybe-decidable-subtype : is-surjective (extend-Maybe map-maybe-decidable-subtype) - is-surjective-extend-map-maybe-decidable-subtype (inr star) = - intro-exists exception-Maybe refl - is-surjective-extend-map-maybe-decidable-subtype (inl (x , x∈S)) = - intro-exists (unit-Maybe (x , inl x∈S)) refl + is-surjective-extend-map-maybe-decidable-subtype = + is-surjective-is-split-surjective + ( is-split-surjective-extend-map-maybe-decidable-subtype) + + surjection-extend-map-maybe-decidable-subtype : + Maybe (Σ X (is-decidable ∘ is-in-decidable-subtype S)) ↠ + Maybe (type-decidable-subtype S) + surjection-extend-map-maybe-decidable-subtype = + ( extend-Maybe map-maybe-decidable-subtype , + is-surjective-extend-map-maybe-decidable-subtype) surjection-maybe-decidable-subtype : Maybe X ↠ Maybe (type-decidable-subtype S) surjection-maybe-decidable-subtype = comp-surjection - ( extend-Maybe map-maybe-decidable-subtype , - is-surjective-extend-map-maybe-decidable-subtype) + ( surjection-extend-map-maybe-decidable-subtype) ( surjection-map-surjection-Maybe ( surjection-equiv (equiv-Σ-decide-is-in-decidable-subtype S))) ``` diff --git a/src/foundation/dependent-binomial-theorem.lagda.md b/src/foundation/dependent-binomial-theorem.lagda.md index d86a4ac3786..7b59e469cbc 100644 --- a/src/foundation/dependent-binomial-theorem.lagda.md +++ b/src/foundation/dependent-binomial-theorem.lagda.md @@ -26,6 +26,8 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies +open import foundation-core.retractions +open import foundation-core.sections open import foundation-core.type-theoretic-principle-of-choice open import foundation-core.univalence @@ -49,8 +51,8 @@ module _ map-compute-total-fam-coproduct : Σ (Fin 2) fam-coproduct → A + B - map-compute-total-fam-coproduct (pair (inl (inr _)) y) = inl (map-inv-raise y) - map-compute-total-fam-coproduct (pair (inr _) y) = inr (map-inv-raise y) + map-compute-total-fam-coproduct (inl (inr _) , y) = inl (map-inv-raise y) + map-compute-total-fam-coproduct (inr _ , y) = inr (map-inv-raise y) map-inv-compute-total-fam-coproduct : A + B → Σ (Fin 2) fam-coproduct @@ -60,17 +62,21 @@ module _ pr2 (map-inv-compute-total-fam-coproduct (inr x)) = map-raise x is-section-map-inv-compute-total-fam-coproduct : - (map-compute-total-fam-coproduct ∘ map-inv-compute-total-fam-coproduct) ~ id + is-section + ( map-compute-total-fam-coproduct) + ( map-inv-compute-total-fam-coproduct) is-section-map-inv-compute-total-fam-coproduct (inl x) = ap inl (is-retraction-map-inv-raise {l2} x) is-section-map-inv-compute-total-fam-coproduct (inr x) = ap inr (is-retraction-map-inv-raise {l1} x) is-retraction-map-inv-compute-total-fam-coproduct : - map-inv-compute-total-fam-coproduct ∘ map-compute-total-fam-coproduct ~ id - is-retraction-map-inv-compute-total-fam-coproduct (pair (inl (inr _)) y) = + is-retraction + ( map-compute-total-fam-coproduct) + ( map-inv-compute-total-fam-coproduct) + is-retraction-map-inv-compute-total-fam-coproduct (inl (inr _) , y) = eq-pair-eq-fiber (is-section-map-inv-raise y) - is-retraction-map-inv-compute-total-fam-coproduct (pair (inr _) y) = + is-retraction-map-inv-compute-total-fam-coproduct (inr _ , y) = eq-pair-eq-fiber (is-section-map-inv-raise y) is-equiv-map-compute-total-fam-coproduct : @@ -98,36 +104,37 @@ module _ type-distributive-Π-coproduct : UU (l1 ⊔ l2 ⊔ l3) type-distributive-Π-coproduct = Σ ( X → Fin 2) - ( λ f → ((x : X) (p : is-zero-Fin 2 (f x)) → A x) × - ((x : X) (p : is-one-Fin 2 (f x)) → B x)) + ( λ f → + ((x : X) (p : is-zero-Fin 2 (f x)) → A x) × + ((x : X) (p : is-one-Fin 2 (f x)) → B x)) distributive-Π-coproduct : ((x : X) → A x + B x) ≃ type-distributive-Π-coproduct distributive-Π-coproduct = - ( ( equiv-tot - ( λ f → - ( ( equiv-product - ( equiv-Π-equiv-family - ( λ x → - equiv-Π-equiv-family - ( λ p → - ( inv-equiv (compute-raise l3 (A x))) ∘e - ( equiv-tr (fam-coproduct (A x) (B x)) p)))) - ( equiv-Π-equiv-family - ( λ x → - equiv-Π-equiv-family - ( λ p → - ( inv-equiv (compute-raise l2 (B x))) ∘e - ( equiv-tr (fam-coproduct (A x) (B x)) p))))) ∘e - ( distributive-Π-Σ)) ∘e + ( equiv-tot + ( λ f → + ( equiv-product + ( equiv-Π-equiv-family + ( λ x → + equiv-Π-equiv-family + ( λ p → + ( inv-equiv (compute-raise l3 (A x))) ∘e + ( equiv-tr (fam-coproduct (A x) (B x)) p)))) ( equiv-Π-equiv-family ( λ x → - ( equiv-universal-property-coproduct - ( fam-coproduct (A x) (B x) (f x))) ∘e - ( equiv-diagonal-exponential-is-contr - ( fam-coproduct (A x) (B x) (f x)) - ( is-contr-is-zero-or-one-Fin-2 (f x))))))) ∘e - ( distributive-Π-Σ)) ∘e + equiv-Π-equiv-family + ( λ p → + ( inv-equiv (compute-raise l2 (B x))) ∘e + ( equiv-tr (fam-coproduct (A x) (B x)) p))))) ∘e + ( distributive-Π-Σ) ∘e + ( equiv-Π-equiv-family + ( λ x → + ( equiv-universal-property-coproduct + ( fam-coproduct (A x) (B x) (f x))) ∘e + ( equiv-diagonal-exponential-is-contr + ( fam-coproduct (A x) (B x) (f x)) + ( is-contr-is-zero-or-one-Fin-2 (f x))))))) ∘e + ( distributive-Π-Σ) ∘e ( equiv-Π-equiv-family ( λ x → inv-compute-total-fam-coproduct (A x) (B x))) @@ -136,70 +143,47 @@ module _ type-distributive-Π-coproduct-binary-coproduct-Decomposition = Σ ( binary-coproduct-Decomposition l1 l1 X) ( λ d → - ( ( (u : left-summand-binary-coproduct-Decomposition d) → - ( A - ( map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition d) - ( inl u)))) × - ( ( v : right-summand-binary-coproduct-Decomposition d) → - ( B - ( map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition d) - ( inr v)))))) + ( (u : left-summand-binary-coproduct-Decomposition d) → + ( A + ( map-inv-matching-correspondence-binary-coproduct-Decomposition d + ( inl u)))) × + ( ( v : right-summand-binary-coproduct-Decomposition d) → + ( B + ( map-inv-matching-correspondence-binary-coproduct-Decomposition d + ( inr v))))) equiv-type-distributive-Π-coproduct-binary-coproduct-Decomposition : type-distributive-Π-coproduct ≃ type-distributive-Π-coproduct-binary-coproduct-Decomposition equiv-type-distributive-Π-coproduct-binary-coproduct-Decomposition = equiv-Σ - ( λ d → - ( (u : left-summand-binary-coproduct-Decomposition d) → - A - ( map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition d) - ( inl u))) × - ( (v : right-summand-binary-coproduct-Decomposition d) → - B - ( map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition d) - ( inr v)))) - ( equiv-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ X) + ( λ d → + ( (u : left-summand-binary-coproduct-Decomposition d) → + A ( map-inv-matching-correspondence-binary-coproduct-Decomposition d + ( inl u))) × + ( (v : right-summand-binary-coproduct-Decomposition d) → + B ( map-inv-matching-correspondence-binary-coproduct-Decomposition d + ( inr v)))) + ( equiv-binary-coproduct-Decomposition-map-into-Fin-2) ( λ f → equiv-product - ( equiv-Π - ( λ z → - A - ( map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - ( X) - ( f)) - ( inl z))) - ( id-equiv) - ( λ a → - equiv-eq - ( ap - ( A) - ( compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ - ( X) - ( f) - ( a)))) ∘e + ( equiv-Π-equiv-family + ( λ a → + equiv-eq + ( ap + ( A) + ( compute-left-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-2 + ( f) + ( a)))) ∘e inv-equiv equiv-ev-pair) - ( equiv-Π - ( λ z → - B - ( map-inv-equiv - ( matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ - X f) - ( inr z))) - ( id-equiv) - ( λ a → - equiv-eq - ( ap - ( B) - ( compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-Two-ℕ - ( X) - ( f) - ( a)))) ∘e + ( equiv-Π-equiv-family + ( λ a → + equiv-eq + ( ap + ( B) + ( compute-right-inv-matching-correspondence-binary-coporducd-Decomposition-map-into-Fin-2 + ( f) + ( a)))) ∘e inv-equiv equiv-ev-pair)) distributive-Π-coproduct-binary-coproduct-Decomposition : diff --git a/src/foundation/retracts-of-types.lagda.md b/src/foundation/retracts-of-types.lagda.md index 1de9f4bdf06..0f959868dbb 100644 --- a/src/foundation/retracts-of-types.lagda.md +++ b/src/foundation/retracts-of-types.lagda.md @@ -79,21 +79,23 @@ module _ htpy-eq-retract : (R S : A retract-of B) → R ＝ S → htpy-retract R S htpy-eq-retract R .R refl = refl-htpy-retract R - is-torsorial-htpy-retract : - (R : A retract-of B) → is-torsorial (htpy-retract R) - is-torsorial-htpy-retract R = - is-torsorial-Eq-structure - ( is-torsorial-htpy (inclusion-retract R)) - ( inclusion-retract R , refl-htpy) - ( is-torsorial-Eq-structure - ( is-torsorial-htpy (map-retraction-retract R)) - ( map-retraction-retract R , refl-htpy) - ( is-torsorial-htpy (is-retraction-map-retraction-retract R))) - - is-equiv-htpy-eq-retract : - (R S : A retract-of B) → is-equiv (htpy-eq-retract R S) - is-equiv-htpy-eq-retract R = - fundamental-theorem-id (is-torsorial-htpy-retract R) (htpy-eq-retract R) + abstract + is-torsorial-htpy-retract : + (R : A retract-of B) → is-torsorial (htpy-retract R) + is-torsorial-htpy-retract R = + is-torsorial-Eq-structure + ( is-torsorial-htpy (inclusion-retract R)) + ( inclusion-retract R , refl-htpy) + ( is-torsorial-Eq-structure + ( is-torsorial-htpy (map-retraction-retract R)) + ( map-retraction-retract R , refl-htpy) + ( is-torsorial-htpy (is-retraction-map-retraction-retract R))) + + abstract + is-equiv-htpy-eq-retract : + (R S : A retract-of B) → is-equiv (htpy-eq-retract R S) + is-equiv-htpy-eq-retract R = + fundamental-theorem-id (is-torsorial-htpy-retract R) (htpy-eq-retract R) extensionality-retract : (R S : A retract-of B) → (R ＝ S) ≃ htpy-retract R S extensionality-retract R S = @@ -132,35 +134,40 @@ module _ equiv-eq-retracts : (R S : retracts l2 A) → R ＝ S → equiv-retracts R S equiv-eq-retracts R .R refl = refl-equiv-retracts R - is-torsorial-equiv-retracts : - (R : retracts l2 A) → is-torsorial (equiv-retracts R) - is-torsorial-equiv-retracts R = - is-torsorial-Eq-structure - ( is-torsorial-equiv (type-retracts R)) - ( type-retracts R , id-equiv) - ( is-contr-equiv - ( Σ (retract A (type-retracts R)) (htpy-retract (retract-retracts R))) - ( equiv-tot - ( λ S → - equiv-tot - ( λ I → - equiv-tot - ( λ J → - equiv-concat-htpy' - ( is-retraction-map-retraction-retracts R) - ( ap-concat-htpy - ( horizontal-concat-htpy J I) - ( right-unit-htpy ∙h - left-unit-law-left-whisker-comp - ( is-retraction-map-retraction-retract S))))))) - ( is-torsorial-htpy-retract (retract-retracts R))) - - is-equiv-equiv-eq-retracts : - (R S : retracts l2 A) → is-equiv (equiv-eq-retracts R S) - is-equiv-equiv-eq-retracts R = - fundamental-theorem-id (is-torsorial-equiv-retracts R) (equiv-eq-retracts R) - - extensionality-retracts : (R S : retracts l2 A) → (R ＝ S) ≃ equiv-retracts R S + abstract + is-torsorial-equiv-retracts : + (R : retracts l2 A) → is-torsorial (equiv-retracts {l2} R) + is-torsorial-equiv-retracts R = + is-torsorial-Eq-structure + ( is-torsorial-equiv (type-retracts R)) + ( type-retracts R , id-equiv) + ( is-contr-equiv + ( Σ (retract A (type-retracts R)) (htpy-retract (retract-retracts R))) + ( equiv-tot + ( λ S → + equiv-tot + ( λ I → + equiv-tot + ( λ J → + equiv-concat-htpy' + ( is-retraction-map-retraction-retracts R) + ( ap-concat-htpy + ( horizontal-concat-htpy J I) + ( right-unit-htpy ∙h + left-unit-law-left-whisker-comp + ( is-retraction-map-retraction-retract S))))))) + ( is-torsorial-htpy-retract (retract-retracts R))) + + abstract + is-equiv-equiv-eq-retracts : + (R S : retracts l2 A) → is-equiv (equiv-eq-retracts R S) + is-equiv-equiv-eq-retracts R = + fundamental-theorem-id + ( is-torsorial-equiv-retracts R) + ( equiv-eq-retracts R) + + extensionality-retracts : + (R S : retracts l2 A) → (R ＝ S) ≃ equiv-retracts R S extensionality-retracts R S = ( equiv-eq-retracts R S , is-equiv-equiv-eq-retracts R S) diff --git a/src/logic/propositionally-decidable-maps.lagda.md b/src/logic/propositionally-decidable-maps.lagda.md index 5d0eb7a334a..cdaf3133be5 100644 --- a/src/logic/propositionally-decidable-maps.lagda.md +++ b/src/logic/propositionally-decidable-maps.lagda.md @@ -9,13 +9,19 @@ module logic.propositionally-decidable-maps where ```agda open import elementary-number-theory.natural-numbers +open import foundation.complements-images open import foundation.coproduct-types open import foundation.decidable-dependent-pair-types open import foundation.decidable-maps open import foundation.dependent-pair-types open import foundation.double-negation-dense-equality-maps +open import foundation.equivalences +open import foundation.full-subtypes open import foundation.identity-types +open import foundation.images open import foundation.propositional-truncations +open import foundation.type-arithmetic-coproduct-types +open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation-core.fibers-of-maps @@ -24,6 +30,7 @@ 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.propositions open import logic.propositionally-decidable-types ``` @@ -185,3 +192,25 @@ module _ ( is-inhabited-or-empty-map-iterate-has-double-negation-dense-equality-map ( n)) ``` + +## The coproduct decomposition of the codomain of a propositionally decidable map + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + coproduct-decomposition-codomain-inhabited-or-empty-map : + (f'@(f , F) : inhabited-or-empty-map A B) → + B ≃ im f + nonim f + coproduct-decomposition-codomain-inhabited-or-empty-map (f , F) = + equivalence-reasoning + B + ≃ Σ B (λ y → is-inhabited-or-empty (fiber f y)) + by + inv-equiv-inclusion-is-full-subtype + ( is-inhabited-or-empty-Prop ∘ fiber f) + ( F) + ≃ im f + nonim f + by left-distributive-Σ-coproduct +```