From e475a6c68514de297497e59a87a6ff6ff02e414b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 18 Jul 2024 11:51:26 -0500
Subject: [PATCH] exercises

---
 src/HoTTEST/Agda/Cubical/Exercises7.lagda.md     |  8 ++++++--
 src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md | 11 ++++++-----
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md b/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md
index 6c6ba2a..3af10b3 100644
--- a/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md
+++ b/src/HoTTEST/Agda/Cubical/Exercises7.lagda.md
@@ -139,11 +139,11 @@ module _ {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} where
 
   ΣPathP : Σ p ꞉ pr₁ x ≡ pr₁ y , PathP (λ i → B (p i)) (pr₂ x) (pr₂ y)
          → x ≡ y
-  ΣPathP = {!!}
+  ΣPathP (fst , snd) i = fst i , snd i
 
   PathPΣ : x ≡ y
          → Σ p ꞉ pr₁ x ≡ pr₁ y , PathP (λ i → B (p i)) (pr₂ x) (pr₂ y)
-  PathPΣ = {!!}
+  PathPΣ p = (λ i → Σ.fst (p i)) , (λ i → Σ.snd (p i))
 
   ΣPathP-PathPΣ : ∀ p → PathPΣ (ΣPathP p) ≡ p
   ΣPathP-PathPΣ = {!!}
@@ -172,6 +172,10 @@ and `Torus'` with a path constructor `square` that involves composition.
 
 Using these two ideas, define the *Klein bottle* in two different ways.
 
+```
+data KleinBottle : Type where
+```
+
 ### Exercise 10 (★★)
 
 Prove
diff --git a/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md b/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md
index 6a8ffc3..fd52330 100644
--- a/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md
+++ b/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md
@@ -35,10 +35,10 @@ open import sums
 Prove
 ```agda
 uncurry : {A B X : Type} → (A → B → X) → (A × B → X)
-uncurry = {!!}
+uncurry f (a , b) = f a b
 
 curry : {A B X : Type} → (A × B → X) → (A → B → X)
-curry = {!!}
+curry f a b = f (a , b)
 ```
 You might know these functions from programming e.g. in Haskell.
 But what do they say under the propositions-as-types interpretation?
@@ -108,7 +108,7 @@ tne = {!!}
 Prove
 ```agda
 ¬¬-functor : {A B : Type} → (A → B) → ¬¬ A → ¬¬ B
-¬¬-functor = {!!}
+¬¬-functor f ¬¬A ¬B = ¬¬A (λ A → ¬B (f A))
 
 ¬¬-kleisli : {A B : Type} → (A → ¬¬ B) → ¬¬ A → ¬¬ B
 ¬¬-kleisli = {!!}
@@ -131,7 +131,8 @@ to a true proposition while an uninhabited type corresponds to a false propositi
 With this in mind construct a family
 ```agda
 bool-as-type : Bool → Type
-bool-as-type = {!!}
+bool-as-type true = 𝟙
+bool-as-type false = {!  𝟘 !}
 ```
 such that `bool-as-type true` corresponds to "true" and
 `bool-as-type false` corresponds to "false". (Hint:
@@ -143,7 +144,7 @@ we have seen canonical types corresponding true and false in the lectures)
 Prove
 ```agda
 bool-≡-char₁ : ∀ (b b' : Bool) → b ≡ b' → (bool-as-type b ⇔ bool-as-type b')
-bool-≡-char₁ = {!!}
+bool-≡-char₁ b b' p = (λ x → {!   !}) , λ x → {!   !}
 ```