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 [ConNF.Params] (α : ConNF.TypeIndex) : ConNF.TypeIndex → Type u

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

• nil: [inst : ConNF.Params] → {α : ConNF.TypeIndex} → α ↝ α
• cons: [inst : ConNF.Params] → {α β γ : ConNF.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 [ConNF.Params] {α β : ConNF.TypeIndex} (h : β < α) : α ↝ β

Equations

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

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

Typeclass for the ↘ notation.

• sderiv : X → γ < β → Y

class ConNF.Derivative [ConNF.Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : outParam ConNF.TypeIndex) (γ : ConNF.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 ⇘ ConNF.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 [ConNF.Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : outParam ConNF.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 ⇘. ConNF.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 [ConNF.Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : ConNF.TypeIndex) (γ : outParam ConNF.TypeIndex) : Type (max u_1 u_2)

Typeclass for the ↗ notation.

• scoderiv : X → γ < β → Y

class ConNF.Coderivative [ConNF.Params] (X : Type u_1) (Y : outParam (Type u_2)) (β : ConNF.TypeIndex) (γ : outParam ConNF.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 ⇗ ConNF.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 [ConNF.Params] {β γ : ConNF.TypeIndex} {X : Type u_1} {Y : Type u_2} [ConNF.Derivative X Y β γ] (x : X) (h : γ < β) : x ⇘ ConNF.Path.single h = x ↘ h

@[simp]

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

@[simp]

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

Downwards recursion along paths

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

Equations

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

def ConNF.Path.recSderiv [ConNF.Params] {α : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → α ↝ β → Sort u_1} (nil : motive α ConNF.Path.nil) (sderiv : (β γ : ConNF.TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β A → motive γ (A ↘ h)) {β : ConNF.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 [ConNF.Params] {α : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → α ↝ β → Sort u_1} (nil : motive α ConNF.Path.nil) (sderiv : (β γ : ConNF.TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β A → motive γ (A ↘ h)) : ConNF.Path.recSderiv nil sderiv ConNF.Path.nil = nil

@[simp]

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

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

def ConNF.Path.recSderivLe [ConNF.Params] {α : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → β ≤ α → Sort u_1} (nil : motive α ⋯) (sderiv : (β γ : ConNF.TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β ⋯ → motive γ ⋯) {β : ConNF.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 [ConNF.Params] {α : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → β ≤ α → Sort u_1} (nil : motive α ⋯) (sderiv : (β γ : ConNF.TypeIndex) → (A : α ↝ β) → (h : γ < β) → motive β ⋯ → motive γ ⋯) : ConNF.Path.recSderivLe nil sderiv ConNF.Path.nil = nil

@[simp]

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

def ConNF.Path.recSderivGlobal [ConNF.Params] {α : ConNF.TypeIndex} {motive : ConNF.TypeIndex → Sort u_1} (nil : motive α) (sderiv : (β γ : ConNF.TypeIndex) → α ↝ β → γ < β → motive β → motive γ) {β : ConNF.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 [ConNF.Params] {α : ConNF.TypeIndex} {motive : ConNF.TypeIndex → Sort u_1} (nil : motive α) (sderiv : (β γ : ConNF.TypeIndex) → α ↝ β → γ < β → motive β → motive γ) : ConNF.Path.recSderivGlobal nil sderiv ConNF.Path.nil = nil

@[simp]

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

Derivatives of paths

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

Equations

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

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

Equations

• ConNF.instBotDerivativePathBotTypeIndex = ConNF.BotDerivative.mk (fun (A : α ↝ β) (B : β ↝ ⊥) => A ⇘ B) ⋯

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

Equations

• ConNF.instCoderivativePath = ConNF.Coderivative.mk (fun (A : β ↝ γ) (B : α ↝ β) => B ⇘ A) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Upwards recursion along paths

inductive ConNF.RevPath [ConNF.Params] (α : ConNF.TypeIndex) : ConNF.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: [inst : ConNF.Params] → {α : ConNF.TypeIndex} → ConNF.RevPath α α
• cons: [inst : ConNF.Params] → {α β γ : ConNF.TypeIndex} → ConNF.RevPath α β → β < γ → ConNF.RevPath α γ

def ConNF.RevPath.rec' [ConNF.Params] {α : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → ConNF.RevPath α β → Sort u_1} (nil : motive α ConNF.RevPath.nil) (cons : {β γ : ConNF.TypeIndex} → (A : ConNF.RevPath α β) → (h : β < γ) → motive β A → motive γ (A.cons h)) {β : ConNF.TypeIndex} (A : ConNF.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 [ConNF.Params] {β γ : ConNF.TypeIndex} (h : γ < β) {α : ConNF.TypeIndex} : ConNF.RevPath β α → ConNF.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 [ConNF.Params] {α β : ConNF.TypeIndex} : α ↝ β → ConNF.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 [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.Path.nil.rev = ConNF.RevPath.nil

@[simp]

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

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

Equations

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

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

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

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

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

def ConNF.Path.recScoderiv' [ConNF.Params] {γ : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ ConNF.Path.nil) (scoderiv : (α β : ConNF.TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) {β : ConNF.TypeIndex} (A : ConNF.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 [ConNF.Params] {γ : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ ConNF.Path.nil) (scoderiv : (α β : ConNF.TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) : ConNF.Path.recScoderiv' nil scoderiv ConNF.RevPath.nil = nil

@[simp]

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

def ConNF.Path.recScoderiv [ConNF.Params] {γ : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ ConNF.Path.nil) (scoderiv : (α β : ConNF.TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) {β : ConNF.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 [ConNF.Params] {γ : ConNF.TypeIndex} {motive : (β : ConNF.TypeIndex) → β ↝ γ → Sort u_1} (nil : motive γ ConNF.Path.nil) (scoderiv : (α β : ConNF.TypeIndex) → (A : β ↝ γ) → (h : β < α) → motive β A → motive α (A ↗ h)) : ConNF.Path.recScoderiv nil scoderiv ConNF.Path.nil = nil

@[simp]

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

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

Cardinality bounds on paths

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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