diff --git a/src/HDTT/hw2-handout.agda b/src/HDTT/hw2-handout.agda
new file mode 100644
index 0000000..62748e8
--- /dev/null
+++ b/src/HDTT/hw2-handout.agda
@@ -0,0 +1,160 @@
+{-# OPTIONS --without-K #-}
+
+module HDTT.hw2-handout where
+
+Type = Set₀
+
+record Σ (A : Type) (B : A → Type) : Type where
+  constructor _,_
+  field
+    fst : A
+    snd : B fst
+open Σ public
+infixr 60 _,_
+
+data _⊔_ (A : Type) (B : Type) : Type where
+  inl : A → A ⊔ B
+  inr : B → A ⊔ B
+infixr 4 _⊔_
+
+data ⊥ : Type where
+
+abort : ∀ {A : Type} → ⊥ → A
+abort ()
+
+data ℕ : Type where
+  zero : ℕ
+  suc  : (n : ℕ) → ℕ
+{-# BUILTIN NATURAL ℕ #-}
+
+data _≡_ {A : Type} (x : A) : A → Type where
+  refl : x ≡ x
+
+_∙_ : ∀ {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+refl ∙ q = q
+infixr 80 _∙_
+
+!_ : ∀ {A : Type} {x y : A} → x ≡ y → y ≡ x
+! refl = refl
+infixr 100 !_
+
+{- Lots of lemmas which may or may not be useful. -}
+
+∙-unit-r : ∀ {A : Type} {x y : A} (q : x ≡ y) → q ∙ refl ≡ q
+∙-unit-r refl = refl
+
+∙-unit-l : ∀ {A : Type} {x y : A} (q : x ≡ y) → refl ∙ q ≡ q
+∙-unit-l q = refl
+
+!-inv-l : ∀ {A : Type} {x y : A} (p : x ≡ y) → (! p) ∙ p ≡ refl
+!-inv-l refl = refl
+
+!-inv-r : ∀ {A : Type} {x y : A} (p : x ≡ y) → p ∙ (! p) ≡ refl
+!-inv-r refl = refl
+
+!-! : ∀ {A : Type} {x y : A} (p : x ≡ y) → ! (! p) ≡ p
+!-! refl = refl
+
+∙-assoc : ∀ {A : Type} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
+  → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
+∙-assoc refl q r = refl
+
+ap : ∀ {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
+ap f refl = refl
+
+ap-∙ : ∀ {A B : Type} (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
+  → ap f (p ∙ q) ≡ ap f p ∙ ap f q
+ap-∙ f refl q = refl
+
+ap-! : ∀ {A B : Type} (f : A → B) {x y : A} (p : x ≡ y) → ap f (! p) ≡ ! (ap f p)
+ap-! f refl = refl
+
+------------------------------------------------------------------------------------
+{- Task 1 -}
+------------------------------------------------------------------------------------
+
+-- loop spaces
+Ω² : ∀ (A : Type) → A → Type
+Ω² A x = (refl {x = x}) ≡ refl
+
+{- Task 1.1: prove this lemma -}
+ap-id : ∀ {A : Type} {x y : A} (p : x ≡ y) → ap (λ x → x) p ≡ p
+ap-id refl = refl
+
+-- binary version of ap
+ap2 : ∀ {A B C : Type} (f : A → B → C) {x y : A} → x ≡ y → {z w : B} → z ≡ w → f x z ≡ f y w
+ap2 f {x} {y} p {z} {w} q = ap (λ a → f a z) p ∙ ap (λ b → f y b) q
+
+{- Task 1.2: find another way to implement ap2 that is "symmetric" to the above ap2 -}
+ap2' : ∀ {A B C : Type} (f : A → B → C) {x y : A} → x ≡ y → {z w : B} → z ≡ w → f x z ≡ f y w
+ap2' f {x} refl q = ap (f x) q
+
+-- You might find this useful in Tasks 1.3 and 1.4
+lemma₀ : ∀ {A : Type} {x : A} (p : Ω² A x) → ap (λ x → x ∙ refl) p ≡ p
+lemma₀ {x = x} p = lemma₀' p ∙ ∙-unit-r p where
+  lemma₀' : ∀ {l : x ≡ x} (p : refl ≡ l) → ap (λ x → x ∙ refl) p ≡ p ∙ ! (∙-unit-r l)
+  lemma₀' refl = refl
+
+{- Task 1.3: check the definition of `ap2` and prove this lemma -}
+task1-3 : ∀ {A : Type} {x : A} (p q : Ω² A x) → ap2 (λ x y → x ∙ y) p q ≡ p ∙ q
+task1-3 p q = {!    !} where
+{- Hints:
+   1. What are the implicit arguments x, y, z, and w when applying ap2?
+   2. What's the relation between λ x → x and λ x → refl ∙ x? -}
+
+{- Task 1.4: prove this lemma -}
+task1-4 : ∀ {A : Type} {x : A} (p q : Ω² A x) → ap2' (λ x y → x ∙ y) p q ≡ q ∙ p
+task1-4 p q = {!   !}
+
+{- Task 1.5: prove that ap2 f p q ≡ ap2' f p q -}
+task1-5 : ∀ {A B C : Type} (f : A → B → C) {x y : A} (p : x ≡ y) {z w : B} (q : z ≡ w) → ap2 f p q ≡ ap2' f p q
+task1-5 f refl refl = refl
+
+{- Task 1.6: the final theorem -}
+eckmann-hilton : ∀ {A : Type} {x : A} (p q : Ω² A x) → p ∙ q ≡ q ∙ p
+eckmann-hilton p q = {!    !}
+
+------------------------------------------------------------------------------------
+{- Task 2 -}
+------------------------------------------------------------------------------------
+
+¬_ : Type → Type
+¬ A = A → ⊥
+
+has-all-paths : Type → Type
+has-all-paths A = (x y : A) → x ≡ y
+
+{- This version is different from what we had on 2/13.
+   One can show "has-all-paths" and "is-prop" are equivalent. -}
+is-set : Type → Type
+is-set A = (x y : A) → has-all-paths (x ≡ y)
+{- for comparison: the one on 2/13 was: is-set A = (x y : A) → is-prop (x ≡ y) -}
+
+has-dec-eq : Type → Type
+has-dec-eq A = (x y : A) → (x ≡ y) ⊔ (¬ (x ≡ y))
+
+replacement₁ : ∀ {A : Type} → has-dec-eq A → {x y : A} → x ≡ y → x ≡ y
+replacement₁ dec {x} {y} p with dec x y
+... | inl q = q
+... | inr ¬p = abort (¬p p)
+
+replacement₂ : ∀ {A : Type} → has-dec-eq A → {x y : A} → x ≡ y → x ≡ y
+replacement₂ dec p = ! (replacement₁ dec refl) ∙ replacement₁ dec p
+
+{- Task 2.1: the replacement is an identity function -}
+task2-1 : ∀ {A : Type} (dec : has-dec-eq A) {x y : A} (p : x ≡ y) → replacement₂ dec p ≡ p
+task2-1 dec refl = {! refl  !}
+
+{- Task 2.2: the replacement is (weakly) constant -}
+task2-2 : ∀ {A : Type} (dec : has-dec-eq A) {x y : A} (p q : x ≡ y) → replacement₂ dec p ≡ replacement₂ dec q
+task2-2 = {!   !}
+{- hints: start with "task2-2 dec {x} {y} p q with dec x y".
+   Agda will simplify the goal with the knowledge obtained from the pattern matching. -}
+
+{- Task 2.3: so... A is a set! -}
+hedberg : ∀ {A : Type} → has-dec-eq A → is-set A
+hedberg = {!   !}
+{- hints: if you are lost, start with "hedberg dec x y p q = {!!}" and use "C-c C-e"
+   to see the type of the hole in Emacs. -}
+
+-- Done? Remove the definition of "magic" to make sure you did not forget anything.
diff --git a/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md b/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md
index 3af10b3..fddb9a1 100644
--- a/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md
+++ b/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md
@@ -97,14 +97,8 @@ Use funExt⁻ to prove isSetΠ:
 
 ```agda
 isSetΠ : (h : (x : A) → isSet (B x)) → isSet ((x : A) → B x)
-isSetΠ h =
-  λ p q → -- p, q : (x : A) → B x
-    λ r s → -- r, s : p ≡ q
-      λ i j → -- j : p ≡ q, i : r j ≡ s j
-        λ x →
-          let
-            test = funExt⁻ r x
-          in {!   !}
+isSetΠ h = λ f g → λ p q → λ i j → λ x →
+  (h x) (f x) (g x) (funExt⁻ p x) (funExt⁻ q x) i j 
 ```
 
 ### Exercise 7 (★★★): alternative contractibility of singletons
@@ -121,7 +115,7 @@ Prove the corresponding version of contractibility of singetons for
 
 ```agda
 isContrSingl' : (x : A) → isContr (singl' x)
-isContrSingl' x = {!!}
+isContrSingl' x = (x , refl) , λ (y , p) i → p (~ i) , λ j → p (~ i ∨ j)
 ```
 
 ## Part III: Equality in Σ-types
@@ -146,10 +140,10 @@ module _ {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} where
   PathPΣ p = (λ i → Σ.fst (p i)) , (λ i → Σ.snd (p i))
 
   ΣPathP-PathPΣ : ∀ p → PathPΣ (ΣPathP p) ≡ p
-  ΣPathP-PathPΣ = {!!}
+  ΣPathP-PathPΣ (p , p2) i = p , p2
 
   PathPΣ-ΣPathP : ∀ p → ΣPathP (PathPΣ p) ≡ p
-  PathPΣ-ΣPathP = {!!}
+  PathPΣ-ΣPathP p i = p
 ```
 
 If one looks carefully the proof of prf in Lecture 7 uses ΣPathP
@@ -182,7 +176,26 @@ Prove
 
 ```agda
 suspUnitChar : Susp Unit ≡ Interval
-suspUnitChar = {!!}
+suspUnitChar = isoToPath (iso f g fg gf) where
+  f : Susp Unit → Interval
+  f north = zero
+  f south = one
+  f (merid a i) = seg i
+
+  g : Interval → Susp Unit
+  g zero = north
+  g one = south
+  g (seg i) = merid ⋆ i
+
+  fg : section f g
+  fg zero = refl
+  fg one = refl
+  fg (seg i) j = seg i
+
+  gf : retract f g
+  gf north = refl
+  gf south = refl
+  gf (merid ⋆ i) j = merid ⋆ i
 ```
 
 
@@ -197,11 +210,6 @@ Define suspension using the Pushout HIT and prove that it's equal to Susp.
 
 The goal of this exercise is to prove
 
-```agda
-suspBoolChar : Susp Bool ≡ S¹
-suspBoolChar = {!!}
-```
-
 For the map `Susp Bool → S¹`, we have to specify the behavior of two
 path constructors. The idea is to map one to `loop` and one to `refl`.
 
@@ -249,3 +257,52 @@ result, that is a direct consequence of `comp-filler` in `Cubical Agda`
 rUnit : {x y : A} (p : x ≡ y) → p ∙ refl ≡ p
 rUnit p = sym (comp-filler p refl)
 ```
+
+```agda
+suspBoolChar : Susp Bool ≡ S¹
+suspBoolChar = isoToPath (iso f g fg gf) where
+  f : Susp Bool → S¹
+  f north = base
+  f south = base
+  f (merid true i) = loop i
+  f (merid false i) = refl {x = base} i
+
+  g : S¹ → Susp Bool
+  g base = north
+  g (loop i) = (merid true ∙ sym (merid false)) i
+
+  q = ap
+
+  fg : section f g -- f(g(x)) ≡ x
+  fg base = refl
+  fg (loop i) k = 
+    -- f(g(loop)) ≡ loop
+    -- f(merid true ∙ sym (merid false)) ≡ loop
+    -- ap f (merid true) ∙ ap f (sym (merid false)) ≡ loop
+    -- (loop) ∙ (refl) ≡ loop
+    let
+      -- bottomFace = λ j =
+      --   let u = λ k → λ where
+      --     (i = i0) → f (refl {x = north} j)
+      --     (i = i1) → f (merid false (~ j))
+      --   in hfill u (inS (f (merid true i))) j
+
+      -- leftFace =
+      --   let u = λ j → λ where
+      --     (i = i0) → f (refl {x = north} j)
+      --     (i = i1) → f (merid false (~ j))
+      --   in hfill u (inS (f (merid true i))) {!    !}
+
+      u = λ j → λ where
+        (i = i0) → base
+        (i = i1) → f (merid false (~ j))
+        (k = i0) → comp-filler (λ i → f (merid true i)) (λ j → f (merid false (~ j))) j i
+        (k = i1) → loop i
+    in hcomp u (f (merid true i))
+
+  gf : retract f g -- g(f(x)) ≡ x
+  gf north = refl
+  gf south = merid false
+  gf (merid false i) j = merid false (i ∧ j)
+  gf (merid true i) j = {!   !}
+```
\ No newline at end of file
diff --git a/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md b/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md
index dcce9e2..a94df81 100644
--- a/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md
+++ b/src/HoTTEST/Agda/Cubical/Exercises8.lagda.md
@@ -40,7 +40,7 @@ Prove the propositional computation law for `J`:
 ```agda
 JRefl : {A : Type ℓ} {x : A} (P : (z : A) → x ≡ z → Type ℓ'')
   (d : P x refl) → J P d refl ≡ d
-JRefl P d = {!!}
+JRefl P d i = {!    !}
 ```
 
 ### Exercise 2 (★★)