exercises3

src/HoTTEST/Agda/Exercises/03-Exercises.lagda.md

@@ -43,13 +43,13 @@ can be inferred directly from the same operations on paths.
 Try to prove reflexivity, symmetry and transitivity of `_∼_` by filling these holes.
 ```agda
   ∼-refl : (f : (x : A) → B x) → f ∼ f
-  ∼-refl f = {!!}
+  ∼-refl f x = refl (f x)
 
   ∼-inv : (f g : (x : A) → B x) → (f ∼ g) → (g ∼ f)
-  ∼-inv f g H x = {!!}
+  ∼-inv f g H x = sym (H x)
 
   ∼-concat : (f g h : (x : A) → B x) → f ∼ g → g ∼ h → f ∼ h
-  ∼-concat f g h H K x = {!!}
+  ∼-concat f g h H K x = H x ∙ K x
 
   infix 0 _∼_
 ```
@@ -84,10 +84,10 @@ infix 0 _≅_
 Reformulate the same definition using Sigma-types.
 ```agda
 is-bijection' : {A B : Type} → (A → B) → Type
-is-bijection' f = {!!}
+is-bijection' {A} {B} f = Sigma (B → A) λ g → (g ∘ f ∼ id) × (f ∘ g ∼ id)
 
 _≅'_ : Type → Type → Type
-A ≅' B = {!!}
+A ≅' B = Sigma (A → B) is-bijection'
 ```
 The definition with `Σ` is probably more intuitive, but, as discussed above,
 the definition with a record is often easier to work with,
@@ -115,26 +115,26 @@ Prove that 𝟚 and Bool are isomorphic
 
 ```agda
 Bool-𝟚-isomorphism : Bool ≅ 𝟚
-Bool-𝟚-isomorphism = record { bijection = {!!} ; bijectivity = {!!} }
+Bool-𝟚-isomorphism = record { bijection = f ; bijectivity = f-is-bijection }
  where
   f : Bool → 𝟚
-  f false = {!!}
-  f true  = {!!}
+  f false = 𝟎
+  f true  = 𝟏
 
   g : 𝟚 → Bool
-  g 𝟎 = {!!}
-  g 𝟏 = {!!}
+  g 𝟎 = false
+  g 𝟏 = true
 
   gf : g ∘ f ∼ id
-  gf true  = {!!}
-  gf false = {!!}
+  gf true  = refl true
+  gf false = refl false
 
   fg : f ∘ g ∼ id
-  fg 𝟎 = {!!}
-  fg 𝟏 = {!!}
+  fg 𝟎 = refl 𝟎
+  fg 𝟏 = refl 𝟏
 
   f-is-bijection : is-bijection f
-  f-is-bijection = record { inverse = {!!} ; η = {!!} ; ε = {!!} }
+  f-is-bijection = record { inverse = g ; η = gf ; ε = fg }
 ```
 
 
@@ -161,8 +161,8 @@ Fin-elim : (A : {n : ℕ} → Fin n → Type)
 Fin-elim A a f = h
  where
   h : {n : ℕ} (k : Fin n) → A k
-  h zero    = {!!}
-  h (suc k) = {!!}
+  h zero    = a
+  h (suc k) = f k (h k)
 ```
 
 We give the other definition of the finite types and introduce some notation.
@@ -188,23 +188,23 @@ Fin-isomorphism : (n : ℕ) → Fin n ≅ Fin' n
 Fin-isomorphism n = record { bijection = f n ; bijectivity = f-is-bijection n }
  where
   f : (n : ℕ) → Fin n → Fin' n
-  f (suc n) zero    = {!!}
-  f (suc n) (suc k) = {!!}
+  f (suc n) zero    = inl ⋆
+  f (suc n) (suc k) = inr (f n k)
 
   g : (n : ℕ) → Fin' n → Fin n
-  g (suc n) (inl ⋆) = {!!}
-  g (suc n) (inr k) = {!!}
+  g (suc n) (inl ⋆) = zero
+  g (suc n) (inr k) = suc (g n k)
 
   gf : (n : ℕ) → g n ∘ f n ∼ id
-  gf (suc n) zero    = {!!}
+  gf (suc n) zero    = refl zero
   gf (suc n) (suc k) = γ
    where
     IH : g n (f n k) ≡ k
     IH = gf n k
 
-    γ = g (suc n) (f (suc n) (suc k)) ≡⟨ {!!} ⟩
-        g (suc n) (suc' (f n k))      ≡⟨ {!!} ⟩
-        suc (g n (f n k))             ≡⟨ {!!} ⟩
+    γ = g (suc n) (f (suc n) (suc k)) ≡⟨ refl (g (suc n) (inr (f n k))) ⟩
+        g (suc n) (suc' (f n k))      ≡⟨ refl (g (suc n) (inr (f n k))) ⟩
+        suc (g n (f n k))             ≡⟨ ap suc IH ⟩
         suc k                         ∎
 
   fg : (n : ℕ) → f n ∘ g n ∼ id
@@ -214,9 +214,9 @@ Fin-isomorphism n = record { bijection = f n ; bijectivity = f-is-bijection n }
     IH : f n (g n k) ≡ k
     IH = fg n k
 
-    γ = f (suc n) (g (suc n) (suc' k)) ≡⟨ {!!} ⟩
-        f (suc n) (suc (g n k))        ≡⟨ {!!} ⟩
-        suc' (f n (g n k))             ≡⟨ {!!} ⟩
+    γ = f (suc n) (g (suc n) (suc' k)) ≡⟨ refl (f (suc n) (suc (g n k))) ⟩
+        f (suc n) (suc (g n k))        ≡⟨ refl (f (suc n) (suc (g n k))) ⟩
+        suc' (f n (g n k))             ≡⟨ ap suc' IH ⟩
         suc' k                         ∎
 
   f-is-bijection : (n : ℕ) → is-bijection (f n)
@@ -234,9 +234,9 @@ Give the recursive definition of the less than or equals relation on the natural
 
 ```agda
 _≤₁_ : ℕ → ℕ → Type
-0     ≤₁ y     = {!!}
-suc x ≤₁ 0     = {!!}
-suc x ≤₁ suc y = {!!}
+0     ≤₁ y     = Fin (suc y)
+suc x ≤₁ 0     = 𝟘
+suc x ≤₁ suc y = x ≤₁ y
 ```
 
 ### Exercise 7 (⋆)
@@ -261,7 +261,8 @@ minimal-element P = Σ n ꞉ ℕ , (P n) × (is-lower-bound P n)
 Prove that all numbers are at least as large as zero.
 ```agda
 leq-zero : (n : ℕ) → 0 ≤₁ n
-leq-zero n = {!!}
+leq-zero zero = zero
+leq-zero (suc n) = suc (leq-zero n)
 ```
 
 
@@ -347,3 +348,4 @@ is-zero-well-ordering-principle P d zero p p0 = {!   !}
 is-zero-well-ordering-principle P d (suc m) pm =
   is-zero-well-ordering-principle-suc P d m pm (d 0) {!!}
 ```
+