Levels

In this file, we provide a typeclass Level that stores the current type level of the construction.

Main declarations

• ConNF.Level: The current level.
• ConNF.LtLevel: A type index less than the current level.
• ConNF.LeLevel: A type index less than or equal to the current level.

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

• α : ConNF.Λ

  The current level of the construction.

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

• elim : β < ↑ConNF.α

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

• elim : β ≤ ↑ConNF.α

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

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

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