Exercises for Section 1¶

Exercise 1.1¶

Given functions \(f : A \to B\) and \(g : B \to C\), define their composite \(g \circ f : A \to C\). Show that we have \(h \circ (g \circ f) \equiv (h \circ g) \circ f\).

Go to solution

Exercise 1.2¶

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

Go to solution

Exercise 1.3¶

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.)

Go to solution