Some closure properties of decidable maps and embeddings (#1184)

Formalizes a series of basic closure properties for decidable maps and
embeddings.

- Left cancellation for decidable maps and embeddings
- Triangle properties for decidable maps and embeddings
- Σ-closure properties for decidable maps and embeddings
- Base change closure for decidable maps and embeddings
- Retract closure for decidable maps and embeddings
- Product closure for decidable maps and embeddings
- Coproduct closure for decidable maps and embeddings
- Factor out lemmas about decidable maps from decidable embeddings file

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

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