Solution to exercise 1.3

This is a literate Rzk file:

#lang rzk-1

Problem statement

Derive the induction principle for products \(ind_{A \times B}\), using only the projections and the propositional uniqueness principle \(uniq_{A \times B}\). Verify that the definitional equalities are valid. Generalize \(uniq_{A \times B}\) to \(\Sigma\)-types, and do the same for \(\Sigma\)-types. (This requires concepts from Chapter 2.)

Solution