6.1 Induction, in abstract

In this section, we prove a theorem on inductive constructions using a proof-irrelevant \( \mathsf{Prop}\).

Definition 6.1

Let \( I : \mathsf{Type}_u \) be a type with a well-founded transitive relation \( \prec \). Let \( A : I \to \mathsf{Type}_v \) be a family of types indexed by \( I \), and let

\[ B : \prod _{i : I} A_i \to \left(\prod _{j : I} j \prec i \to A_j\right) \to \mathsf{Sort}_w \]

An inductive construction for \( (I, A, B) \) is a pair of functions

\begin{align*} & F_A : \prod _{i : I} \prod _{d : \prod _{j : I} j \prec i \to A_j} \\ & \quad \left( \prod _{j : I} \prod _{h : j \prec i} B\ j\ (d\ j\ h)\ (k\ h’ \mapsto d\ k\ (\operatorname {\mathsf{trans}}(h’,h))) \right) \to A_i \\ & F_B : \prod _{i : I} \prod _{d : \prod _{j : I} j \prec i \to A_j} \\ & \quad \prod _{h : \left( \prod _{j : I} \prod _{h : j \prec i} B\ j\ (d\ j\ h)\ (k\ h' \mapsto d\ k\ (\operatorname {\mathsf{trans}}(h',h))) \right)} B\ i\ (F_A\ i\ d\ h)\ d \end{align*}

Proposition 6.2 inductive construction theorem for propositions

Let \( (F_A, F_B) \) be an inductive construction for \( (I, A, B) \), where \( w \) is \( 0 \). Then there are computable functions

\[ G : \prod _{i : I} A_i;\quad H : \prod _{i : I} B\ i\ G_i\ (j\ \_ \mapsto G_j) \]

such that for each \( i : I \),

\[ G_i = F_A\ i\ (j\ \_ \mapsto G_j)\ (F_B\ i\ (j\ \_ \mapsto H_j)) \]

Proof ▶

Recall that \( \operatorname {\mathsf{Part}}\alpha \) denotes the type \( \sum _{p: \mathsf{Prop}} (p \to \alpha ) \). For \( i : I \), we define the hypothesis on data \( t : \prod _{j : I} j \prec i \to \operatorname {\mathsf{Part}}A_j \) to be the proposition

\begin{align*} \operatorname {\mathsf{IH}}(i, t) = & \sum _{D : \prod _{j : I} \prod _{h : j \prec i} \operatorname {\mathsf{pr}}_1(t\ j\ h)} \prod _{j : I} \prod _{h : j \prec i} B\ j\ (\operatorname {\mathsf{pr}}_2(t\ j\ h)\ (D\ j\ h))\\ & \quad (k\ h’ \mapsto (\operatorname {\mathsf{pr}}_2(t\ k\ (\operatorname {\mathsf{trans}}(h’,h)))\ (D\ k\ (\operatorname {\mathsf{trans}}(h’,h))))) \end{align*}

Now we define \( K : \prod _{i : I} \operatorname {\mathsf{Part}}A_i \) by

\[ K = \operatorname {\mathsf{fix}}_{\operatorname {\mathsf{Part}}A_{(-)}} \left( i t \mapsto \left\langle \operatorname {\mathsf{IH}}(i, t), h \mapsto F_A\ i\ (j\ h' \mapsto (\operatorname {\mathsf{pr}}_2(t\ j\ h')\ (\operatorname {\mathsf{pr}}_1(h)\ j\ h')))\ \operatorname {\mathsf{pr}}_2(h) \right\rangle \right) \]

where \( \operatorname {\mathsf{fix}}_C \) is the fixed point function for \( \prec \) and induction motive \( C : I \to \mathsf{Type}_v \), with type

\[ \operatorname {\mathsf{fix}}_C : \left( \prod _{i : I} \left( \prod _{j : I} j \prec i \to C_j \right) \to C_i \right) \to \prod _{i : I} C_i \]

By definition of \( \operatorname {\mathsf{fix}} \), we obtain the equation

\[ K_i = \left\langle \operatorname {\mathsf{IH}}(i, j \_ \mapsto K_j), h \mapsto F_A\ i\ (j\ h' \mapsto (\operatorname {\mathsf{pr}}_2(K_j)\ (\operatorname {\mathsf{pr}}_1(h)\ j\ h')))\ \operatorname {\mathsf{pr}}_2(h) \right\rangle \]

Further, if \( h_1 : \operatorname {\mathsf{pr}}_1(K_i) \), we have the equation

\[ \operatorname {\mathsf{pr}}_2(K_i)\ h_1 = F_A\ i\ (j\ h' \mapsto (\operatorname {\mathsf{pr}}_2(K_j)\ (\operatorname {\mathsf{pr}}_1(h_2)\ j\ h')))\ \operatorname {\mathsf{pr}}_2(h_2) \]

where \( h_2 : \operatorname {\mathsf{IH}}(i, j \_ \mapsto K_j) \) is obtained by casting from \( h_1 \) using the previous equation; this equation is derived from the extensionality principle of \( \operatorname {\mathsf{Part}}\), which states that

\[ \prod _{x, y : \operatorname {\mathsf{Part}}\alpha } \left( \prod _{a : \alpha } (\exists h,\, a = \operatorname {\mathsf{pr}}_2(x)\ h) \leftrightarrow (\exists h,\, a = \operatorname {\mathsf{pr}}_2(y)\ h) \right) x = y \]

Using these two equations, we may now show directly by induction on \( i \) that \( D' : \prod _{i : I} \operatorname {\mathsf{pr}}_1(K_i) \). ¹ From this, we may define \( G : \prod _{i : I} A_i \) by \( G_i = \operatorname {\mathsf{pr}}_2(K_i)\ D'_i \). We may then easily obtain \( H : \prod _{i : I}\ B\ i\ G_i\ (j \_ \mapsto G_j) \) by appealing to \( F_B \) and the two equations above. The required equality also easily follows from the two given equations.

Theorem 6.3 inductive construction theorem

Let \( (F_A, F_B) \) be an inductive construction for \( (I, A, B) \). Then there are noncomputable functions

\[ G : \prod _{i : I} A_i;\quad H : \prod _{i : I} B\ i\ G_i\ (j\ \_ \mapsto G_j) \]

such that for each \( i : I \),

\[ G_i = F_A\ i\ (j\ \_ \mapsto G_j)\ (F_B\ i\ (j\ \_ \mapsto H_j)) \]

Proof ▶

Define

\[ C : \prod _{i : I} A_i \to \left(\prod _{j : I} j \prec i \to A_j\right) \to \mathsf{Prop} \]

by \( C\ i\ x\ d = \operatorname {\mathsf{Nonempty}}(B\ i\ x\ d) \). We then define the inductive construction \( (F_A', F_B') \) for \( (I, A, C) \) by

\[ F_A'\ i\ d\ h = F_A\ i\ d\ (j h' \mapsto \operatorname {\mathsf{some}}(h\ j\ h'));\quad F_B'\ i\ d\ h = \langle F_B\ i\ d\ (j h' \mapsto \operatorname {\mathsf{some}}(h\ j\ h')) \rangle \]

where \( \langle -\rangle \) is the constructor and \( \operatorname {\mathsf{some}} \) is the noncomputable destructor of \( \operatorname {\mathsf{Nonempty}} \). The result is then direct from proposition 6.2.