Introduction to Homotopy Type Theory, Chapter 2

src/foundation/booleans.lagda.md

@@ -7,6 +7,7 @@ module foundation.booleans where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.contractible-types
 open import foundation.decidable-equality
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
@@ -342,3 +343,19 @@ abstract
     (b : bool) → ¬ (is-equiv (const bool b))
   is-not-equiv-const-bool b e = no-section-const-bool b (section-is-equiv e)
 ```
+
+### The type of booleans is not contractible
+
+```agda
+abstract
+  is-not-contractible-bool : ¬ (is-contr bool)
+  is-not-contractible-bool (b , eq) = no-section-const-bool b (id , eq)
+```
+
+### The type of booleans is not equivalent to the unit type
+
+```agda
+abstract
+  is-not-unit-bool : ¬ (bool ≃ unit)
+  is-not-unit-bool e = is-not-contractible-bool (is-contr-equiv-unit e)
+```

src/foundation/functoriality-cartesian-product-types.lagda.md

@@ -11,6 +11,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.morphisms-arrows
+open import foundation.sections
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
@@ -254,7 +255,7 @@ module _
   pr2 compute-fiber-map-product = is-equiv-map-compute-fiber-map-product
 ```
 
-### If `map-product f g : A × B → C × D` is an equivalence, then we have `D → is-equiv f` and `C → is-equiv g`
+### `map-product f g : A × B → C × D` is an equivalence if and only if we have `D → is-equiv f` and `C → is-equiv g`
 
 ```agda
 module _
@@ -291,6 +292,35 @@ module _
             ( map-compute-fiber-map-product f g (c , y))
             ( is-equiv-map-compute-fiber-map-product f g (c , y))
             ( is-contr-map-is-equiv is-equiv-fg (c , y))))
+
+  map-inv-map-product' : (D → is-equiv f) → (C → is-equiv g) → C × D → A × B
+  pr1 (map-inv-map-product' F G (c , d)) = map-inv-is-equiv (F d) c
+  pr2 (map-inv-map-product' F G (c , d)) = map-inv-is-equiv (G c) d
+
+  abstract
+    is-section-map-inv-map-product' :
+      (F : D → is-equiv f) (G : C → is-equiv g) →
+      is-section (map-product f g) (map-inv-map-product' F G)
+    is-section-map-inv-map-product' F G (c , d) =
+      eq-pair
+        ( is-section-map-inv-is-equiv (F d) c)
+        ( is-section-map-inv-is-equiv (G c) d)
+
+    is-retraction-map-inv-map-product' :
+      (F : D → is-equiv f) (G : C → is-equiv g) →
+      is-retraction (map-product f g) (map-inv-map-product' F G)
+    is-retraction-map-inv-map-product' F G (a , b) =
+      eq-pair
+        ( is-retraction-map-inv-is-equiv (F (g b)) a)
+        ( is-retraction-map-inv-is-equiv (G (f a)) b)
+
+  is-equiv-map-product' :
+    (D → is-equiv f) → (C → is-equiv g) → is-equiv (map-product f g)
+  is-equiv-map-product' F G =
+    is-equiv-is-invertible
+      ( map-inv-map-product' F G)
+      ( is-section-map-inv-map-product' F G)
+      ( is-retraction-map-inv-map-product' F G)
 ```
 
 ### The functorial action of products on arrows

src/foundation/unit-type.lagda.md

@@ -11,6 +11,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.diagonal-maps-of-types
 open import foundation.raising-universe-levels
+open import foundation.singleton-induction
 open import foundation.universe-levels
 
 open import foundation-core.constant-maps
@@ -107,6 +108,14 @@ abstract
     is-contr-equiv' unit (compute-raise l1 unit) is-contr-unit
 ```
 
+### The unit type satisfies singleton induction
+
+```agda
+abstract
+  is-singleton-unit : {l : Level} → is-singleton l unit star
+  is-singleton-unit B = ind-unit , λ b → refl
+```
+
 ### Any contractible type is equivalent to the unit type
 
 ```agda