Solution to exercise 1.2

This is a literate Rzk file:

#lang rzk-1

Problem statement

Exercise 1.2

Derive the recursion principle for products \(\mathsf{rec}_{A \times B}\) using only the projections, and verify that the definitional equalities are valid. Do the same for \(\Sigma\)-types.

Solution for products

In this solution, we use prod and projections (pr₁ and pr₂), defined earlier in section 1.5.

Introducing constructor for values of prod type:

#def pair
  ( A B : U)
  : A → B → prod A B
  := \ a b → (a , b)

The type of the recursor on \(A \times B\) is

\[ \mathsf{rec}_{A \times B}: \prod_{C:\mathcal{U}} (A \to B \to C) \to A \times B \to C \]

It can be defined using projection as such:

\[ rec_{A\times B}(C, g, x) :\equiv g(\mathsf{pr}_1(x))(\mathsf{pr}_2(x)) \]

And represented in rzk like so:

#def prod-rec-via-projections
  ( A B : U)
  ( C : U)
  ( g : A → B → C)
  ( p : prod A B)
  : C
  := g (pr₁ A B p) (pr₂ A B p)

Definitions of projections via recursion in the other direction (pr₁-via-rec, pr₂-via-rec) were already provided in section 1.5.

Checking definitional equalities

Recursion from projections:

#def prod-rec-via-projections-works
  ( A B C : U)
  ( g : A → B → C)
  ( a : A)
  ( b : B)
  : prod-rec-via-projections A B C g (pair A B a b) = g a b
  := refl

TODO

Write down the explicit proofs (in latex/rzk syntax)

Projections from the recursion:

#def pr₁-via-rec-works
  ( A B : U)
  ( a : A)
  ( b : B)
  : pr₁-via-rec A B (pair A B a b) = a
  := refl

#def pr₂-from-rec-works
  ( A B : U)
  ( a : A)
  ( b : B)
  : pr₂-via-rec A B (pair A B a b) = b
  := refl

TODO

Write down the explicit proofs (in latex/rzk syntax)

Solution for dependant pairs

Similarly, for \(\Sigma\)-types, the recursion principle has the type:

\[ \mathsf{rec}_{\Sigma_{x:A}B(x)} : \Pi_{C:U}(\Pi_{x:A} B(x) \to C) \to (\Sigma_{x:A} B(x)) \to C \]

and can be defined using the projection functions as such:

\[ \mathsf{rec}_{\Sigma_{x:A}B(x)}(C, g, x) :\equiv g(\mathsf{pr}_1(x))(\mathsf{pr}_2(x)) \]

\(\Sigma\)-types are built-in. Also, pr₁-Σ, pr₂-Σ, rec-Σ, ind-Σ were already defined in section 1.6.

Defining recursion from pr₁-Σ and pr₂-Σ:

#def rec-Σ-via-projections
  ( A : U)
  ( B : A → U)
  ( C : U)
  ( g : (x : A) → B x → C)
  ( p : Σ (x : A) , B x)
  : C
  := g (pr₁-Σ A B p) (pr₂-Σ A B p)

(Extra, not in the task) Other direction of definition (projecitons via recursion):

#def pr₁-Σ-via-rec
  ( A : U)
  ( B : A → U)
  : ( Σ ( x : A) , B x) → A
  := rec-Σ A B A (\ x y → x)

For the second projection (\(\mathsf{pr}_2\)) we need the induction, since the output type depends on \(x : A\):

#def pr₂-Σ-via-rec
  ( A : U)
  ( B : A → U)
  : ( p : Σ (x : A) , B x) → (B (pr₁-Σ-via-rec A B p))
  := ind-Σ A B (\ p1 → B (pr₁-Σ-via-rec A B p1)) (\ x y → y)

Checking the definitional equalities

#def rec-Σ-via-projections-works
  ( A : U)
  ( B : A → U)
  ( C : U)
  ( g : (x : A) → B x → C)
  ( a : A)
  ( b : B a)
  : rec-Σ-via-projections A B C g (a , b) = g a b
  := refl

#def pr₁-Σ-via-rec-works
  ( A : U)
  ( B : A → U)
  ( a : A)
  ( b : B a)
  : pr₁-Σ-via-rec A B (a , b) = a
  := refl

#def pr₂-Σ-via-rec-works
  ( A : U)
  ( B : A → U)
  ( a : A)
  ( b : B a)
  : pr₂-Σ-via-rec A B (a , b) = b
  := refl

TODO

Write down the explicit proofs (in latex/rzk syntax)