diff --git a/src/HoTTEST/Agda/Exercises/01-Exercises.lagda.md b/src/HoTTEST/Agda/Exercises/01-Exercises.lagda.md
index c5fc2a7..5446123 100644
--- a/src/HoTTEST/Agda/Exercises/01-Exercises.lagda.md
+++ b/src/HoTTEST/Agda/Exercises/01-Exercises.lagda.md
@@ -40,7 +40,10 @@ the leftmost argument only.
 
 ```agda
 _&&'_ : Bool → Bool → Bool
-a &&' b = {!!}
+true &&' true = true
+true &&' false = false
+false &&' true = false
+false &&' false = false
 ```
 
 One advantage of this definition is that it reads just like a Boolean truth
@@ -54,7 +57,10 @@ verbose definition.
 
 ```agda
 _xor_ : Bool → Bool → Bool
-a xor b = {!!}
+true xor true = false
+true xor false = true
+false xor true = true
+false xor false = false
 ```
 
 ### Exercise 3 (★)
@@ -67,16 +73,18 @@ left hand side and the right hand side compute to the same value.
 
 ```agda
 _^_ : ℕ → ℕ → ℕ
-n ^ m = {!!}
+n ^ zero = 1
+n ^ suc m = n * (n ^ m)
 
 ^-example : 3 ^ 4 ≡ 81
-^-example = {!!} -- refl 81 should fill the hole here
+^-example = refl 81 -- refl 81 should fill the hole here
 
 _! : ℕ → ℕ
-n ! = {!!}
+zero ! = 1
+suc n ! = (suc n) * (n !)
 
 !-example : 4 ! ≡ 24
-!-example = {!!} -- refl 24 should fill the hole here
+!-example = refl 24 -- refl 24 should fill the hole here
 ```
 
 ### Exercise 4 (★)
@@ -93,10 +101,13 @@ max (suc n) (suc m) = suc (max n m)
 
 ```agda
 min : ℕ → ℕ → ℕ
-min = {!!}
+min zero zero = zero
+min zero (suc y) = zero
+min (suc x) zero = zero
+min (suc x) (suc y) = 1 + min x y
 
 min-example : min 5 3 ≡ 3
-min-example = {!!} -- refl 3 should fill the hole here
+min-example = refl 3 -- refl 3 should fill the hole here
 ```
 
 ### Exercise 5 (★)
@@ -110,10 +121,11 @@ element of the list `xs` and returns the resulting list.
 
 ```agda
 map : {X Y : Type} → (X → Y) → List X → List Y
-map f xs = {!!}
+map {X} {Y} f [] = []
+map {X} {Y} f (x :: xs) = f x :: map f xs
 
 map-example : map (_+ 3) (1 :: 2 :: 3 :: []) ≡ 4 :: 5 :: 6 :: []
-map-example = {!!} -- refl _ should fill the hole here
+map-example = refl _ -- refl _ should fill the hole here
 
                    -- We write the underscore, because we don't wish to repeat
                    -- the relatively long "4 :: 5 :: 6 :: []" and Agda can
@@ -130,14 +142,15 @@ should return [4 , 3 , 1], see the code below.
 
 ```agda
 filter : {X : Type} (p : X → Bool) → List X → List X
-filter = {!!}
+filter p [] = []
+filter p (x :: xs) = if p x then x :: filter p xs else filter p xs
 
 is-non-zero : ℕ → Bool
 is-non-zero zero    = false
 is-non-zero (suc _) = true
 
 filter-example : filter is-non-zero (4 :: 3 :: 0 :: 1 :: 0 :: []) ≡ 4 :: 3 :: 1 :: []
-filter-example = {!!} -- refl _ should fill the hole here
+filter-example = refl _ -- refl _ should fill the hole here
 ```
 
 ## Part II: The identity type of the Booleans (★/★★)
@@ -152,7 +165,10 @@ are the same natural number, or else is empty, if `x` and `y` are different.
 
 ```agda
 _≣_ : Bool → Bool → Type
-a ≣ b = {!!}
+true ≣ true = 𝟙
+true ≣ false = 𝟘
+false ≣ true = 𝟘
+false ≣ false = 𝟙
 ```
 
 ### Exercise 2 (★)
@@ -161,7 +177,8 @@ a ≣ b = {!!}
 
 ```agda
 Bool-refl : (b : Bool) → b ≣ b
-Bool-refl = {!!}
+Bool-refl true = ⋆
+Bool-refl false = ⋆
 ```
 
 ### Exercise 3 (★★)
@@ -175,10 +192,16 @@ back and forth between `a ≣ b` and `a ≡ b`.
 
 ```agda
 ≡-to-≣ : (a b : Bool) → a ≡ b → a ≣ b
-≡-to-≣ = {!!}
+≡-to-≣ true true x = ⋆
+≡-to-≣ true false ()
+≡-to-≣ false true ()
+≡-to-≣ false false x = ⋆
 
 ≣-to-≡ : (a b : Bool) → a ≣ b → a ≡ b
-≣-to-≡ = {!!}
+≣-to-≡ true true ⋆ = refl _
+≣-to-≡ true false ()
+≣-to-≡ false true ()
+≣-to-≡ false false ⋆ = refl _
 ```
 
 ## Part III: Proving in Agda (★★/★★★)
@@ -199,7 +222,10 @@ Use pattern matching to **prove** that `||` is commutative.
 
 ```agda
 ||-is-commutative : (a b : Bool) → a || b ≡ b || a
-||-is-commutative a b = {!!}
+||-is-commutative true true = refl _
+||-is-commutative true false = refl _
+||-is-commutative false true = refl _
+||-is-commutative false false = refl _
 ```
 
 ### Exercise 2 (★★)
@@ -208,8 +234,11 @@ Taking inspiration from the above, try to **state** and **prove** that `&&` is
 commutative.
 
 ```agda
-&&-is-commutative : {!!}
-&&-is-commutative = {!!}
+&&-is-commutative : (a b : Bool) → a && b ≡ b && a
+&&-is-commutative true true = refl _
+&&-is-commutative true false = refl _
+&&-is-commutative false true = refl _
+&&-is-commutative false false = refl _
 ```
 
 ### Exercise 3 (★★)
@@ -218,10 +247,24 @@ commutative.
 
 ```agda
 &&-is-associative : (a b c : Bool) → a && (b && c) ≡ (a && b) && c
-&&-is-associative = {!!}
+&&-is-associative true true true = refl _
+&&-is-associative true true false = refl _
+&&-is-associative true false true = refl _
+&&-is-associative true false false = refl _
+&&-is-associative false true true = refl _
+&&-is-associative false true false = refl _
+&&-is-associative false false true = refl _
+&&-is-associative false false false = refl _
 
 &&'-is-associative : (a b c : Bool) → a &&' (b &&' c) ≡ (a &&' b) &&' c
-&&'-is-associative = {!!}
+&&'-is-associative true true true = refl _
+&&'-is-associative true true false = refl _
+&&'-is-associative true false true = refl _
+&&'-is-associative true false false = refl _
+&&'-is-associative false true true = refl _
+&&'-is-associative false true false = refl _
+&&'-is-associative false false true = refl _
+&&'-is-associative false false false = refl _
 ```
 
 **Question**: Can you spot a downside of the more verbose definition of `&&'`
@@ -249,7 +292,10 @@ max-is-commutative (suc n) (suc m) = to-show
 
 ```agda
 min-is-commutative : (n m : ℕ) → min n m ≡ min m n
-min-is-commutative = {!!}
+min-is-commutative zero zero = refl _
+min-is-commutative zero (suc m) = refl _
+min-is-commutative (suc n) zero = refl _
+min-is-commutative (suc n) (suc m) = ap suc (min-is-commutative n m)
 ```
 
 ### Exercise 5 (★★★)
@@ -259,7 +305,8 @@ number `n`.
 
 ```agda
 0-right-neutral : (n : ℕ) → n ≡ n + 0
-0-right-neutral = {!!}
+0-right-neutral zero = refl _
+0-right-neutral (suc n) = ap suc (0-right-neutral n)
 ```
 
 ### Exercise 6 (★★★)
@@ -271,9 +318,11 @@ Try to **prove** these equations using pattern matching and inductive proofs.
 
 ```agda
 map-id : {X : Type} (xs : List X) → map id xs ≡ xs
-map-id xs = {!!}
+map-id {X} [] = refl _
+map-id {X} (x :: xs) = ap (λ xs → x :: xs) (map-id xs)
 
 map-comp : {X Y Z : Type} (f : X → Y) (g : Y → Z)
            (xs : List X) → map (g ∘ f) xs ≡ map g (map f xs)
-map-comp f g xs = {!!}
+map-comp {X} {Y} {Z} f g [] = refl _
+map-comp {X} {Y} {Z} f g (x :: xs) = ap (λ xs → g (f x) :: xs) (map-comp f g xs)
 ```