exercises

.vscode/settings.json

@@ -3,5 +3,5 @@
 	"gitdoc.enabled": false,
 	"gitdoc.autoCommitDelay": 300000,
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
-	"agdaMode.connection.commandLineOptions": "--no-load-primitives"
+	"agdaMode.connection.commandLineOptions": ""
 }

src/HoTTEST/Agda/Cubical/Exercises7.lagda.md

@@ -42,11 +42,21 @@ private
 
 State and prove funExt for dependent functions `f g : (x : A) → B x`
 
+```
+funExtDep : {f g : (x : A) → B x}
+  → ((x : A) → f x ≡ g x)
+  → f ≡ g
+funExtDep p i x = (p x) i
+```
+
 ### Exercise 2 (★)
 
 Generalize the type of ap to dependent function `f : (x : A) → B x`
 (hint: the result should be a `PathP`)
 
+```
+-- apDep : 
+```
 
 ## Part II: Some facts about (homotopy) propositions and sets
 
@@ -65,7 +75,11 @@ Prove
 
 ```agda
 isPropΠ : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x)
-isPropΠ = {!!}
+isPropΠ h f g i x =
+  let
+    a = f x
+    b = g x
+  in h x a b i
 ```
 
 ### Exercise 5 (★)
@@ -74,7 +88,7 @@ Prove the inverse of `funExt` (sometimes called `happly`):
 
 ```agda
 funExt⁻ : {f g : (x : A) → B x} → f ≡ g → ((x : A) → f x ≡ g x)
-funExt⁻  = {!!}
+funExt⁻ p x i = p i x
 ```
 
 ### Exercise 6 (★★)
@@ -83,7 +97,14 @@ Use funExt⁻ to prove isSetΠ:
 
 ```agda
 isSetΠ : (h : (x : A) → isSet (B x)) → isSet ((x : A) → B x)
-isSetΠ = {!!}
+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 {!   !}
 ```
 
 ### Exercise 7 (★★★): alternative contractibility of singletons
@@ -165,6 +186,8 @@ suspUnitChar = {!!}
 
 Define suspension using the Pushout HIT and prove that it's equal to Susp.
 
+```
+```
 
 ### Exercise 12 (🌶)