Dependencies

The inductive step for the main hypothesis is the function

given as follows. Given the hypotheses \( \alpha , M, H \), we use the definitions from definition 6.6 to obtain model data at level \( \alpha \) and coherent data below level \( \alpha \). The remaining proof obligations are handled by ??.

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

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

We define the main hypothesis

at \( \alpha \), given \( \mathsf{Motive}_\alpha \) and \( \prod _{\beta {\lt} \alpha } \mathsf{Motive}_\beta \), to be the type consisting of the following data.

• For \( \gamma {\lt} \beta \leq \alpha \), there is a map \( \mathsf{AllPerm}_\beta \to \mathsf{AllPerm}_\gamma \) that commutes with the coercions from \( \mathsf{AllPerm}_{(-)} \) to \( \mathsf{StrPerm}_{(-)} \).

• Let \( \beta , \gamma {\lt} \alpha \) be distinct with \( \gamma \) proper. Let \( t : \mathsf{Tang}_\beta \) and \( \rho : \mathsf{AllPerm}_\alpha \). Then

  \[ (\rho _\gamma )_\bot (f_{\beta ,\gamma }(t)) = f_{\beta ,\gamma }(\rho _\beta (t)) \]

• Suppose that \( (\rho (\beta ))_{\beta {\lt} \alpha } \) is a collection of allowable permutations such that whenever \( \beta , \gamma {\lt} \alpha \) are distinct, \( \gamma \) is proper, and \( t : \mathsf{Tang}_\gamma \), we have

  \[ (\rho (\gamma ))_\bot (f_{\beta ,\gamma }(t)) = f_{\beta ,\gamma }(\rho (\beta )(t)) \]

  Then there is an \( \alpha \)-allowable permutation \( \rho \) with \( \rho _\beta = \rho (\beta ) \) for each \( \beta {\lt} \alpha \).

• For any \( \beta {\lt} \alpha \),

  \[ U_\alpha (x)(\beta ) \subseteq \operatorname {\mathsf{ran}}U_\beta \]

• (extensionality) If \( \beta : \lambda \) is such that \( \beta {\lt} \alpha \), the map \( U_\alpha (-)(\beta ) : \mathsf{TSet}_\beta \to \operatorname {\mathsf{Set}}\mathsf{StrSet}_\beta \) is injective.

• If \( \beta : \lambda \) is such that \( \beta {\lt} \alpha \), for every \( x : \mathsf{TSet}_\beta \) there is some \( y : \mathsf{TSet}_\alpha \) such that \( U_\alpha (y)(\beta ) = \{ x \} \), and we write \( \operatorname {\mathsf{singleton}}_\alpha (x) \) for this object \( y \).

For a proper type index \( \alpha \), the main motive at \( \alpha \) is the type \( \mathsf{Motive}_\alpha \) consisting of model data at \( \alpha \), a position function for \( \mathsf{Tang}_\alpha \), and typed near-litters at \( \alpha \), such that if \( (x, S) \) is an \( \alpha \)-tangle and \( y \) is an atom or near-litter that occurs in the range of \( S_A \), then \( \iota (y) {\lt} \iota (x, S) \).

The inductive step for the main motive is the function

given as follows. Given the hypotheses \( \alpha , M, H \), we use definition 3.12 to construct model data at level \( \alpha \). Then, combine this with \( H \) to create an instance of coherent data below level \( \alpha \). ¹ By proposition 5.45, we conclude that \( \# \mathsf{Tang}_\alpha = \# \mu \), and so by proposition 3.15 there is a position function on \( \mathsf{Tang}_\alpha \) that respects the typed near-litters defined in definition 3.13. These data comprise the main motive at level \( \alpha \).

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

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

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

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

There are noncomputable functions

and

such that for each \( \alpha : \lambda \),