Add exercise: all identity type families are equal

basics.tex

@@ -2691,7 +2691,35 @@ \section{Universal properties}
 \end{ex}
 
 \begin{ex}\label{ex:sigma-eq-components-neq}
-  We have seen that $\bfalse \neq \btrue$ (\cref{rmk:false-neq-true}). Show that, nevertheless, $(\bool, \bfalse) =_{\sm{A:\type}A} (\bool, \btrue)$ (see \cref{rmk:sigma-equality-extraction}).
+  We have seen that $\bfalse \neq \btrue$ (\cref{rmk:true-neq-false}). Show that, nevertheless, $(\bool, \bfalse) =_{\sm{A:\type}A} (\bool, \btrue)$ (see \cref{rmk:sigma-equality-extraction}).
+\end{ex}
+
+\begin{ex}
+  Suppose that we have a type family analogous to identity:
+
+  \[ \mathsf{Id}' : \prd{A:\UU} A \to A \to \UU \]
+
+  with a function analogous to reflexivity:
+
+  \[ \mathsf{refl}' : \prd{A:\UU}{a:A} \mathsf{Id}'_A(a, a) \]
+
+  and a function analogous to based path induction:
+
+  \[
+    \mathsf{ind}_{\mathsf{Id}'} :
+    \prd{A:\UU}
+    \prd{a:A}
+    \prd{C:\prd{x:A} \mathsf{Id}'_A(a, x) \to \UU}
+    \prd{c:C(a, \mathsf{refl}'_a)}
+    \sm{f:\prd{x:A} \prd{p:\mathsf{Id}'_A(a, x)} C(x, p)}
+    \mathsf{Id}'_{C(a, \mathsf{refl}'_a)}(f(a, \mathsf{refl}'_a), c)
+  \]
+
+  Show that $\mathsf{Id}' = \mathsf{Id}$. Deduce in particular that
+
+  \[ \prd{A,B:\UU} \eqv{(\mathsf{Id}'_{\UU}(A, B))}{(\eqv{A}{B})} \]
+
+  Hence, although we postulated univalence for the built-in identity type family $\mathsf{Id}$, it automatically applies to any type family with the same basic properties.
 \end{ex}
 
 % Local Variables: