Excercise 2.1

src/Chapter2/Exercises.lagda.md

@@ -9,6 +9,23 @@ module Chapter2.Exercises where
 
 open import Chapter2.Book public
 
+-- Exercise 2.1
+≡-trans-alt₁ : {A : 𝒰 𝒾} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+≡-trans-alt₁ (refl x) p = p
+
+≡-trans-alt₂ : {A : 𝒰 𝒾} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+≡-trans-alt₂ p (refl x) = p
+
+≡-trans-equal₁ :
+    {A : 𝒰 𝒾} {x y z : A} (p : x ≡ y) (q : y ≡ z)
+  → p ∙ q ≡ ≡-trans-alt₁ p q
+≡-trans-equal₁ (refl _) (refl _) = refl _
+
+≡-trans-equal₂ :
+    {A : 𝒰 𝒾} {x y z : A} (p : x ≡ y) (q : y ≡ z)
+  → p ∙ q ≡ ≡-trans-alt₂ p q
+≡-trans-equal₂ (refl _) (refl _) = refl _
+
 -- Exercise 2.10
 Σ-assoc : {A : 𝒰 𝒾} {B : A → 𝒰 𝒿} (C : (Σ x ꞉ A , B x) → 𝒰 𝓀)
         → (Σ x ꞉ A , (Σ y ꞉ B x , C (x , y))) ≃ (Σ p ꞉ (Σ x ꞉ A , B x) , C p)