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 [Params] : Type u

• α : Λ

  The current level of the construction.

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

• elim : β < ↑α

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

• elim : β ≤ ↑α

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

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

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