Position functions

In this file, we define what it means for a type to have a position function. Various well-foundedness constraints in our model are enforced by position functions, which are injections into μ. If we can define a relation on a type with a position function such that r x y only if pos x < pos y, then r must be well-founded; this situation will occur frequently.

class ConNF.Position [ConNF.Params] (X : Type u_1) : Type (max u u_1)

A position function on a type X is an injection from X into μ.

• pos : X ↪ ConNF.μ

theorem ConNF.card_le_of_position [ConNF.Params] {X : Type u} [ConNF.Position X] : Cardinal.mk X ≤ Cardinal.mk ConNF.μ

If X has a position function, then the cardinality of X must be at most #μ.

def ConNF.pos_induction [ConNF.Params] {X : Type u_1} [ConNF.Position X] {C : X → Prop} (x : X) (h : ∀ (x : X), (∀ (y : X), ConNF.pos y < ConNF.pos x → C y) → C x) : C x

An induction (or recursion) principle for any type with a position function. C is the motive of the recursion. If we can produce C x given C y for all y with position lower than x, we can produce C x for all x.

Equations

• ⋯ = ⋯