Back to index

Chapter 1. Type Theory - Exercises

module Chapter1.Exercises where

open import Chapter1.Book public

-- Exercise 1.1
_∘_ : {X : 𝒰 𝒾} {Y : 𝒰 𝒿} {Z : Y β†’ 𝒰 𝓀}
    β†’ ((y : Y) β†’ Z y)
    β†’ (f : X β†’ Y)
    β†’ (x : X) β†’ Z (f x)
g ∘ f = Ξ» x β†’ g (f x)
infixl 70 _∘_

-- Exercise 1.2.
prjβ‡’rec-Ξ£ : {A : 𝒰 𝒾} {B : A β†’ 𝒰 𝒿} {C : 𝒰 𝓀}
          β†’ ((x : A) (y : B x) β†’ C)
          β†’ Ξ£ B β†’ C
prjβ‡’rec-Ξ£ g p = g (pr₁ p) (prβ‚‚ p)

_ : {A : 𝒰 𝒾} {B : A β†’ 𝒰 𝒿} {C : 𝒰 𝓀}
    β†’ (g : (x : A) (y : B x) β†’ C)
    β†’ (p : Ξ£ B) β†’ (rec-Ξ£ g p ≑ prjβ‡’rec-Ξ£ g p)
_ = Ξ» g p β†’ refl _

-- As the following exercises need additional theorems about the identity type,
-- we will introduce some of them now in a private block. These will be later
-- redefined in Chapter 2.
private
  _⁻¹ : {A : 𝒰 𝒾} β†’ {x y : A} β†’ x ≑ y β†’ y ≑ x
  (refl x)⁻¹ = refl x
  infix  40 _⁻¹

  _βˆ™_ : {A : 𝒰 𝒾} {x y z : A} β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z
  (refl x) βˆ™ (refl x) = (refl x)
  infixl 30 _βˆ™_

  begin_ : {A : 𝒰 𝒾} {x y : A} β†’ x ≑ y β†’ x ≑ y
  begin_ x≑y = x≑y
  infix  1 begin_

  _β‰‘βŸ¨βŸ©_ : {A : 𝒰 𝒾} (x {y} : A) β†’ x ≑ y β†’ x ≑ y
  _ β‰‘βŸ¨βŸ© x≑y = x≑y

  step-≑ : {A : 𝒰 𝒾} (x {y z} : A) β†’ y ≑ z β†’ x ≑ y β†’ x ≑ z
  step-≑ _ y≑z x≑y = x≑y βˆ™ y≑z
  syntax step-≑ x y≑z x≑y = x β‰‘βŸ¨ x≑y ⟩ y≑z

  step-β‰‘Λ˜ : {A : 𝒰 𝒾} (x {y z} : A) β†’ y ≑ z β†’ y ≑ x β†’ x ≑ z
  step-β‰‘Λ˜ _ y≑z y≑x = (y≑x)⁻¹ βˆ™ y≑z
  syntax step-β‰‘Λ˜ x y≑z y≑x = x β‰‘Λ˜βŸ¨ y≑x ⟩ y≑z
  infixr 2 _β‰‘βŸ¨βŸ©_ step-≑ step-β‰‘Λ˜

  _∎ : {A : 𝒰 𝒾} (x : A) β†’ x ≑ x
  _∎ x = refl x
  infix  3 _∎

  ap : {A : 𝒰 𝒾} {B : 𝒰 𝒿} (f : A β†’ B) {x x' : A} β†’ x ≑ x' β†’ f x ≑ f x'
  ap f {x} {x'} (refl x) = refl (f x)

  tr : {A : 𝒰 𝒾} (P : A β†’ 𝒰 𝒿) {x y : A}
     β†’ x ≑ y β†’ P x β†’ P y
  tr P (refl x) = id

-- Exercise 1.3.
uniq-Ξ£' : {A : 𝒰 𝒾} {P : A β†’ 𝒰 𝒿} (z : Ξ£ P)
        β†’ z ≑ (pr₁ z , prβ‚‚ z)
uniq-Ξ£' (x , y) = refl _

ind-Ξ£' : {A : 𝒰 𝒾} {B : A β†’ 𝒰 𝒿} {C : Ξ£ B β†’ 𝒰 𝓀}
       β†’ ((x : A) (y : B x) β†’ C (x , y))
       β†’ ((x , y) : Ξ£ B) β†’ C (x , y)
ind-Ξ£' {C = C} g p =
  tr C ((uniq-Ξ£' p)⁻¹) (g (pr₁ p) (prβ‚‚ p))

-- Exercise 1.4.
iter⇒rec-ℕ :
    (iter : (C : 𝒰 𝒾) β†’ C β†’ (C β†’ C) β†’ β„• β†’ C)
  β†’ (C : 𝒰 𝒾)
  β†’ C β†’ (β„• β†’ C β†’ C)
  β†’ β„• β†’ C
iter⇒rec-ℕ iter C c₀ c'ₛ n =
  pr₁ (iter (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) n)

iter⇒rec-ℕ-comp-0 :
    (iter : (C : 𝒰 𝒾) β†’ C β†’ (C β†’ C) β†’ β„• β†’ C)
  β†’ (iter-comp-0 : (C : 𝒰 𝒾) (cβ‚€ : C) (cβ‚› : C β†’ C) β†’  iter C cβ‚€ cβ‚› 0 ≑ cβ‚€)
  β†’ (iter-comp-succ : (C : 𝒰 𝒾) (cβ‚€ : C) (cβ‚› : C β†’ C) (n : β„•)
    β†’ iter C cβ‚€ cβ‚› (succ n) ≑ cβ‚› (iter C cβ‚€ cβ‚› n))
  β†’ (C : 𝒰 𝒾) (cβ‚€ : C) (cβ‚› : β„• β†’ C β†’ C)
  β†’ iterβ‡’rec-β„• iter C cβ‚€ cβ‚› 0 ≑ cβ‚€
iter⇒rec-ℕ-comp-0 iter iter-comp-0 iter-comp-succ C c₀ c'ₛ =
  ap pr₁ (iter-comp-0 (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)))

iter⇒rec-ℕ-comp-succ-helper :
    (iter : (C : 𝒰 𝒾) β†’ C β†’ (C β†’ C) β†’ β„• β†’ C)
  β†’ (iter-comp-0 : (C : 𝒰 𝒾) (cβ‚€ : C) (cβ‚› : C β†’ C) β†’  iter C cβ‚€ cβ‚› 0 ≑ cβ‚€)
  β†’ (iter-comp-succ : (C : 𝒰 𝒾) (cβ‚€ : C) (cβ‚› : C β†’ C) (n : β„•)
    β†’ iter C cβ‚€ cβ‚› (succ n) ≑ cβ‚› (iter C cβ‚€ cβ‚› n))
  β†’ (C : 𝒰 𝒾) (cβ‚€ : C) (c'β‚› : β„• β†’ C β†’ C) (n : β„•)
  β†’ prβ‚‚ (iter (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) n) ≑ n
iter⇒rec-ℕ-comp-succ-helper iter iter-comp-0 iter-comp-succ C c₀ c'ₛ zero =
  ap prβ‚‚ (iter-comp-0 (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)))
iter⇒rec-ℕ-comp-succ-helper iter iter-comp-0 iter-comp-succ C c₀ c'ₛ (succ n) =
  begin
  prβ‚‚ (iter (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) (succ n)) β‰‘βŸ¨ i ⟩
  prβ‚‚ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) (itern))                        β‰‘βŸ¨ ii ⟩
  prβ‚‚ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) (pr₁ itern , prβ‚‚ itern))        β‰‘βŸ¨βŸ©
  succ (prβ‚‚ itern)                                                      β‰‘βŸ¨ iii ⟩
  succ n                                                                ∎
  where
    i = ap prβ‚‚
      (iter-comp-succ (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) n)
    itern = iter (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) n
    ii = ap (Ξ» - β†’ prβ‚‚ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) -))
      (uniq-Ξ£' (iter (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) n))
    iii = ap succ
      (iter⇒rec-ℕ-comp-succ-helper iter iter-comp-0 iter-comp-succ C c₀ c'ₛ n)

iter⇒rec-ℕ-comp-succ :
    (iter : (C : 𝒰 𝒾) β†’ C β†’ (C β†’ C) β†’ β„• β†’ C)
  β†’ (iter-comp-0 : (C : 𝒰 𝒾) (cβ‚€ : C) (cβ‚› : C β†’ C) β†’  iter C cβ‚€ cβ‚› 0 ≑ cβ‚€)
  β†’ (iter-comp-succ : (C : 𝒰 𝒾) (cβ‚€ : C) (cβ‚› : C β†’ C) (n : β„•)
    β†’ iter C cβ‚€ cβ‚› (succ n) ≑ cβ‚› (iter C cβ‚€ cβ‚› n))
  β†’ (C : 𝒰 𝒾) (cβ‚€ : C) (c'β‚› : β„• β†’ C β†’ C) (n : β„•)
  β†’ iterβ‡’rec-β„• iter C cβ‚€ c'β‚› (succ n) ≑ c'β‚› n (iterβ‡’rec-β„• iter C cβ‚€ c'β‚› n)
iter⇒rec-ℕ-comp-succ iter iter-comp-0 iter-comp-succ C c₀ c'ₛ zero = begin
  iterβ‡’rec-β„• iter C cβ‚€ c'β‚› 1                                    β‰‘βŸ¨ i ⟩
  pr₁ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m))
    (iter (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) 0)) β‰‘βŸ¨ ii ⟩
  pr₁ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) (cβ‚€ , 0))               β‰‘βŸ¨βŸ©
  c'β‚› 0 cβ‚€                                                      β‰‘Λ˜βŸ¨ iii ⟩
  c'β‚› zero (iterβ‡’rec-β„• iter C cβ‚€ c'β‚› zero)                      ∎
  where
    i = ap pr₁
      (iter-comp-succ (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) 0)
    ii = ap (Ξ» - β†’ pr₁ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) -))
      (iter-comp-0 (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)))
    iii = ap (c'β‚› 0)
      (iter⇒rec-ℕ-comp-0 iter iter-comp-0 iter-comp-succ C c₀ c'ₛ)
iter⇒rec-ℕ-comp-succ iter iter-comp-0 iter-comp-succ C c₀ c'ₛ (succ n) = begin
  iterβ‡’rec-β„• iter C cβ‚€ c'β‚› (succ (succ n))                             β‰‘βŸ¨ i ⟩
  pr₁ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) iter-sn)                       β‰‘βŸ¨ ii ⟩
  pr₁ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) (pr₁ iter-sn , prβ‚‚ iter-sn))   β‰‘βŸ¨βŸ©
  c'β‚› (prβ‚‚ iter-sn) (pr₁ iter-sn)                                      β‰‘βŸ¨ iii ⟩
  c'β‚› (succ n) (iterβ‡’rec-β„• iter C cβ‚€ c'β‚› (succ n))                     ∎
  where
    iter-sn = iter (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) (succ n)
    i = ap pr₁
      (iter-comp-succ (C Γ— β„•) (cβ‚€ , 0) (Ξ» (c , m) β†’ (c'β‚› m c , succ m)) (succ n))
    ii = ap (Ξ» - β†’ pr₁ ((Ξ» (c , m) β†’ (c'β‚› m c , succ m)) -)) (uniq-Ξ£' iter-sn)
    iii = ap (Ξ» - β†’ c'β‚› - (pr₁ iter-sn))
      (iter⇒rec-ℕ-comp-succ-helper
        iter iter-comp-0 iter-comp-succ C cβ‚€ c'β‚› (succ n))