removed J exercises from quest 2

1FundamentalGroup/Quest2Solutions.agda

@@ -36,42 +36,6 @@ data _⊔_ (A B : Type) : Type where
   leftInv (pos n) = refl
   leftInv (negsuc n) = refl
 
-∙refl : {A : Type} {x y : A} (p : x ≡ y) → p ∙ refl ≡ p
-∙refl = J (λ y p → p ∙ refl ≡ p) refl∙refl
-
-refl∙ : {A : Type} {x y : A} (p : x ≡ y) → refl ∙ p ≡ p
-refl∙ = J (λ y p → refl ∙ p ≡ p) refl∙refl
-
-∙sym : {A : Type} {x y : A} (p : x ≡ y) → p ∙ sym p ≡ refl
-∙sym = J (λ y p → p ∙ sym p ≡ refl)
-       (
-         refl ∙ sym refl
-       ≡⟨ cong (λ p → refl ∙ p) symRefl ⟩
-         refl ∙ refl
-       ≡⟨ refl∙refl ⟩
-         refl ∎)
-
-sym∙ : {A : Type} {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
-sym∙ = J (λ y p → (sym p) ∙ p ≡ refl)
-       (
-         (sym refl) ∙ refl
-       ≡⟨ cong (λ p → p ∙ refl) symRefl ⟩
-         refl ∙ refl
-       ≡⟨ refl∙refl ⟩
-         refl ∎)
-
-assoc : {A : Type} {w x : A} (p : w ≡ x) {y z : A} (q : x ≡ y) (r : y ≡ z)
-        → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
-assoc {A} = J
-        -- casing on p
-        (λ x p → {y z : A} (q : x ≡ y) (r : y ≡ z) → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r))
-        -- reduce to showing when p = refl
-        λ q r →  (refl ∙ q) ∙ r
-                 ≡⟨ cong (λ p' → p' ∙ r) (refl∙ q) ⟩
-                  q ∙ r
-                 ≡⟨ sym (refl∙ (q ∙ r)) ⟩
-                  refl ∙ q ∙ r ∎
-
 private
   variable
     A B : Type