Solution to exercise 2.1

This is a literate Rzk file:

#lang rzk-1

Problem statement

Show that the three obvious proofs of Lemma 2.1.2 are pairwise equal.

Lemma 2.1.2: (note we use \(\circ\) instead of square dot due to technical limitations)

For every type \(A\) and every \(x, y, z : A\) there is a function

\[ (x = y) \rightarrow (y = z) \rightarrow (x = z), \]

written \(p \mapsto q \mapsto p \circ q\), such that \(\text{refl}_x \circ \text{refl}_x \equiv \text{refl}_x\) for any \(x : A\). We call \(p \circ q\) the concatenation or composite of \(p\) and \(q\).

Solution