add hott book files

src/HottBook/Chapter2.lagda.md

@@ -0,0 +1,4 @@
+```
+module HottBook.Chapter2 where
+```
+

src/HottBook/Chapter2Exercises.lagda.md

@@ -0,0 +1,43 @@
+```
+module HottBook.Chapter2Exercises where
+
+open import Relation.Binary.PropositionalEquality
+Type = Set
+transport = subst
+```
+
+## Exercise 2.4
+
+Define, by induction on n, a general notion of n-dimensional path in a type A,
+simultaneously with the type of boundaries for such paths.
+
+(tracked in [#6][6])
+
+[6]: https://git.mzhang.io/school/cubical/issues/6
+
+```
+
+```
+
+## Exercise 2.5
+
+Prove that the functions [2.3.6] and (2.3.7) are inverse equivalences.
+
+[2.3.6]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.6
+[2.3.7]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.7
+
+Here is the definition of transportconst from lemma 2.3.5:
+
+```
+transportconst : {A : Type} {x y : A} (B : Type) → (p : x ≡ y) → (b : B)
+  → transport (λ _ → B) p b ≡ b
+transportconst {A} {x} B p b =
+  let
+    D : (x y : A) → (p : x ≡ y) → Type
+    D x y p = transport (λ _ → B) p b ≡ b
+
+    d : (x : A) → D x x refl
+    d x = refl
+  in
+  J (λ x p → transport (λ _ → B) p b ≡ b) p (d x)
+```