exercises: solution to eq-proofs-commute

HoTT · Oct 22, 2017 · d24b93d · d24b93d
1 parent 7760aba
commit d24b93d
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v
@@ -272,7 +272,14 @@ End Book_2_1_Proofs_Are_Equal.
 (* ================================================== ex:eq-proofs-commute *)
 (** Exercise 2.2 *)
 
-
+Definition Book_2_2 :
+  forall {A : Type} {x y z : A} (p : x = y) (q : y = z), 
+    (Book_2_1_concatenation1_eq_Book_2_1_concatenation2 p q) ⬛1
+    (Book_2_1_concatenation2_eq_Book_2_1_concatenation3 p q) =
+    (Book_2_1_concatenation1_eq_Book_2_1_concatenation3 p q).
+  induction p, q.
+  reflexivity.
+Defined.
 
 (* ================================================== ex:fourth-concat *)
 (** Exercise 2.3 *)