some remaining exercises in Chapter 2

contrib/HoTTBookExercises.v

@@ -680,17 +680,19 @@ Definition Book_2_13 := @HoTT.Types.Bool.equiv_bool_aut_bool.
 (* ================================================== ex:equality-reflection *)
 (** Exercise 2.14 *)
 
-
+(** Assuming the equality reflection rule, given any [q : x = y], [x] and [y] are definitionally equal, so [q] and [refl_x] have the same type [x = x]. We can form the type [forall x y, forall q, q = refl_x]. A path induction produces an element r, with [(r x x p) : p = refl_x], which is also definitional by the equality reflection rule. *)
 
 (* ================================================== ex:strengthen-transport-is-ap *)
 (** Exercise 2.15 *)
 
-
+Definition Book_2_15 {A} (B : A -> Type) {x y : A} (p : x = y)
+  : transport B p = HoTT.Types.Universe.equiv_path _ _ (ap B p)
+  := match p with 1 => 1 end.
 
 (* ================================================== ex:strong-from-weak-funext *)
 (** Exercise 2.16 *)
 
-
+Definition Book_2_16 := @HoTT.Metatheory.FunextVarieties.NaiveFunext_implies_Funext.
 
 (* ================================================== ex:equiv-functor-types *)
 (** Exercise 2.17 *)
@@ -700,7 +702,16 @@ Definition Book_2_13 := @HoTT.Types.Bool.equiv_bool_aut_bool.
 (* ================================================== ex:dep-htpy-natural *)
 (** Exercise 2.18 *)
 
+(** This exercise is solved in the library as HoTT.Basics.PathGroupoids.apD_homotopic *)
 
+Definition Book_2_18 {A : Type} {B : A -> Type} {f g : forall x, B x}
+  (H : forall x, f x = g x) {x y : A} (p : x = y)
+  : apD f p @ H y = ap (transport B p) (H x) @ apD g p.
+Proof.
+  destruct p.
+  unfold transport.
+  exact (concat_1p _ @ (ap_idmap _)^ @ (concat_p1 _)^).
+Defined.
 
 (* ================================================== ex:equiv-functor-set *)
 (** Exercise 3.1 *)