1.5 Product types

This is a literate Rzk file:

#lang rzk-1

Rzk has built-in support for dependent pairs, so we define product types here in terms of those.

#define prod (A B : U)
  : U
  := Σ (_ : A) , B

To construct a pair, we can now simply use tuple syntax for \(\Sigma\)-types: (a, b).

To use a pair, we can use pattern matching or introduce projections:

#define pr₁
  ( A B : U)
  : prod A B → A
  := \ (a , _b) → a

#define pr₂
  ( A B : U)
  : prod A B → B
  := \ (_a , b) → b

The recursor for product types can be defined as follows:

#define prod-rec
  ( A B : U)
  : ( C : U) → (A → B → C) → prod A B → C
  := \ C f (a , b) → f a b

Then instead of defining functions such as pr1 and pr2 directly by a defining equation, we could define

#define pr₁-via-rec
  ( A B : U)
  : prod A B → A
  := prod-rec A B A (\ a _b → a)

#define pr₂-via-rec
  ( A B : U)
  : prod A B → B
  := prod-rec A B B (\ _a b → b)

To be able to define dependent functions over the product type, we have to generalize the recursor:

#define prod-ind
  ( A B : U)
  : ( C : prod A B → U) → ((x : A) → (y : B) → C (x , y)) → (x : prod A B) → C x
  := \ C f (x , y) → f x y

For example, in this way we can prove the propositional uniqueness principle, which says that every element of A × B is equal to a pair. Specifically, we can construct a function

#define prod-uniq
  ( A B : U)
  : ( x : prod A B) → (pr₁ A B x , pr₂ A B x) =_{prod A B} x
  := \ (a , b) → refl_{(a , b)}

Unit type

Rzk has a built-in Unit type which behaves slightly differently from the unit type in the HoTT Book. In particular, in Rzk, uniqueness principle for the unit type is built in, making some proofs easier than in the book.

Still, following the book, here is the recursor for the unit type:

#define Unit-rec
  : ( C : U) → C → Unit → C
  := \ _C c _unit → c

And, similarly, the induction principle for the unit type:

#define Unit-ind
  : ( C : Unit → U) → C unit → (x : Unit) → C x
  := \ _C c unit → c

Induction enables us to prove the propositional uniqueness principle for Unit, which asserts that its only inhabitant is unit:

#define Unit-uniq
  : ( x : Unit) → x = unit
  := Unit-ind (\ x → x = unit) refl_{unit}

As mentioned above, this uniqueness principle is built into Rzk (making any value of type Unit definitionally equal to unit), allowing to use refl immediately:

#define Unit-uniq'
  : ( x : Unit) → x = unit
  := \ _ → refl