Paths of type indices

In this file, we define the notion of a path, and the derivative and coderivative operations.

Main declarations

• ConNF.Path: A path of type indices.
• ConNF.Path.recSderiv, ConNF.Path.recSderivLe, ConNF.Path.recSderivGlobal: Downwards induction principles for paths.
• ConNF.Path.recScoderiv: An upwards induction principle for paths.

inductive ConNF.Path [Params] (α : TypeIndex) : TypeIndex → Type u

A path of type indices starting at α and ending at β is a finite sequence of type indices α > ... > β.

• nil [Params] {α : TypeIndex} : α ↝ α
• cons [Params] {α β γ : TypeIndex} : α ↝ β → γ < β → α ↝ γ

def ConNF.«term_↝_» : Lean.TrailingParserDescr

A path of type indices starting at α and ending at β is a finite sequence of type indices α > ... > β.

Equations

• ConNF.«term_↝_» = Lean.ParserDescr.trailingNode `ConNF.«term_↝_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↝ ") (Lean.ParserDescr.cat `term 71))

def ConNF.Path.single [Params] {α β : TypeIndex} (h : β < α) : α ↝ β

Equations

• ConNF.Path.single h = ConNF.Path.nil.cons h

class ConNF.SingleDerivative [Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : outParam TypeIndex) (γ : TypeIndex) : Type (max u_1 u_2)

Typeclass for the ↘ notation.

• sderiv : X → γ < β → Y

class ConNF.Derivative [Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : outParam TypeIndex) (γ : TypeIndex) extends ConNF.SingleDerivative X Y β γ : Type (max (max u u_1) u_2)

Typeclass for the ⇘ notation.

• sderiv : X → γ < β → Y
• deriv : X → β ↝ γ → Y
• deriv_single (x : X) (h : γ < β) : x ⇘ Path.single h = x ↘ h

class ConNF.BotSingleDerivative (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ↘. notation.

• botSderiv : X → Y

class ConNF.BotDerivative [Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : outParam TypeIndex) extends ConNF.BotSingleDerivative X Y : Type (max (max u u_1) u_2)

Typeclass for the ⇘. notation.

• botSderiv : X → Y
• botDeriv : X → β ↝ ⊥ → Y
• botDeriv_single (x : X) (h : ⊥ < β) : x ⇘. Path.single h = x ↘.

  We often need to do case analysis on β to show that it's a proper type index here. This case check doesn't need to be done in most actual use cases of the notation.

class ConNF.SingleCoderivative [Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : TypeIndex) (γ : outParam TypeIndex) : Type (max u_1 u_2)

Typeclass for the ↗ notation.

• scoderiv : X → γ < β → Y

class ConNF.Coderivative [Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : TypeIndex) (γ : outParam TypeIndex) extends ConNF.SingleCoderivative X Y β γ : Type (max (max u u_1) u_2)

Typeclass for the ⇗ notation.

• scoderiv : X → γ < β → Y
• coderiv : X → β ↝ γ → Y
• coderiv_single (x : X) (h : γ < β) : x ⇗ Path.single h = x ↗ h

def ConNF.«term_↘_» : Lean.TrailingParserDescr

Equations

• ConNF.«term_↘_» = Lean.ParserDescr.trailingNode `ConNF.«term_↘_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↘ ") (Lean.ParserDescr.cat `term 76))

def ConNF.«term_⇘_» : Lean.TrailingParserDescr

Equations

• ConNF.«term_⇘_» = Lean.ParserDescr.trailingNode `ConNF.«term_⇘_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇘ ") (Lean.ParserDescr.cat `term 76))

def ConNF.«term_↘.» : Lean.TrailingParserDescr

Equations

• ConNF.«term_↘.» = Lean.ParserDescr.trailingNode `ConNF.«term_↘.» 75 75 (Lean.ParserDescr.symbol " ↘.")

def ConNF.«term_⇘._» : Lean.TrailingParserDescr

Equations

• ConNF.«term_⇘._» = Lean.ParserDescr.trailingNode `ConNF.«term_⇘._» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇘. ") (Lean.ParserDescr.cat `term 76))

def ConNF.«term_↗_» : Lean.TrailingParserDescr

Equations

• ConNF.«term_↗_» = Lean.ParserDescr.trailingNode `ConNF.«term_↗_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↗ ") (Lean.ParserDescr.cat `term 76))

def ConNF.«term_⇗_» : Lean.TrailingParserDescr

Equations

• ConNF.«term_⇗_» = Lean.ParserDescr.trailingNode `ConNF.«term_⇗_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇗ ") (Lean.ParserDescr.cat `term 76))

@[simp]

theorem ConNF.deriv_single [Params] {β γ : TypeIndex} {X : Type u_1} {Y : Type u_2} [Derivative X Y β γ] (x : X) (h : γ < β) : x ⇘ Path.single h = x ↘ h

@[simp]

theorem ConNF.coderiv_single [Params] {β γ : TypeIndex} {X : Type u_1} {Y : Type u_2} [Coderivative X Y β γ] (x : X) (h : γ < β) : x ⇗ Path.single h = x ↗ h

@[simp]

theorem ConNF.botDeriv_single [Params] {β : TypeIndex} {X : Type u_1} {Y : Type u_2} [BotDerivative X Y β] (x : X) (h : ⊥ < β) : x ⇘. Path.single h = x ↘.

Downwards recursion along paths

instance ConNF.instSingleDerivativePath [Params] {α β γ : TypeIndex} : SingleDerivative (α ↝ β) (α ↝ γ) β γ

Equations

• ConNF.instSingleDerivativePath = { sderiv := ConNF.Path.cons }

def ConNF.Path.recSderiv [Params] {α : TypeIndex} {motive : (β : TypeIndex) → α ↝ β → Sort u_1} (nil : motive α nil) (sderiv : (β γ : TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β A → motive γ (A ↘ h)) {β : TypeIndex} (A : α ↝ β) : motive β A

The downwards recursion principle for paths.

Equations

• ConNF.Path.recSderiv nil sderiv ConNF.Path.nil = nil
• ConNF.Path.recSderiv nil sderiv (A.cons h) = sderiv β x✝ A h (ConNF.Path.recSderiv nil sderiv A)

@[simp]

theorem ConNF.Path.recSderiv_nil [Params] {α : TypeIndex} {motive : (β : TypeIndex) → α ↝ β → Sort u_1} (nil : motive α nil) (sderiv : (β γ : TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β A → motive γ (A ↘ h)) : recSderiv nil sderiv ConNF.Path.nil = nil

@[simp]

theorem ConNF.Path.recSderiv_sderiv [Params] {α : TypeIndex} {motive : (β : TypeIndex) → α ↝ β → Sort u_1} (nil : motive α nil) (sderiv : (β γ : TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β A → motive γ (A ↘ h)) {β γ : TypeIndex} (A : α ↝ β) (h : γ < β) : recSderiv nil sderiv (A ↘ h) = sderiv β γ A h (recSderiv nil sderiv A)

theorem ConNF.Path.le [Params] {α β : TypeIndex} (A : α ↝ β) : β ≤ α

def ConNF.Path.recSderivLe [Params] {α : TypeIndex} {motive : (β : TypeIndex) → β ≤ α → Sort u_1} (nil : motive α ⋯) (sderiv : (β γ : TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β ⋯ → motive γ ⋯) {β : TypeIndex} (A : α ↝ β) : motive β ⋯

The downwards recursion principle for paths, specialised to the case where the motive at β only depends on the fact that β ≤ α.

Equations

• ConNF.Path.recSderivLe nil sderiv = ConNF.Path.recSderiv nil sderiv

@[simp]

theorem ConNF.Path.recSderivLe_nil [Params] {α : TypeIndex} {motive : (β : TypeIndex) → β ≤ α → Sort u_1} (nil : motive α ⋯) (sderiv : (β γ : TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β ⋯ → motive γ ⋯) : recSderivLe nil sderiv ConNF.Path.nil = nil

@[simp]

theorem ConNF.Path.recSderivLe_sderiv [Params] {α : TypeIndex} {motive : (β : TypeIndex) → β ≤ α → Sort u_1} (nil : motive α ⋯) (sderiv : (β γ : TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β ⋯ → motive γ ⋯) {β γ : TypeIndex} (A : α ↝ β) (h : γ < β) : recSderivLe nil sderiv (A ↘ h) = sderiv β γ A h (recSderiv nil sderiv A)

def ConNF.Path.recSderivGlobal [Params] {α : TypeIndex} {motive : TypeIndex → Sort u_1} (nil : motive α) (sderiv : (β γ : TypeIndex) → α ↝ β → γ < β → motive β → motive γ) {β : TypeIndex} : α ↝ β → motive β

The downwards recursion principle for paths, specialised to the case where the motive is not dependent on the relation of β to α.

Equations

• ConNF.Path.recSderivGlobal nil sderiv = ConNF.Path.recSderiv nil sderiv

@[simp]

theorem ConNF.Path.recSderivGlobal_nil [Params] {α : TypeIndex} {motive : TypeIndex → Sort u_1} (nil : motive α) (sderiv : (β γ : TypeIndex) → α ↝ β → γ < β → motive β → motive γ) : recSderivGlobal nil sderiv ConNF.Path.nil = nil

@[simp]

theorem ConNF.Path.recSderivGlobal_sderiv [Params] {α : TypeIndex} {motive : TypeIndex → Sort u_1} (nil : motive α) (sderiv : (β γ : TypeIndex) → α ↝ β → γ < β → motive β → motive γ) {β γ : TypeIndex} (A : α ↝ β) (h : γ < β) : recSderivGlobal nil sderiv (A ↘ h) = sderiv β γ A h (recSderiv nil sderiv A)

Derivatives of paths

instance ConNF.instDerivativePath [Params] {α β γ : TypeIndex} : Derivative (α ↝ β) (α ↝ γ) β γ

Equations

• One or more equations did not get rendered due to their size.

instance ConNF.instBotDerivativePathBotTypeIndex [Params] {α β : TypeIndex} : BotDerivative (α ↝ β) (α ↝ ⊥) β

Equations

• One or more equations did not get rendered due to their size.

instance ConNF.instCoderivativePath [Params] {α β γ : TypeIndex} : Coderivative (β ↝ γ) (α ↝ γ) α β

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConNF.Path.deriv_nil [Params] {α β : TypeIndex} (A : α ↝ β) : A ⇘ nil = A

@[simp]

theorem ConNF.Path.deriv_sderiv [Params] {α β γ δ : TypeIndex} (A : α ↝ β) (B : β ↝ γ) (h : δ < γ) : A ⇘ (B ↘ h) = A ⇘ B ↘ h

@[simp]

theorem ConNF.Path.nil_deriv [Params] {α β : TypeIndex} (A : α ↝ β) : nil ⇘ A = A

@[simp]

theorem ConNF.Path.deriv_sderivBot [Params] {α β γ : TypeIndex} (A : α ↝ β) (B : β ↝ γ) : A ⇘ (B ↘.) = A ⇘ B ↘.

@[simp]

theorem ConNF.Path.botSderiv_bot_eq [Params] {α : TypeIndex} (A : α ↝ ⊥) : A ↘. = A

@[simp]

theorem ConNF.Path.botSderiv_coe_eq [Params] {α : TypeIndex} {β : Λ} (A : α ↝ ↑β) : A ↘ ⋯ = A ↘.

@[simp]

theorem ConNF.Path.deriv_assoc [Params] {α β γ δ : TypeIndex} (A : α ↝ β) (B : β ↝ γ) (C : γ ↝ δ) : A ⇘ (B ⇘ C) = A ⇘ B ⇘ C

@[simp]

theorem ConNF.Path.deriv_sderiv_assoc [Params] {α β γ δ : TypeIndex} (A : α ↝ β) (B : β ↝ γ) (h : δ < γ) : A ⇘ (B ↘ h) = A ⇘ B ↘ h

@[simp]

theorem ConNF.Path.deriv_scoderiv [Params] {α β γ δ : TypeIndex} (A : α ↝ β) (B : γ ↝ δ) (h : γ < β) : A ⇘ (B ↗ h) = A ↘ h ⇘ B

@[simp]

theorem ConNF.Path.botDeriv_scoderiv [Params] {α β γ : TypeIndex} (A : α ↝ β) (B : γ ↝ ⊥) (h : γ < β) : A ⇘. (B ↗ h) = A ↘ h ⇘. B

theorem ConNF.Path.coderiv_eq_deriv [Params] {α β γ : TypeIndex} (A : α ↝ β) (B : β ↝ γ) : B ⇗ A = A ⇘ B

theorem ConNF.Path.coderiv_deriv [Params] {α β γ δ : TypeIndex} (A : β ↝ γ) (h₁ : β < α) (h₂ : δ < γ) : A ↗ h₁ ↘ h₂ = A ↘ h₂ ↗ h₁

theorem ConNF.Path.coderiv_deriv' [Params] {α β γ δ : TypeIndex} (A : β ↝ γ) (h : β < α) (B : γ ↝ δ) : A ↗ h ⇘ B = A ⇘ B ↗ h

theorem ConNF.Path.eq_nil [Params] {β : TypeIndex} (A : β ↝ β) : A = nil

theorem ConNF.Path.sderiv_index_injective [Params] {α β γ δ : TypeIndex} {A : α ↝ β} {B : α ↝ γ} {hδβ : δ < β} {hδγ : δ < γ} (h : A ↘ hδβ = B ↘ hδγ) : β = γ

theorem ConNF.Path.sderivBot_index_injective [Params] {α : TypeIndex} {β γ : Λ} {A : α ↝ ↑β} {B : α ↝ ↑γ} (h : A ↘. = B ↘.) : β = γ

theorem ConNF.Path.sderiv_path_injective [Params] {α β γ : TypeIndex} {A B : α ↝ β} {hγ : γ < β} (h : A ↘ hγ = B ↘ hγ) : A = B

theorem ConNF.Path.sderivBot_path_injective [Params] {α : TypeIndex} {β : Λ} {A B : α ↝ ↑β} (h : A ↘. = B ↘.) : A = B

theorem ConNF.Path.deriv_left_injective [Params] {α β γ : TypeIndex} {A B : α ↝ β} {C : β ↝ γ} (h : A ⇘ C = B ⇘ C) : A = B

theorem ConNF.Path.deriv_right_injective [Params] {α β γ : TypeIndex} {A : α ↝ β} {B C : β ↝ γ} (h : A ⇘ B = A ⇘ C) : B = C

@[simp]

theorem ConNF.Path.sderiv_left_inj [Params] {α β γ : TypeIndex} {A B : α ↝ β} {h : γ < β} : A ↘ h = B ↘ h ↔ A = B

@[simp]

theorem ConNF.Path.deriv_left_inj [Params] {α β γ : TypeIndex} {A B : α ↝ β} {C : β ↝ γ} : A ⇘ C = B ⇘ C ↔ A = B

@[simp]

theorem ConNF.Path.deriv_right_inj [Params] {α β γ : TypeIndex} {A : α ↝ β} {B C : β ↝ γ} : A ⇘ B = A ⇘ C ↔ B = C

@[simp]

theorem ConNF.Path.scoderiv_left_inj [Params] {α β γ : TypeIndex} {A B : β ↝ γ} {h : β < α} : A ↗ h = B ↗ h ↔ A = B

@[simp]

theorem ConNF.Path.coderiv_left_inj [Params] {α β γ : TypeIndex} {A B : β ↝ γ} {C : α ↝ β} : A ⇗ C = B ⇗ C ↔ A = B

@[simp]

theorem ConNF.Path.coderiv_right_inj [Params] {α β γ : TypeIndex} {A : β ↝ γ} {B C : α ↝ β} : A ⇗ B = A ⇗ C ↔ B = C

Upwards recursion along paths

inductive ConNF.RevPath [Params] (α : TypeIndex) : TypeIndex → Type u

The same as Path, but the components of this path point "upwards" instead of "downwards". This type is only used for proving revScoderiv, and should be considered an implementation detail.

• nil [Params] {α : TypeIndex} : RevPath α α
• cons [Params] {α β γ : TypeIndex} : RevPath α β → β < γ → RevPath α γ

def ConNF.RevPath.rec' [Params] {α : TypeIndex} {motive : (β : TypeIndex) → RevPath α β → Sort u_1} (nil : motive α nil) (cons : {β γ : TypeIndex} → (A : RevPath α β) → (h : β < γ) → motive β A → motive γ (A.cons h)) {β : TypeIndex} (A : RevPath α β) : motive β A

A computable statement of the recursion principle for RevPath. This needs to be written due to a current limitation in the Lean 4 kernel: it cannot generate code for the .rec functions.

Equations

• ConNF.RevPath.rec' nil cons ConNF.RevPath.nil = nil
• ConNF.RevPath.rec' nil cons (A.cons h) = cons A h (ConNF.RevPath.rec' nil (fun {β γ : ConNF.TypeIndex} => cons) A)

def ConNF.RevPath.snoc [Params] {β γ : TypeIndex} (h : γ < β) {α : TypeIndex} : RevPath β α → RevPath γ α

Equations

• ConNF.RevPath.snoc h ConNF.RevPath.nil = ConNF.RevPath.nil.cons h
• ConNF.RevPath.snoc h (A.cons h_1) = (ConNF.RevPath.snoc h A).cons h_1

def ConNF.Path.rev [Params] {α β : TypeIndex} : α ↝ β → RevPath β α

Equations

• A.rev = ConNF.Path.recSderiv ConNF.RevPath.nil (fun (x x_1 : ConNF.TypeIndex) (x_2 : α ↝ x) (h : x_1 < x) => ConNF.RevPath.snoc h) A

@[simp]

theorem ConNF.Path.rev_nil [Params] {α : TypeIndex} : nil.rev = RevPath.nil

@[simp]

theorem ConNF.Path.rev_sderiv [Params] {α β γ : TypeIndex} (A : α ↝ β) (h : γ < β) : (A ↘ h).rev = RevPath.snoc h A.rev

def ConNF.RevPath.rev [Params] {β α : TypeIndex} : RevPath β α → α ↝ β

Equations

• ConNF.RevPath.nil.rev = ConNF.Path.nil
• (A.cons h).rev = A.rev ↗ h

theorem ConNF.Path.sderiv_rev [Params] {α β γ : TypeIndex} (A : α ↝ β) (h : γ < β) : (A ↘ h).rev = RevPath.snoc h A.rev

theorem ConNF.Path.scoderiv_rev [Params] {α β γ : TypeIndex} (A : β ↝ γ) (h : β < α) : (A ↗ h).rev = A.rev.cons h

theorem ConNF.RevPath.snoc_rev [Params] {α β γ : TypeIndex} (A : RevPath β α) (h : γ < β) : (snoc h A).rev = A.rev ↘ h

theorem ConNF.Path.rev_rev [Params] {α β : TypeIndex} (A : α ↝ β) : A.rev.rev = A

def ConNF.Path.recScoderiv' [Params] {γ : TypeIndex} {motive : (β : TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ nil) (scoderiv : (α β : TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) {β : TypeIndex} (A : RevPath γ β) : motive β A.rev

Equations

• ConNF.Path.recScoderiv' nil scoderiv A = ConNF.RevPath.rec' nil (fun {β γ_1 : ConNF.TypeIndex} (A : ConNF.RevPath γ β) => scoderiv γ_1 β A.rev) A

@[simp]

theorem ConNF.Path.recScoderiv'_nil [Params] {γ : TypeIndex} {motive : (β : TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ nil) (scoderiv : (α β : TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) : recScoderiv' nil scoderiv RevPath.nil = nil

@[simp]

theorem ConNF.Path.recScoderiv'_cons [Params] {α β γ : TypeIndex} {motive : (β : TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ nil) (scoderiv : (α β : TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) (A : RevPath γ β) (h : β < α) : recScoderiv' nil scoderiv (A.cons h) = scoderiv α β A.rev h (recScoderiv' nil scoderiv A)

def ConNF.Path.recScoderiv [Params] {γ : TypeIndex} {motive : (β : TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ nil) (scoderiv : (α β : TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) {β : TypeIndex} (A : β ↝ γ) : motive β A

The upwards recursion principle for paths. The scoderiv computation rule recScoderiv_scoderiv is not a definitional equality.

Equations

• ConNF.Path.recScoderiv nil scoderiv A = cast ⋯ (ConNF.Path.recScoderiv' nil scoderiv A.rev)

@[simp]

theorem ConNF.Path.recScoderiv_nil [Params] {γ : TypeIndex} {motive : (β : TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ nil) (scoderiv : (α β : TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) : recScoderiv nil scoderiv ConNF.Path.nil = nil

@[simp]

theorem ConNF.Path.recScoderiv_scoderiv [Params] {γ : TypeIndex} {motive : (β : TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ nil) (scoderiv : (α β : TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) {α β : TypeIndex} (A : β ↝ γ) (h : β < α) : recScoderiv nil scoderiv (A ↗ h) = scoderiv α β A h (recScoderiv nil scoderiv A)

theorem ConNF.Path.scoderiv_index_injective [Params] {α β γ δ : TypeIndex} {A : β ↝ δ} {B : γ ↝ δ} {hβα : β < α} {hγα : γ < α} (h : A ↗ hβα = B ↗ hγα) : β = γ

Cardinality bounds on paths

def ConNF.Path.toList [Params] {α β : TypeIndex} : α ↝ β → List ↑{β : TypeIndex | β < α}

Equations

• A.toList = ConNF.Path.recSderiv [] (fun (_β γ : ConNF.TypeIndex) (A : α ↝ _β) (h : γ < _β) (ih : List ↑{β : ConNF.TypeIndex | β < α}) => ⟨γ, ⋯⟩ :: ih) A

@[simp]

theorem ConNF.Path.toList_nil [Params] {α : TypeIndex} : nil.toList = []

@[simp]

theorem ConNF.Path.toList_sderiv [Params] {α β γ : TypeIndex} (A : α ↝ β) (h : γ < β) : (A ↘ h).toList = ⟨γ, ⋯⟩ :: A.toList

@[simp]

theorem ConNF.Path.eq_of_toList_eq [Params] {α β γ : TypeIndex} (A : α ↝ β) (B : α ↝ γ) : A.toList = B.toList → β = γ

theorem ConNF.Path.toList_injective [Params] (α β : TypeIndex) : Function.Injective toList

theorem ConNF.card_path_lt [Params] (α β : TypeIndex) : Cardinal.mk (α ↝ β) < (Cardinal.mk μ).ord.cof

theorem ConNF.card_path_lt' [Params] (α β : TypeIndex) : Cardinal.mk (α ↝ β) < Cardinal.mk μ

theorem ConNF.card_path_ne_zero [Params] (α : TypeIndex) : Cardinal.mk (α ↝ ⊥) ≠ 0

theorem ConNF.card_path_any_lt_Λ [Params] (α : TypeIndex) : Cardinal.mk ((β : Λ) × α ↝ ↑β) < (Cardinal.mk μ).ord.cof

theorem ConNF.card_path_any_lt [Params] (α : TypeIndex) : Cardinal.mk ((β : TypeIndex) × α ↝ β) < (Cardinal.mk μ).ord.cof