Documentation

ConNF.Base.TypeIndex

Type indices #

We are going to use the inhabitants of Λ to enumerate the type levels in the final model we will construct. However, in order to run the model construction, we need to first build an auxiliary layer of the model below all of the ones that will appear in the final model. This extra level is sometimes called "type -1".

The easiest way for us to introduce such an extra index is to formally adjoin a new symbol to Λ, called ⊥, which will play the role of -1. This new type, with ⊥ adjoined, is called the type of type indices. When a distinction between Λ and the type indices is important, we call the former the type of proper type indices.

It is important to take note of the difference between a type-in-Lean and a type-in-the-model; hopefully it should be clear from context which is meant.

source
@[reducible]
def ConNF.TypeIndex [ConNF.Params] :
Type u

Either the base type or a proper type index (an inhabitant of Λ). The base type index is written ⊥.

Equations
Instances For
    source
    instance ConNF.instWellFoundedRelationTypeIndex [ConNF.Params] :
    WellFoundedRelation ConNF.TypeIndex

    Allows us to use termination_by clauses with TypeIndex.

    Equations
    • ConNF.instWellFoundedRelationTypeIndex = { rel := fun (x1 x2 : ConNF.TypeIndex) => x1 < x2, wf := ⋯ }
    source
    @[simp]
    theorem ConNF.TypeIndex.type [ConNF.Params] :
    (Ordinal.type fun (x1 x2 : ConNF.TypeIndex) => x1 < x2) = Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2

    Because the order type of Λ is infinite, the order type of the type indices is the same as the order type of Λ.

    source
    @[simp]
    theorem ConNF.TypeIndex.card [ConNF.Params] :
    Cardinal.mk ConNF.TypeIndex = Cardinal.mk ConNF.Λ

    The type indices and the proper type indices have the same cardinality.

    source
    theorem ConNF.Λ_card_Iio_lt [ConNF.Params] (α : ConNF.Λ) :
    Cardinal.mk ↑{β : ConNF.Λ | β < α} < (Cardinal.mk ConNF.μ).ord.cof

    Initial segments of Λ (excluding the endpoint) have cardinalities less than the cofinality of μ. This means that maps from such initial segments into μ cannot be cofinal.

    source
    theorem ConNF.Λ_card_Iic_lt [ConNF.Params] (α : ConNF.Λ) :
    Cardinal.mk ↑{β : ConNF.Λ | β ≤ α} < (Cardinal.mk ConNF.μ).ord.cof

    Initial segments of Λ (including the endpoint) have cardinalities less than the cofinality of μ.

    source
    theorem ConNF.TypeIndex.card_Iio_lt [ConNF.Params] (α : ConNF.TypeIndex) :
    Cardinal.mk ↑{β : ConNF.TypeIndex | β < α} < (Cardinal.mk ConNF.μ).ord.cof

    Initial segments of the type indices (including the endpoint) have cardinalities less than the cofinality of μ.

    source
    theorem ConNF.TypeIndex.card_Iic_lt [ConNF.Params] (α : ConNF.TypeIndex) :
    Cardinal.mk ↑{β : ConNF.TypeIndex | β ≤ α} < (Cardinal.mk ConNF.μ).ord.cof

    Initial segments of the type indices (including the endpoint) have cardinalities less than the cofinality of μ.