Exercises

This is a literate Rzk file:

#lang rzk-1

Exercise 1

Show that modus-ponens is equal to a specialised identity.

Solution to Exercise 1

Exercise 1

#define eq-modus-ponens-identity
  (A B : U)
  : modus-ponens A B = identity (A → B)
  := refl

Exercise 2

Define composition of (non-dependent) functions. That is, given f : A → B and g : B → C, provide a function of type A → C.

Solution to Exercise 2

#define compose
  (A B C : U)
  (f : A → B)
  (g : B → C)
  : A → C
  := \ x → g (f x)

Exercise 3

Show that the composition of 2-to-Σ and Σ-to-2 either way is equal to identity.

Solution to Exercise 3

#define eq-Σ-to-2-to-Σ
  (funext : FunExt)
  (A : U)
  (d : 2 → A)
  : compose
      (2 → A) (Σ-arrow A) (2 → A)
      (2-to-Σ A) (Σ-to-2 A)
    = identity (2 → A)
  := funext (2 → A) (2 → A)
        (compose (2 → A) (Σ-arrow A) (2 → A) (2-to-Σ A) (Σ-to-2 A))
        (identity (2 → A))
        (\_ → refl)

#define eq-2-to-Σ-to-2
  (funext : FunExt)
  (A : U)
  (xyf : Σ-arrow A)
  : compose
      (Σ-arrow A) (2 → A) (Σ-arrow A)
      (Σ-to-2 A) (2-to-Σ A)
    = identity (Σ-arrow A)
  := funext (Σ-arrow A) (Σ-arrow A)
      (compose (Σ-arrow A) (2 → A) (Σ-arrow A) (Σ-to-2 A) (2-to-Σ A))
      (identity (Σ-arrow A))
      (\_ → refl)