add apD_natural to PathGroupoids.v

contrib/HoTTBookExercises.v

@@ -702,16 +702,7 @@ Definition Book_2_16 := @HoTT.Metatheory.FunextVarieties.NaiveFunext_implies_Fun
 (* ================================================== 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.
+Definition Book_2_18 := @HoTT.Basics.PathGroupoids.apD_natural.
 
 (* ================================================== ex:equiv-functor-set *)
 (** Exercise 3.1 *)

theories/Basics/PathGroupoids.v

@@ -479,14 +479,21 @@ Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A}
     | idpath => concat_p1_1p _
   end.
 
+Definition apD_natural {A : Type} {B : A -> Type} {f g : forall x, B x}
+  (p : forall x, f x = g x) {x y : A} (q : x = y)
+  : apD f q @ p y = ap (transport B q) (p x) @ apD g q.
+Proof.
+  destruct q.
+  unfold transport.
+  exact (concat_1p _ @ (ap_idmap _)^ @ (concat_p1 _)^).
+Defined.
+
 Definition apD_homotopic {A : Type} {B : A -> Type} {f g : forall x, B x}
   (p : forall x, f x = g x) {x y : A} (q : x = y)
   : apD f q = ap (transport B q) (p x) @ apD g q @ (p y)^.
 Proof.
   apply moveL_pV.
-  destruct q; unfold apD, transport.
-  symmetry.
-  exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
+  exact (apD_natural _ _).
 Defined.
 
 (** Naturality with other paths hanging around. *)