Indices

In this file, we create instances for various facts about comparisons between type indices, and also define extended type indices.

Main declarations

• ConNF.ExtendedIndex: The type of extended type indices from a given base type index.

class ConNF.Level [ConNF.Params] : Type u

The current level of the structure we are building. This is registered as a class so that Lean can find it easily.

• α : ConNF.Λ

class ConNF.LtLevel [ConNF.Params] [ConNF.Level] (β : ConNF.TypeIndex) : Prop

The type index β is less than our current level. This is listed as a class so that Lean can find this hypothesis without having to include the type β < α in the goal state.

• elim : β < ↑ConNF.α

theorem ConNF.LtLevel.elim [ConNF.Params] [ConNF.Level] {β : ConNF.TypeIndex} [self : ConNF.LtLevel β] : β < ↑ConNF.α

instance ConNF.instLtLevelSomeΛOfSome [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [inst : ConNF.LtLevel (some β)] : ConNF.LtLevel ↑β

Equations

• ⋯ = inst

instance ConNF.instLtLevelBotTypeIndex [ConNF.Params] [ConNF.Level] : ConNF.LtLevel ⊥

Equations

• ⋯ = ⋯

class ConNF.LeLevel [ConNF.Params] [ConNF.Level] (β : ConNF.TypeIndex) : Prop

The type index β is at most our current level. This is listed as a class so that Lean can find this hypothesis without having to include the type β < α in the goal state.

• elim : β ≤ ↑ConNF.α

theorem ConNF.LeLevel.elim [ConNF.Params] [ConNF.Level] {β : ConNF.TypeIndex} [self : ConNF.LeLevel β] : β ≤ ↑ConNF.α

instance ConNF.instLeLevelSomeΛα [ConNF.Params] [ConNF.Level] : ConNF.LeLevel ↑ConNF.α

Equations

• ⋯ = ⋯

instance ConNF.instLeLevelOfLtLevel [ConNF.Params] [ConNF.Level] {β : ConNF.TypeIndex} [ConNF.LtLevel β] : ConNF.LeLevel β

Equations

• ⋯ = ⋯

instance ConNF.instLeLevelSomeΛOfSome [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [inst : ConNF.LeLevel (some β)] : ConNF.LeLevel ↑β

Equations

• ⋯ = inst

instance ConNF.instQuiverTypeIndex [ConNF.Params] : Quiver ConNF.TypeIndex

We define the type of paths from certain types to lower types as inhabitants of this quiver.

Equations

• ConNF.instQuiverTypeIndex = { Hom := fun (x x_1 : ConNF.TypeIndex) => x > x_1 }

def ConNF.ExtendedIndex [ConNF.Params] (α : ConNF.TypeIndex) : Type u

A (finite) path from the type α to the base type. This is a way that we can perceive extensionality, iteratively descending to lower types in the hierarchy until we reach the base type. As Λ is well-ordered, there are no infinite descending paths.

Equations

• ConNF.ExtendedIndex α = Quiver.Path α ⊥

theorem ConNF.le_of_path [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} : Quiver.Path α β → β ≤ α

If there is a path between α and β, we must have β ≤ α. The case β = α can occur with the nil path.

theorem ConNF.path_eq_nil [ConNF.Params] {α : ConNF.TypeIndex} (p : Quiver.Path α α) : p = Quiver.Path.nil

Paths from a type index to itself must be the nil path.

theorem ConNF.ExtendedIndex.length_ne_zero [ConNF.Params] {α : ConNF.Λ} (A : ConNF.ExtendedIndex ↑α) : Quiver.Path.length A ≠ 0

Extended indices cannot be the nil path.

@[simp]

theorem ConNF.mk_extendedIndex [ConNF.Params] (α : ConNF.TypeIndex) : Cardinal.mk (ConNF.ExtendedIndex α) ≤ Cardinal.mk ConNF.Λ

There are at most Λ α-extended type indices.

instance ConNF.ltToHom [ConNF.Params] (β : ConNF.Λ) (γ : ConNF.Λ) : Coe (β < γ) (↑γ ⟶ ↑β)

If β < γ, we have a path directly between the two types in the opposite order. Note that the ⟶ symbol (long right arrow) is not the normal → (right arrow), even though monospace fonts often display them similarly.

Equations

• ConNF.ltToHom β γ = { coe := ⋯ }

instance ConNF.instInhabitedExtendedIndex [ConNF.Params] (α : ConNF.TypeIndex) : Inhabited (ConNF.ExtendedIndex α)

Equations

• ConNF.instInhabitedExtendedIndex x = match x with | none => { default := Quiver.Path.nil } | some α => { default := Quiver.Hom.toPath ⋯ }

theorem ConNF.mk_extendedIndex_ne_zero [ConNF.Params] (α : ConNF.TypeIndex) : Cardinal.mk (ConNF.ExtendedIndex α) ≠ 0

There exists an α-extended type index. -