- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
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 \). 1 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 \),