diff --git a/src/foundation-core/empty-types.lagda.md b/src/foundation-core/empty-types.lagda.md
index 273b55df60..16c785826f 100644
--- a/src/foundation-core/empty-types.lagda.md
+++ b/src/foundation-core/empty-types.lagda.md
@@ -91,6 +91,16 @@ equiv-is-empty f g =
   ( pair f (is-equiv-is-empty f id))
 ```
 
+### Any map into an empty type is an embedding
+
+```agda
+abstract
+  is-emb-is-empty :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
+    is-empty B → is-emb f
+  is-emb-is-empty f H = is-emb-is-equiv (is-equiv-is-empty f H)
+```
+
 ### The empty type is a proposition
 
 ```agda
diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
index 4eda140f40..768597d72c 100644
--- a/src/foundation-core/functoriality-dependent-pair-types.lagda.md
+++ b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
@@ -298,10 +298,10 @@ module _
         ( is-section-fiber-fiber-map-Σ-map-base t)
         ( is-retraction-fiber-fiber-map-Σ-map-base t)
 
-  equiv-fiber-map-Σ-map-base-fiber :
+  compute-fiber-map-Σ-map-base :
     (t : Σ B C) → fiber f (pr1 t) ≃ fiber (map-Σ-map-base f C) t
-  pr1 (equiv-fiber-map-Σ-map-base-fiber t) = fiber-map-Σ-map-base-fiber t
-  pr2 (equiv-fiber-map-Σ-map-base-fiber t) =
+  pr1 (compute-fiber-map-Σ-map-base t) = fiber-map-Σ-map-base-fiber t
+  pr2 (compute-fiber-map-Σ-map-base t) =
     is-equiv-fiber-map-Σ-map-base-fiber t
 ```
 
@@ -318,7 +318,7 @@ module _
     is-contr-map-map-Σ-map-base is-contr-f (pair y z) =
       is-contr-equiv'
         ( fiber f y)
-        ( equiv-fiber-map-Σ-map-base-fiber f C (pair y z))
+        ( compute-fiber-map-Σ-map-base f C (pair y z))
         ( is-contr-f y)
 ```
 
diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md
index d18d5f6df8..fc452b45c0 100644
--- a/src/foundation/decidable-embeddings.lagda.md
+++ b/src/foundation/decidable-embeddings.lagda.md
@@ -8,45 +8,52 @@ module foundation.decidable-embeddings where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.cartesian-morphisms-arrows
 open import foundation.decidable-maps
-open import foundation.decidable-subtypes
+open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-coproduct-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositional-maps
-open import foundation.structured-type-duality
+open import foundation.retracts-of-maps
 open import foundation.subtype-identity-principle
 open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universal-property-equivalences
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
-open import foundation-core.contractible-maps
-open import foundation-core.contractible-types
 open import foundation-core.coproduct-types
-open import foundation-core.decidable-propositions
 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.propositions
 open import foundation-core.torsorial-type-families
-open import foundation-core.type-theoretic-principle-of-choice
 ```
 
 </details>
 
 ## Idea
 
-A map is said to be a decidable embedding if it is an embedding and its fibers
-are decidable types.
+A [map](foundation-core.function-types.md) is said to be a
+{{#concept "decidable embedding" Disambiguation="of types" Agda=is-decidable-emb}}
+if it is an [embedding](foundation-core.embeddings.md) and its
+[fibers](foundation-core.fibers-of-maps.md) are
+[decidable types](foundation.decidable-types.md).
+
+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}}.
 
 ## Definitions
 
@@ -55,18 +62,18 @@ are decidable types.
 ```agda
 is-decidable-emb :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (X → Y) → UU (l1 ⊔ l2)
-is-decidable-emb {Y = Y} f = is-emb f × is-decidable-map f
+is-decidable-emb f = is-emb f × is-decidable-map f
 
 abstract
   is-emb-is-decidable-emb :
     {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X → Y} →
     is-decidable-emb f → is-emb f
-  is-emb-is-decidable-emb H = pr1 H
+  is-emb-is-decidable-emb = pr1
 
 is-decidable-map-is-decidable-emb :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X → Y} →
   is-decidable-emb f → is-decidable-map f
-is-decidable-map-is-decidable-emb H = pr2 H
+is-decidable-map-is-decidable-emb = pr2
 ```
 
 ### Decidably propositional maps
@@ -164,52 +171,31 @@ module _
       is-decidable-emb f → is-decidable-prop-map f
     pr1 (is-decidable-prop-map-is-decidable-emb H y) =
       is-prop-map-is-decidable-emb H y
-    pr2 (is-decidable-prop-map-is-decidable-emb H y) = pr2 H y
-
-decidable-subtype-decidable-emb :
-  {l1 l2 : Level} {X : UU l1} {Y : UU l2} →
-  (X ↪ᵈ Y) → (decidable-subtype (l1 ⊔ l2) Y)
-pr1 (decidable-subtype-decidable-emb f y) = fiber (map-decidable-emb f) y
-pr2 (decidable-subtype-decidable-emb f y) =
-  is-decidable-prop-map-is-decidable-emb (pr2 f) y
-```
-
-### The type of all decidable embeddings into a type `A` is equivalent to the type of decidable subtypes of `A`
-
-```agda
-equiv-Fiber-Decidable-Prop :
-  (l : Level) {l1 : Level} (A : UU l1) →
-  Σ (UU (l1 ⊔ l)) (λ X → X ↪ᵈ A) ≃ (decidable-subtype (l1 ⊔ l) A)
-equiv-Fiber-Decidable-Prop l A =
-  ( equiv-Fiber-structure l is-decidable-prop A) ∘e
-  ( equiv-tot
-    ( λ X →
-      equiv-tot
-        ( λ f →
-          ( inv-distributive-Π-Σ) ∘e
-          ( equiv-product (equiv-is-prop-map-is-emb f) id-equiv))))
+    pr2 (is-decidable-prop-map-is-decidable-emb H y) =
+      is-decidable-map-is-decidable-emb H y
 ```
 
-### Any equivalence is a decidable embedding
+### Equivalences are decidable embeddings
 
 ```agda
 abstract
   is-decidable-emb-is-equiv :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
     is-equiv f → is-decidable-emb f
-  pr1 (is-decidable-emb-is-equiv H) = is-emb-is-equiv H
-  pr2 (is-decidable-emb-is-equiv H) x = inl (center (is-contr-map-is-equiv H x))
+  is-decidable-emb-is-equiv H =
+    ( is-emb-is-equiv H , is-decidable-map-is-equiv H)
+```
 
+### Identity maps are decidable embeddings
+
+```agda
 abstract
   is-decidable-emb-id :
     {l1 : Level} {A : UU l1} → is-decidable-emb (id {A = A})
-  pr1 (is-decidable-emb-id {l1} {A}) = is-emb-id
-  pr2 (is-decidable-emb-id {l1} {A}) x = inl (pair x refl)
+  is-decidable-emb-id = (is-emb-id , is-decidable-map-id)
 
-decidable-emb-id :
-  {l1 : Level} {A : UU l1} → A ↪ᵈ A
-pr1 (decidable-emb-id {l1} {A}) = id
-pr2 (decidable-emb-id {l1} {A}) = is-decidable-emb-id
+decidable-emb-id : {l1 : Level} {A : UU l1} → A ↪ᵈ A
+decidable-emb-id = (id , is-decidable-emb-id)
 ```
 
 ### Being a decidable embedding is a property
@@ -231,26 +217,60 @@ abstract
 ### Decidable embeddings are closed under composition
 
 ```agda
-abstract
+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-decidable-emb' :
+      is-decidable-emb g → is-decidable-map f → is-decidable-map (g ∘ f)
+    is-decidable-map-comp-is-decidable-emb' K H x =
+      rec-coproduct
+        ( λ u →
+          is-decidable-equiv
+            ( ( left-unit-law-Σ-is-contr
+                ( is-proof-irrelevant-is-prop
+                  ( is-prop-map-is-emb (is-emb-is-decidable-emb K) x) u)
+                ( u)) ∘e
+              ( compute-fiber-comp g f x))
+            ( H (pr1 u)))
+        ( λ α → inr (λ t → α (f (pr1 t) , pr2 t)))
+        ( is-decidable-map-is-decidable-emb K x)
+
+  is-decidable-map-comp-is-decidable-emb :
+    is-decidable-emb g → is-decidable-emb f → is-decidable-map (g ∘ f)
+  is-decidable-map-comp-is-decidable-emb K H =
+    is-decidable-map-comp-is-decidable-emb'
+      ( K)
+      ( is-decidable-map-is-decidable-emb H)
+
   is-decidable-emb-comp :
-    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
-    {g : B → C} {f : A → B} →
-    is-decidable-emb f → is-decidable-emb g → is-decidable-emb (g ∘ f)
-  pr1 (is-decidable-emb-comp {g = g} {f} H K) =
-    is-emb-comp _ _ (pr1 K) (pr1 H)
-  pr2 (is-decidable-emb-comp {g = g} {f} H K) x =
-    rec-coproduct
-      ( λ u →
-        is-decidable-equiv
-          ( compute-fiber-comp g f x)
-          ( is-decidable-equiv
-            ( left-unit-law-Σ-is-contr
-              ( is-proof-irrelevant-is-prop
-                ( is-prop-map-is-emb (is-emb-is-decidable-emb K) x) ( u))
-              ( u))
-            ( is-decidable-map-is-decidable-emb H (pr1 u))))
-      ( λ α → inr (λ t → α (f (pr1 t) , pr2 t)))
-      ( pr2 K x)
+    is-decidable-emb g → is-decidable-emb f → is-decidable-emb (g ∘ f)
+  is-decidable-emb-comp K H =
+    ( is-emb-comp _ _ (pr1 K) (pr1 H) ,
+      is-decidable-map-comp-is-decidable-emb K H)
+```
+
+### Left cancellation for decidable embeddings
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : A → B} {g : B → C}
+  where
+
+  is-decidable-emb-right-factor' :
+      is-decidable-emb (g ∘ f) → is-emb g → is-decidable-emb f
+  is-decidable-emb-right-factor' GH G =
+    ( is-emb-right-factor g f G (is-emb-is-decidable-emb GH) ,
+      is-decidable-map-right-factor'
+        ( is-decidable-map-is-decidable-emb GH)
+        ( is-injective-is-emb G))
+
+  is-decidable-emb-right-factor :
+      is-decidable-emb (g ∘ f) → is-decidable-emb g → is-decidable-emb f
+  is-decidable-emb-right-factor GH G =
+    is-decidable-emb-right-factor' GH (is-emb-is-decidable-emb G)
 ```
 
 ### Decidable embeddings are closed under homotopies
@@ -260,12 +280,46 @@ abstract
   is-decidable-emb-htpy :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} →
     f ~ g → is-decidable-emb g → is-decidable-emb f
-  pr1 (is-decidable-emb-htpy {f = f} {g} H K) =
-    is-emb-htpy H (is-emb-is-decidable-emb K)
-  pr2 (is-decidable-emb-htpy {f = f} {g} H K) b =
-    is-decidable-equiv
-      ( equiv-tot (λ a → equiv-concat (inv (H a)) b))
-      ( is-decidable-map-is-decidable-emb K b)
+  is-decidable-emb-htpy {f = f} {g} H K =
+    ( is-emb-htpy H (is-emb-is-decidable-emb K) ,
+      is-decidable-map-htpy H (is-decidable-map-is-decidable-emb K))
+```
+
+### In a commuting triangle of maps, if the top and right maps are decidable embeddings so is the left map
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  {top : A → B} {left : A → C} {right : B → C}
+  (H : left ~ right ∘ top)
+  where
+
+  is-decidable-emb-left-map-triangle :
+    is-decidable-emb top → is-decidable-emb right → is-decidable-emb left
+  is-decidable-emb-left-map-triangle T R =
+    is-decidable-emb-htpy H (is-decidable-emb-comp R T)
+```
+
+### In a commuting triangle of maps, if the left and right maps are decidable embeddings so is the top map
+
+In fact, the right map need only be an embedding.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  {top : A → B} {left : A → C} {right : B → C}
+  (H : left ~ right ∘ top)
+  where
+
+  is-decidable-emb-top-map-triangle' :
+    is-emb right → is-decidable-emb left → is-decidable-emb top
+  is-decidable-emb-top-map-triangle' R' L =
+    is-decidable-emb-right-factor' (is-decidable-emb-htpy (inv-htpy H) L) R'
+
+  is-decidable-emb-top-map-triangle :
+    is-decidable-emb right → is-decidable-emb left → is-decidable-emb top
+  is-decidable-emb-top-map-triangle R L =
+    is-decidable-emb-right-factor (is-decidable-emb-htpy (inv-htpy H) L) R
 ```
 
 ### Characterizing equality in the type of decidable embeddings
@@ -326,13 +380,13 @@ equiv-precomp-decidable-emb-equiv e C =
       equiv-iff-is-prop
         ( is-prop-is-decidable-emb g)
         ( is-prop-is-decidable-emb (g ∘ map-equiv e))
-        ( is-decidable-emb-comp (is-decidable-emb-is-equiv (pr2 e)))
+        ( λ H → is-decidable-emb-comp H (is-decidable-emb-is-equiv (pr2 e)))
         ( λ d →
           is-decidable-emb-htpy
             ( λ b → ap g (inv (is-section-map-inv-equiv e b)))
             ( is-decidable-emb-comp
-              ( is-decidable-emb-is-equiv (is-equiv-map-inv-equiv e))
-              ( d))))
+              ( d)
+              ( is-decidable-emb-is-equiv (is-equiv-map-inv-equiv e)))))
 ```
 
 ### Any map out of the empty type is a decidable embedding
@@ -341,13 +395,11 @@ equiv-precomp-decidable-emb-equiv e C =
 abstract
   is-decidable-emb-ex-falso :
     {l : Level} {X : UU l} → is-decidable-emb (ex-falso {l} {X})
-  pr1 (is-decidable-emb-ex-falso {l} {X}) = is-emb-ex-falso
-  pr2 (is-decidable-emb-ex-falso {l} {X}) x = inr pr1
+  is-decidable-emb-ex-falso = (is-emb-ex-falso , is-decidable-map-ex-falso)
 
 decidable-emb-ex-falso :
   {l : Level} {X : UU l} → empty ↪ᵈ X
-pr1 decidable-emb-ex-falso = ex-falso
-pr2 decidable-emb-ex-falso = is-decidable-emb-ex-falso
+decidable-emb-ex-falso = (ex-falso , is-decidable-emb-ex-falso)
 
 decidable-emb-is-empty :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-empty A → A ↪ᵈ B
@@ -357,7 +409,7 @@ decidable-emb-is-empty {A = A} f =
     ( decidable-emb-ex-falso)
 ```
 
-### The map on total spaces induced by a family of decidable embeddings is a decidable embeddings
+### The map on total spaces induced by a family of decidable embeddings is a decidable embedding
 
 ```agda
 module _
@@ -369,10 +421,143 @@ module _
     ((x : A) → is-decidable-emb (f x)) → is-decidable-emb (tot f)
   is-decidable-emb-tot H =
     ( is-emb-tot (λ x → is-emb-is-decidable-emb (H x)) ,
-      is-decidable-map-tot λ x → is-decidable-map-is-decidable-emb (H x))
+      is-decidable-map-tot (λ x → is-decidable-map-is-decidable-emb (H x)))
 
   decidable-emb-tot : ((x : A) → B x ↪ᵈ C x) → Σ A B ↪ᵈ Σ A C
-  pr1 (decidable-emb-tot f) = tot (λ x → map-decidable-emb (f x))
-  pr2 (decidable-emb-tot f) =
-    is-decidable-emb-tot (λ x → is-decidable-emb-map-decidable-emb (f x))
+  decidable-emb-tot f =
+    ( tot (λ x → map-decidable-emb (f x)) ,
+      is-decidable-emb-tot (λ x → is-decidable-emb-map-decidable-emb (f x)))
+```
+
+### The map on total spaces induced by a decidable embedding on the base is a decidable embedding
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : B → UU l3)
+  where
+
+  is-decidable-emb-map-Σ-map-base :
+    {f : A → B} → is-decidable-emb f → is-decidable-emb (map-Σ-map-base f C)
+  is-decidable-emb-map-Σ-map-base {f} H =
+    ( is-emb-map-Σ-map-base C (is-emb-is-decidable-emb H) ,
+      is-decidable-map-Σ-map-base C (is-decidable-map-is-decidable-emb H))
+
+  decidable-emb-map-Σ-map-base :
+    (f : A ↪ᵈ B) → Σ A (C ∘ map-decidable-emb f) ↪ᵈ Σ B C
+  decidable-emb-map-Σ-map-base f =
+    ( map-Σ-map-base (map-decidable-emb f) C ,
+      is-decidable-emb-map-Σ-map-base ((is-decidable-emb-map-decidable-emb f)))
+```
+
+### The functoriality of dependent pair types preserves decidable embeddings
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} (D : B → UU l4)
+  where
+
+  is-decidable-emb-map-Σ :
+    {f : A → B} {g : (x : A) → C x → D (f x)} →
+    is-decidable-emb f →
+    ((x : A) → is-decidable-emb (g x)) →
+    is-decidable-emb (map-Σ D f g)
+  is-decidable-emb-map-Σ {f} {g} F G =
+    is-decidable-emb-left-map-triangle
+      ( triangle-map-Σ D f g)
+      ( is-decidable-emb-tot G)
+      ( is-decidable-emb-map-Σ-map-base D F)
+
+  decidable-emb-Σ :
+    (f : A ↪ᵈ B) →
+    ((x : A) → C x ↪ᵈ D (map-decidable-emb f x)) →
+    Σ A C ↪ᵈ Σ B D
+  decidable-emb-Σ f g =
+    ( ( map-Σ D (map-decidable-emb f) (λ x → map-decidable-emb (g x))) ,
+      ( is-decidable-emb-map-Σ
+        ( is-decidable-emb-map-decidable-emb f)
+        ( λ x → is-decidable-emb-map-decidable-emb (g x))))
+```
+
+### Products of decidable embeddings are decidable embeddings
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  where
+
+  is-decidable-emb-map-product :
+    {f : A → B} {g : C → D} →
+    is-decidable-emb f → is-decidable-emb g → is-decidable-emb (map-product f g)
+  is-decidable-emb-map-product (eF , dF) (eG , dG) =
+    ( is-emb-map-product eF eG , is-decidable-map-product dF dG)
+
+  decidable-emb-product :
+    A ↪ᵈ B → C ↪ᵈ D → A × C ↪ᵈ B × D
+  decidable-emb-product (f , F) (g , G) =
+    (map-product f g , is-decidable-emb-map-product F G)
+```
+
+### 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}
+    {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+    {f : A → B} {g : X → Y} →
+    is-decidable-emb f →
+    is-decidable-emb g →
+    is-decidable-emb (map-coproduct f g)
+  is-decidable-emb-map-coproduct {f = f} {g} (eF , dF) (eG , dG) =
+    ( is-emb-map-coproduct eF eG , is-decidable-map-coproduct dF dG)
+```
+
+### Decidable embeddings are closed under base change
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  {f : A → B} {g : C → D}
+  where
+
+  is-decidable-prop-map-base-change :
+    cartesian-hom-arrow g f → is-decidable-prop-map f → is-decidable-prop-map g
+  is-decidable-prop-map-base-change α F d =
+    is-decidable-prop-equiv
+      ( equiv-fibers-cartesian-hom-arrow g f α d)
+      ( F (map-codomain-cartesian-hom-arrow g f α d))
+
+  is-decidable-emb-base-change :
+    cartesian-hom-arrow g f → is-decidable-emb f → is-decidable-emb g
+  is-decidable-emb-base-change α F =
+    is-decidable-emb-is-decidable-prop-map
+      ( is-decidable-prop-map-base-change α
+        ( is-decidable-prop-map-is-decidable-emb F))
+```
+
+### Decidable embeddings are closed under retracts of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  {f : A → B} {g : X → Y}
+  where
+
+  is-decidable-prop-map-retract-map :
+    f retract-of-map g → is-decidable-prop-map g → is-decidable-prop-map f
+  is-decidable-prop-map-retract-map R G x =
+    is-decidable-prop-retract-of
+      ( retract-fiber-retract-map f g R x)
+      ( G (map-codomain-inclusion-retract-map f g R x))
+
+  is-decidable-emb-retract-map :
+    f retract-of-map g → is-decidable-emb g → is-decidable-emb f
+  is-decidable-emb-retract-map R G =
+    is-decidable-emb-is-decidable-prop-map
+      ( is-decidable-prop-map-retract-map R
+        ( is-decidable-prop-map-is-decidable-emb G))
 ```
diff --git a/src/foundation/decidable-maps.lagda.md b/src/foundation/decidable-maps.lagda.md
index 22aa4cb08d..893f11da73 100644
--- a/src/foundation/decidable-maps.lagda.md
+++ b/src/foundation/decidable-maps.lagda.md
@@ -8,16 +8,26 @@ module foundation.decidable-maps where
 
 ```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-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.retracts-of-maps
 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.identity-types
+open import foundation-core.homotopies
+open import foundation-core.injective-maps
 open import foundation-core.retractions
 ```
 
@@ -25,7 +35,10 @@ open import foundation-core.retractions
 
 ## Definition
 
-A map is said to be decidable if its fibers are decidable types.
+A [map](foundation-core.function-types.md) is said to be
+{{#concept "decidable" Disambiguation="map of types" Agda=is-decidable-map}} if
+its [fibers](foundation-core.fibers-of-maps.md) are
+[decidable types](foundation.decidable-types.md).
 
 ```agda
 module _
@@ -36,20 +49,81 @@ module _
   is-decidable-map f = (y : B) → is-decidable (fiber f y)
 ```
 
+## Properties
+
+### Decidable maps are closed under homotopy
+
+```agda
+abstract
+  is-decidable-map-htpy :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} →
+    f ~ g → is-decidable-map g → is-decidable-map f
+  is-decidable-map-htpy H K b =
+    is-decidable-equiv
+      ( equiv-tot (λ a → equiv-concat (inv (H a)) b))
+      ( K b)
+```
+
+### Left cancellation for decidable maps
+
+If a composite `g ∘ f` is decidable and the left factor `g` is injective, then
+the right factor `f` is decidable.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {f : A → B} {g : B → C}
+  where
+
+  abstract
+    is-decidable-map-right-factor' :
+      is-decidable-map (g ∘ f) → is-injective g → is-decidable-map f
+    is-decidable-map-right-factor' GF G y with (GF (g y))
+    ... | inl q = inl (pr1 q , G (pr2 q))
+    ... | inr q = inr (λ x → q ((pr1 x) , ap g (pr2 x)))
+```
+
+### Retracts into types with decidable equality are decidable
+
 ```agda
 is-decidable-map-retraction :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} → has-decidable-equality B →
   (i : A → B) → retraction i → is-decidable-map i
-is-decidable-map-retraction d i (pair r R) b =
+is-decidable-map-retraction d i (r , R) b =
   is-decidable-iff
-    ( λ (p : i (r b) ＝ b) → pair (r b) p)
+    ( λ (p : i (r b) ＝ b) → r b , p)
     ( λ t → ap (i ∘ r) (inv (pr2 t)) ∙ (ap i (R (pr1 t)) ∙ pr2 t))
     ( d (i (r b)) b)
 ```
 
-## Properties
+### Any map out of the empty type is decidable
 
-### The map on total spaces induced by a family of decidable embeddings is a decidable embeddings
+```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
 module _
@@ -60,8 +134,84 @@ module _
     {f : (x : A) → B x → C x} →
     ((x : A) → is-decidable-map (f x)) → is-decidable-map (tot f)
   is-decidable-map-tot {f} H x =
-    is-decidable-is-equiv
-      ( is-equiv-map-equiv
-        ( compute-fiber-tot f x))
-      ( H (pr1 x) (pr2 x))
+    is-decidable-equiv (compute-fiber-tot f x) (H (pr1 x) (pr2 x))
+```
+
+### The map on total spaces induced by a decidable map on the base is decidable
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : B → UU l3)
+  where
+
+  is-decidable-map-Σ-map-base :
+    {f : A → B} → is-decidable-map f → is-decidable-map (map-Σ-map-base f C)
+  is-decidable-map-Σ-map-base {f} H x =
+    is-decidable-equiv' (compute-fiber-map-Σ-map-base f C x) (H (pr1 x))
+```
+
+### Products of decidable maps are decidable
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  where
+
+  is-decidable-map-product :
+    {f : A → B} {g : C → D} →
+    is-decidable-map f → is-decidable-map g → is-decidable-map (map-product f g)
+  is-decidable-map-product {f} {g} F G x =
+    is-decidable-equiv
+      ( compute-fiber-map-product f g x)
+      ( is-decidable-product (F (pr1 x)) (G (pr2 x)))
+```
+
+### Coproducts of decidable maps are decidable
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  where
+
+  is-decidable-map-coproduct :
+    {f : A → B} {g : C → D} →
+    is-decidable-map f →
+    is-decidable-map g →
+    is-decidable-map (map-coproduct f g)
+  is-decidable-map-coproduct {f} {g} F G (inl x) =
+    is-decidable-equiv' (compute-fiber-inl-map-coproduct f g x) (F x)
+  is-decidable-map-coproduct {f} {g} F G (inr y) =
+    is-decidable-equiv' (compute-fiber-inr-map-coproduct f g y) (G y)
+```
+
+### Decidable maps are closed under base change
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  {f : A → B} {g : C → D}
+  where
+
+  is-decidable-map-base-change :
+    cartesian-hom-arrow g f → is-decidable-map f → is-decidable-map g
+  is-decidable-map-base-change α F d =
+    is-decidable-equiv
+      ( equiv-fibers-cartesian-hom-arrow g f α d)
+      ( F (map-codomain-cartesian-hom-arrow g f α d))
+```
+
+### Decidable maps are closed under retracts of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  {f : A → B} {g : X → Y}
+  where
+
+  is-decidable-retract-map :
+    f retract-of-map g → is-decidable-map g → is-decidable-map f
+  is-decidable-retract-map R G x =
+    is-decidable-retract-of
+      ( retract-fiber-retract-map f g R x)
+      ( G (map-codomain-inclusion-retract-map f g R x))
 ```
diff --git a/src/foundation/decidable-propositions.lagda.md b/src/foundation/decidable-propositions.lagda.md
index 877d8c5626..e4c26aa083 100644
--- a/src/foundation/decidable-propositions.lagda.md
+++ b/src/foundation/decidable-propositions.lagda.md
@@ -19,6 +19,7 @@ open import foundation.equivalences
 open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositional-extensionality
+open import foundation.propositions
 open import foundation.raising-universe-levels
 open import foundation.type-arithmetic-coproduct-types
 open import foundation.type-arithmetic-dependent-pair-types
@@ -30,7 +31,7 @@ open import foundation-core.coproduct-types
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
-open import foundation-core.propositions
+open import foundation-core.retracts-of-types
 open import foundation-core.sets
 open import foundation-core.small-types
 open import foundation-core.subtypes
@@ -44,7 +45,8 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-A decidable proposition is a proposition that has a decidable underlying type.
+A **decidable proposition** is a [proposition](foundation-core.propositions.md)
+that has a [decidable](foundation.decidable-types.md) underlying type.
 
 ## Properties
 
@@ -265,3 +267,34 @@ pr1 (pr2 (neg-Decidable-Prop P)) = is-prop-neg
 pr2 (pr2 (neg-Decidable-Prop P)) =
   is-decidable-neg (is-decidable-Decidable-Prop P)
 ```
+
+### Decidable propositions are closed under retracts
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-decidable-prop-retract-of :
+    A retract-of B → is-decidable-prop B → is-decidable-prop A
+  is-decidable-prop-retract-of R (p , d) =
+    ( is-prop-retract-of R p , is-decidable-retract-of R d)
+```
+
+### Decidable propositions are closed under equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  is-decidable-prop-equiv :
+    A ≃ B → is-decidable-prop B → is-decidable-prop A
+  is-decidable-prop-equiv e =
+    is-decidable-prop-retract-of (retract-equiv e)
+
+  is-decidable-prop-equiv' :
+    B ≃ A → is-decidable-prop B → is-decidable-prop A
+  is-decidable-prop-equiv' e =
+    is-decidable-prop-retract-of (retract-inv-equiv e)
+```
diff --git a/src/foundation/decidable-subtypes.lagda.md b/src/foundation/decidable-subtypes.lagda.md
index b8c8bce746..9a162ba9f7 100644
--- a/src/foundation/decidable-subtypes.lagda.md
+++ b/src/foundation/decidable-subtypes.lagda.md
@@ -9,18 +9,26 @@ module foundation.decidable-subtypes where
 ```agda
 open import foundation.1-types
 open import foundation.coproduct-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.equality-dependent-function-types
+open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
 open import foundation.logical-equivalences
+open import foundation.propositional-maps
 open import foundation.sets
+open import foundation.structured-type-duality
 open import foundation.subtypes
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.universe-levels
 
 open import foundation-core.embeddings
 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
@@ -34,8 +42,10 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-A decidable subtype of a type consists of a family of decidable propositions
-over it.
+A
+{{#concept "decidable subtype" Disambiguation="of a type" Agda=is-decidable-subtype Agda=decidable-subtype}}
+of a type consists of a family of
+[decidable propositions](foundation-core.decidable-propositions.md) over it.
 
 ## Definitions
 
@@ -100,6 +110,13 @@ module _
   is-emb-inclusion-decidable-subtype =
     is-emb-inclusion-subtype (subtype-decidable-subtype P)
 
+  is-decidable-map-inclusion-decidable-subtype :
+    is-decidable-map inclusion-decidable-subtype
+  is-decidable-map-inclusion-decidable-subtype x =
+    is-decidable-equiv
+      ( equiv-fiber-pr1 (type-Decidable-Prop ∘ P) x)
+      ( is-decidable-Decidable-Prop (P x))
+
   is-injective-inclusion-decidable-subtype :
     is-injective inclusion-decidable-subtype
   is-injective-inclusion-decidable-subtype =
@@ -107,6 +124,43 @@ module _
 
   emb-decidable-subtype : type-decidable-subtype ↪ A
   emb-decidable-subtype = emb-subtype (subtype-decidable-subtype P)
+
+  is-decidable-emb-inclusion-decidable-subtype :
+    is-decidable-emb inclusion-decidable-subtype
+  is-decidable-emb-inclusion-decidable-subtype =
+    ( is-emb-inclusion-decidable-subtype ,
+      is-decidable-map-inclusion-decidable-subtype)
+
+  decidable-emb-decidable-subtype : type-decidable-subtype ↪ᵈ A
+  decidable-emb-decidable-subtype =
+    ( inclusion-decidable-subtype ,
+      is-decidable-emb-inclusion-decidable-subtype)
+```
+
+### The decidable subtype associated to a decidable embedding
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X ↪ᵈ Y)
+  where
+
+  decidable-subtype-decidable-emb : decidable-subtype (l1 ⊔ l2) Y
+  pr1 (decidable-subtype-decidable-emb y) =
+    fiber (map-decidable-emb f) y
+  pr2 (decidable-subtype-decidable-emb y) =
+    is-decidable-prop-map-is-decidable-emb
+      ( is-decidable-emb-map-decidable-emb f)
+      ( y)
+
+  compute-type-decidable-type-decidable-emb :
+    type-decidable-subtype decidable-subtype-decidable-emb ≃ X
+  compute-type-decidable-type-decidable-emb =
+    equiv-total-fiber (map-decidable-emb f)
+
+  inv-compute-type-decidable-type-decidable-emb :
+    X ≃ type-decidable-subtype decidable-subtype-decidable-emb
+  inv-compute-type-decidable-type-decidable-emb =
+    inv-equiv-total-fiber (map-decidable-emb f)
 ```
 
 ## Examples
@@ -223,7 +277,7 @@ set-decidable-subset A P = set-subset A (subtype-decidable-subtype P)
 ```agda
 is-set-decidable-subtype :
   {l1 l2 : Level} {X : UU l1} → is-set (decidable-subtype l2 X)
-is-set-decidable-subtype {l1} {l2} {X} =
+is-set-decidable-subtype =
   is-set-function-type is-set-Decidable-Prop
 ```
 
@@ -265,3 +319,19 @@ module _
     map-equiv (extensionality-decidable-subtype P) refl ＝ (λ x → pair id id)
   refl-extensionality-decidable-subtype = refl
 ```
+
+### The type of decidable subtypes of `A` is equivalent to the type of all decidable embeddings into a type `A`
+
+```agda
+equiv-Fiber-Decidable-Prop :
+  (l : Level) {l1 : Level} (A : UU l1) →
+  Σ (UU (l1 ⊔ l)) (λ X → X ↪ᵈ A) ≃ (decidable-subtype (l1 ⊔ l) A)
+equiv-Fiber-Decidable-Prop l A =
+  ( equiv-Fiber-structure l is-decidable-prop A) ∘e
+  ( equiv-tot
+    ( λ X →
+      equiv-tot
+        ( λ f →
+          ( inv-distributive-Π-Σ) ∘e
+          ( equiv-product-left (equiv-is-prop-map-is-emb f)))))
+```
diff --git a/src/foundation/decidable-types.lagda.md b/src/foundation/decidable-types.lagda.md
index 3bed2fac28..51dffda53c 100644
--- a/src/foundation/decidable-types.lagda.md
+++ b/src/foundation/decidable-types.lagda.md
@@ -140,8 +140,7 @@ is-decidable-function-type :
   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 (inr f) (inl b) = inl (ex-falso ∘ f)
-is-decidable-function-type (inr f) (inr g) = inl (ex-falso ∘ f)
+is-decidable-function-type (inr f) _ = inl (ex-falso ∘ f)
 
 is-decidable-function-type' :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} →
@@ -152,6 +151,36 @@ is-decidable-function-type' (inl a) d with d a
 is-decidable-function-type' (inr na) d = inl (ex-falso ∘ na)
 ```
 
+### Dependent sums of a uniformly decidable family of types over a decidable base is decidable
+
+```agda
+is-decidable-Σ-uniformly-decidable-family :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-decidable A → (((a : A) → B a) + ((a : A) → ¬ B a)) → is-decidable (Σ A B)
+is-decidable-Σ-uniformly-decidable-family (inl a) (inl b) =
+  inl (a , b a)
+is-decidable-Σ-uniformly-decidable-family (inl a) (inr b) =
+  inr (λ x → b (pr1 x) (pr2 x))
+is-decidable-Σ-uniformly-decidable-family (inr a) _ =
+  inr (λ x → a (pr1 x))
+```
+
+### Dependent products of uniformly decidable families over decidable bases are decidable
+
+```agda
+is-decidable-Π-uniformly-decidable-family :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-decidable A →
+  (((a : A) → B a) + ((a : A) → ¬ (B a))) →
+  is-decidable ((a : A) → (B a))
+is-decidable-Π-uniformly-decidable-family (inl a) (inl b) =
+  inl b
+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)
+```
+
 ### The negation of a decidable type is decidable
 
 ```agda
@@ -160,7 +189,7 @@ is-decidable-neg :
 is-decidable-neg d = is-decidable-function-type d is-decidable-empty
 ```
 
-### Decidable types are closed under coinhabited types; retracts, and equivalences
+### Decidable types are closed under coinhabited types
 
 ```agda
 module _
@@ -171,7 +200,11 @@ module _
     (A → B) → (B → A) → is-decidable A → is-decidable B
   is-decidable-iff f g (inl a) = inl (f a)
   is-decidable-iff f g (inr na) = inr (λ b → na (g b))
+```
 
+### Decidable types are closed under retracts
+
+```agda
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}
   where
@@ -180,7 +213,11 @@ module _
     A retract-of B → is-decidable B → is-decidable A
   is-decidable-retract-of (pair i (pair r H)) (inl b) = inl (r b)
   is-decidable-retract-of (pair i (pair r H)) (inr f) = inr (f ∘ i)
+```
+
+### Decidable types are closed under equivalences
 
+```agda
   is-decidable-is-equiv :
     {f : A → B} → is-equiv f → is-decidable B → is-decidable A
   is-decidable-is-equiv {f} (pair (pair g G) (pair h H)) =
@@ -259,7 +296,7 @@ is-fixed-point-is-decidable-is-inhabited {l} {X} t =
   right-unit-law-coproduct-is-empty X (¬ X) (is-nonempty-is-inhabited t)
 ```
 
-### Raising types converves decidability
+### Raising universe level conserves decidability
 
 ```agda
 module _
@@ -267,6 +304,5 @@ module _
   where
 
   is-decidable-raise : is-decidable A → is-decidable (raise l A)
-  is-decidable-raise (inl p) = inl (map-raise p)
-  is-decidable-raise (inr np) = inr (λ p' → np (map-inv-raise p'))
+  is-decidable-raise = is-decidable-equiv' (compute-raise l A)
 ```
diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md
index c58bb50059..6631d6bead 100644
--- a/src/foundation/embeddings.lagda.md
+++ b/src/foundation/embeddings.lagda.md
@@ -309,8 +309,8 @@ module _
   emb-product f g = emb-Σ (λ _ → D) f (λ _ → g)
 
   is-emb-map-product :
-    (f : A → C) (g : B → D) → is-emb f → is-emb g → (is-emb (map-product f g))
-  is-emb-map-product f g is-emb-f is-emb-g =
+    {f : A → C} {g : B → D} → is-emb f → is-emb g → (is-emb (map-product f g))
+  is-emb-map-product {f} {g} is-emb-f is-emb-g =
     is-emb-map-emb (emb-product (f , is-emb-f) (g , is-emb-g))
 ```
 
diff --git a/src/foundation/equality-coproduct-types.lagda.md b/src/foundation/equality-coproduct-types.lagda.md
index f8b1319439..93dae7409e 100644
--- a/src/foundation/equality-coproduct-types.lagda.md
+++ b/src/foundation/equality-coproduct-types.lagda.md
@@ -140,6 +140,11 @@ module _
     map-compute-eq-coproduct-inl-inl : Id {A = A + B} (inl x) (inl y) → x ＝ y
     map-compute-eq-coproduct-inl-inl = map-equiv compute-eq-coproduct-inl-inl
 
+    is-equiv-map-compute-eq-coproduct-inl-inl :
+      is-equiv map-compute-eq-coproduct-inl-inl
+    is-equiv-map-compute-eq-coproduct-inl-inl =
+      is-equiv-map-equiv compute-eq-coproduct-inl-inl
+
   module _
     (x : A) (y : B)
     where
@@ -220,6 +225,11 @@ module _
 
     map-compute-eq-coproduct-inr-inr : Id {A = A + B} (inr x) (inr y) → x ＝ y
     map-compute-eq-coproduct-inr-inr = map-equiv compute-eq-coproduct-inr-inr
+
+    is-equiv-map-compute-eq-coproduct-inr-inr :
+      is-equiv map-compute-eq-coproduct-inr-inr
+    is-equiv-map-compute-eq-coproduct-inr-inr =
+      is-equiv-map-equiv compute-eq-coproduct-inr-inr
 ```
 
 ### The left and right inclusions into a coproduct are embeddings
diff --git a/src/foundation/functoriality-coproduct-types.lagda.md b/src/foundation/functoriality-coproduct-types.lagda.md
index 77a44581e0..349a065fa5 100644
--- a/src/foundation/functoriality-coproduct-types.lagda.md
+++ b/src/foundation/functoriality-coproduct-types.lagda.md
@@ -28,6 +28,7 @@ open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.contractible-types
+open import foundation-core.embeddings
 open import foundation-core.empty-types
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -149,6 +150,12 @@ module _
         ( is-section-fiber-fiber-map-coproduct-inl x)
         ( is-retraction-fiber-fiber-map-coproduct-inl x)
 
+  compute-fiber-inl-map-coproduct :
+    (x : A) → fiber f x ≃ fiber (map-coproduct f g) (inl x)
+  compute-fiber-inl-map-coproduct x =
+    ( fiber-map-coproduct-inl-fiber x ,
+      is-equiv-fiber-map-coproduct-inl-fiber x)
+
   fiber-map-coproduct-inr-fiber :
     (y : B) → fiber g y → fiber (map-coproduct f g) (inr y)
   pr1 (fiber-map-coproduct-inr-fiber y (b' , p)) = inr b'
@@ -184,6 +191,12 @@ module _
         ( fiber-fiber-map-coproduct-inr y)
         ( is-section-fiber-fiber-map-coproduct-inr y)
         ( is-retraction-fiber-fiber-map-coproduct-inr y)
+
+  compute-fiber-inr-map-coproduct :
+    (y : B) → fiber g y ≃ fiber (map-coproduct f g) (inr y)
+  compute-fiber-inr-map-coproduct y =
+    ( fiber-map-coproduct-inr-fiber y ,
+      is-equiv-fiber-map-coproduct-inr-fiber y)
 ```
 
 ### Functoriality of coproducts preserves equivalences
@@ -233,7 +246,50 @@ module _
     is-equiv-map-coproduct (is-equiv-map-equiv e) (is-equiv-map-equiv e')
 ```
 
-### Functoriality of coproducts preserves being surjective
+### Functoriality of coproducts preserves embeddings
+
+```agda
+module _
+  {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'}
+  where
+
+abstract
+  is-emb-map-coproduct :
+    {l1 l2 l3 l4 : Level}
+    {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+    {f : A → B} {g : X → Y} →
+    is-emb f → is-emb g → is-emb (map-coproduct f g)
+  is-emb-map-coproduct {f = f} {g} F G (inl x) (inl y) =
+    is-equiv-left-is-equiv-right-square
+      ( ap (map-coproduct f g))
+      ( ap f)
+      ( map-compute-eq-coproduct-inl-inl x y)
+      ( map-compute-eq-coproduct-inl-inl (f x) (f y))
+      ( λ where refl → refl)
+      ( is-equiv-map-compute-eq-coproduct-inl-inl x y)
+      ( is-equiv-map-compute-eq-coproduct-inl-inl (f x) (f y))
+      ( F x y)
+  is-emb-map-coproduct {f = f} {g} F G (inl x) (inr y) =
+    is-equiv-is-empty
+      ( ap (map-coproduct f g))
+      ( is-empty-eq-coproduct-inl-inr (f x) (g y))
+  is-emb-map-coproduct {f = f} {g} F G (inr x) (inl y) =
+    is-equiv-is-empty
+      ( ap (map-coproduct f g))
+      ( is-empty-eq-coproduct-inr-inl (g x) (f y))
+  is-emb-map-coproduct {f = f} {g} F G (inr x) (inr y) =
+    is-equiv-left-is-equiv-right-square
+      ( ap (map-coproduct f g))
+      ( ap g)
+      ( map-compute-eq-coproduct-inr-inr x y)
+      ( map-compute-eq-coproduct-inr-inr (g x) (g y))
+      ( λ where refl → refl)
+      ( is-equiv-map-compute-eq-coproduct-inr-inr x y)
+      ( is-equiv-map-compute-eq-coproduct-inr-inr (g x) (g y))
+      ( G x y)
+```
+
+### Functoriality of coproducts preserves surjections
 
 ```agda
 module _
diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md
index 86a2912fa7..beffdd38f2 100644
--- a/src/foundation/functoriality-dependent-pair-types.lagda.md
+++ b/src/foundation/functoriality-dependent-pair-types.lagda.md
@@ -187,7 +187,7 @@ module _
     is-trunc-map-map-Σ-map-base k {f} C H y =
       is-trunc-equiv' k
         ( fiber f (pr1 y))
-        ( equiv-fiber-map-Σ-map-base-fiber f C y)
+        ( compute-fiber-map-Σ-map-base f C y)
         ( H (pr1 y))
 
   abstract
diff --git a/src/foundation/propositions.lagda.md b/src/foundation/propositions.lagda.md
index 5a9092e007..cc36431139 100644
--- a/src/foundation/propositions.lagda.md
+++ b/src/foundation/propositions.lagda.md
@@ -42,7 +42,7 @@ pr2 (truncated-type-Prop k P) = is-trunc-is-prop k (is-prop-type-Prop P)
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} (B : UU l2)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
   where
 
   is-prop-retract-of : A retract-of B → is-prop B → is-prop A
diff --git a/src/univalent-combinatorics/binomial-types.lagda.md b/src/univalent-combinatorics/binomial-types.lagda.md
index 67c3f5a8a2..e08d5d666f 100644
--- a/src/univalent-combinatorics/binomial-types.lagda.md
+++ b/src/univalent-combinatorics/binomial-types.lagda.md
@@ -17,6 +17,7 @@ open import foundation.contractible-types
 open import foundation.coproduct-types
 open import foundation.decidable-embeddings
 open import foundation.decidable-propositions
+open import foundation.decidable-subtypes
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.empty-types
@@ -57,9 +58,10 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The binomial types are a categorification of the binomial coefficients. The
-binomial type `(A choose B)` is the type of decidable embeddings from types
-merely equal to `B` into `A`.
+The {{#concept "binomial types" Agda=binomial-type}} are a categorification of
+the binomial coefficients. The binomial type `(A choose B)` is the type of
+[decidable embeddings](foundation.decidable-embeddings.md) from types
+[merely equivalent](foundation.mere-equivalences.md) to `B` into `A`.
 
 ## Definitions
 
diff --git a/src/univalent-combinatorics/embeddings.lagda.md b/src/univalent-combinatorics/embeddings.lagda.md
index 5ec8168e06..e9776b2416 100644
--- a/src/univalent-combinatorics/embeddings.lagda.md
+++ b/src/univalent-combinatorics/embeddings.lagda.md
@@ -1,4 +1,4 @@
-# Injective maps
+# Embeddings
 
 ```agda
 module univalent-combinatorics.embeddings where
@@ -37,6 +37,8 @@ Embeddings in the presence of finite types enjoy further properties.
 
 ## Properties
 
+### Between finite types being an embedding is decidable
+
 ```agda
 is-decidable-is-emb-is-finite :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
@@ -48,7 +50,7 @@ is-decidable-is-emb-is-finite f HA HB =
     ( is-decidable-is-injective-is-finite f HA HB)
 ```
 
-### If `A` can be count, then `trunc-Prop A ↪ᵈ A`
+### If `A` can be counted, then `trunc-Prop A ↪ᵈ A`
 
 ```agda
 decidable-emb-trunc-Prop-count :