New Foundations is consistent

3 Constructing the types

In this section, we are trying to construct the type of tangled sets at level \( \alpha \). We assume model data, position functions for \( \mathsf{Tang}_\beta \), and typed near-litters for all types \( \beta {\lt} \alpha \).