Week 02 - Agda Exercises

Please read before starting the exercises

The exercises are designed to increase in difficulty so that we can cater to our large and diverse audience. This also means that it is perfectly fine if you don’t manage to do all exercises: some of them are definitely a bit hard for beginners and there are likely too many exercises! You may wish to come back to them later when you have learned more.

Having said that, here we go!

This is a markdown file with Agda code, which means that it displays nicely on GitHub, but at the same time you can load this file in Agda and fill the holes to solve exercises.

Please make a copy of this file to work in, so that it doesn’t get overwritten (in case we update the exercises through git)!

{-# OPTIONS --without-K --allow-unsolved-metas #-}

module 02-Exercises where

open import prelude
open import decidability
open import sums

Part I: Propositions as types

Exercise 1 (★)

Prove 
uncurry : {A B X : Type} → (A → B → X) → (A × B → X)
uncurry = {!!}

curry : {A B X : Type} → (A × B → X) → (A → B → X)
curry = {!!}

You might know these functions from programming e.g. in Haskell. But what do they say under the propositions-as-types interpretation?

Exercise 2 (★)

Consider the following goals: 
[i] : {A B C : Type} → (A × B) ∔ C → (A ∔ C) × (B ∔ C)
[i] = {!!}

[ii] : {A B C : Type} → (A ∔ B) × C → (A × C) ∔ (B × C)
[ii] = {!!}

[iii] : {A B : Type} → ¬ (A ∔ B) → ¬ A × ¬ B
[iii] = {!!}

[iv] : {A B : Type} → ¬ (A × B) → ¬ A ∔ ¬ B
[iv] = {!!}

[v] : {A B : Type} → (A → B) → ¬ B → ¬ A
[v] = {!!}

[vi] : {A B : Type} → (¬ A → ¬ B) → B → A
[vi] = {!!}

[vii] : {A B : Type} → ((A → B) → A) → A
[vii] = {!!}

[viii] : {A : Type} {B : A → Type}
    → ¬ (Σ a ꞉ A , B a) → (a : A) → ¬ B a
[viii] = {!!}

[ix] : {A : Type} {B : A → Type}
    → ¬ ((a : A) → B a) → (Σ a ꞉ A , ¬ B a)
[ix] = {!!}

[x] : {A B : Type} {C : A → B → Type}
      → ((a : A) → (Σ b ꞉ B , C a b))
      → Σ f ꞉ (A → B) , ((a : A) → C a (f a))
[x] = {!!}

For each goal determine whether it is provable or not. If it is, fill it. If not, explain why it shouldn’t be possible. Propositions-as-types might help.

Exercise 3 (★★)

¬¬_ : Type → Type
¬¬ A = ¬ (¬ A)

¬¬¬ : Type → Type
¬¬¬ A = ¬ (¬¬ A)
In the lecture we have discussed that we can’t prove ∀ {A : Type} → ¬¬ A → A. What you can prove however, is 
tne : ∀ {A : Type} → ¬¬¬ A → ¬ A
tne = {!!}

Exercise 4 (★★★)

Prove 
¬¬-functor : {A B : Type} → (A → B) → ¬¬ A → ¬¬ B
¬¬-functor = {!!}

¬¬-kleisli : {A B : Type} → (A → ¬¬ B) → ¬¬ A → ¬¬ B
¬¬-kleisli = {!!}

Hint: For the second goal use tne from the previous exercise

Part II: _≡_ for Bool

In this exercise we want to investigate what equality of booleans looks like. In particular we want to show that for true false : Bool we have true ≢ false.

Exercise 1 (★)

Under the propositions-as-types paradigm, an inhabited type corresponds to a true proposition while an uninhabited type corresponds to a false proposition. With this in mind construct a family 
bool-as-type : Bool → Type
bool-as-type = {!!}

such that bool-as-type true corresponds to “true” and bool-as-type false corresponds to “false”. (Hint: we have seen canonical types corresponding true and false in the lectures)

Exercise 2 (★★)

Prove 
bool-≡-char₁ : ∀ (b b' : Bool) → b ≡ b' → (bool-as-type b ⇔ bool-as-type b')
bool-≡-char₁ = {!!}

Exercise 3 (★★)

Using ex. 2, conclude that 
true≢false : ¬ (true ≡ false)
true≢false ()

You can actually prove this much easier! How?

Exercise 4 (★★★)

Finish our characterisation of _≡_ by proving 
bool-≡-char₂ : ∀ (b b' : Bool) → (bool-as-type b ⇔ bool-as-type b') → b ≡ b'
bool-≡-char₂ = {!!}

Part III (🌶)

A type A is called discrete if it has decidable equality. Consider the following predicate on types: 
has-bool-dec-fct : Type → Type
has-bool-dec-fct A = Σ f ꞉ (A → A → Bool) , (∀ x y → x ≡ y ⇔ (f x y) ≡ true)

Prove that

decidable-equality-char : (A : Type) → has-decidable-equality A ⇔ has-bool-dec-fct A
decidable-equality-char = ?