def ConNF.constructionIH [ConNF.Params] (α : ConNF.Λ) : ConNF.MainInduction.IH α

Equations

• ConNF.constructionIH α = (ConNF.MainInduction.buildCumul α).ih α ⋯

theorem ConNF.buildCumul_spec [ConNF.Params] (α : ConNF.Λ) : ConNF.MainInduction.buildCumul α = ConNF.MainInduction.buildCumulStep α fun (β : ConNF.Λ) (x : β < α) => ConNF.MainInduction.buildCumul β

theorem ConNF.buildCumul_apply_eq [ConNF.Params] (α : ConNF.Λ) (β : ConNF.Λ) (hβ : β ≤ α) : (ConNF.MainInduction.buildCumul α).ih β hβ = (ConNF.MainInduction.buildCumul β).ih β ⋯

theorem ConNF.constructionIHProp [ConNF.Params] (α : ConNF.Λ) : ConNF.MainInduction.IHProp α fun (γ : ConNF.Λ) (x : γ ≤ α) => ConNF.constructionIH γ

theorem ConNF.constructionIH_eq [ConNF.Params] (α : ConNF.Λ) : ConNF.constructionIH α = ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯

instance ConNF.modelData [ConNF.Params] (α : ConNF.Λ) : ConNF.ModelData ↑α

Equations

• ConNF.modelData α = (ConNF.constructionIH α).modelData

instance ConNF.positionedTangles [ConNF.Params] (α : ConNF.Λ) : ConNF.PositionedTangles ↑α

Equations

• ConNF.positionedTangles α = (ConNF.constructionIH α).positionedTangles

instance ConNF.typedObjects [ConNF.Params] (α : ConNF.Λ) : ConNF.TypedObjects α

Equations

• ConNF.typedObjects α = (ConNF.constructionIH α).typedObjects

instance ConNF.positionedObjects [ConNF.Params] (α : ConNF.Λ) : ConNF.PositionedObjects α

Equations

• ⋯ = ⋯

instance ConNF.instModelData [ConNF.Params] (β : ConNF.TypeIndex) : ConNF.ModelData β

Equations

• ConNF.instModelData x = match x with | none => ConNF.Bot.modelData | some β => inferInstance

instance ConNF.instPositionedTangles [ConNF.Params] (β : ConNF.TypeIndex) : ConNF.PositionedTangles β

Equations

• ConNF.instPositionedTangles x = match x with | none => ConNF.Bot.positionedTangles | some β => inferInstance

instance ConNF.instModelDataLt [ConNF.Params] [ConNF.Level] : ConNF.ModelDataLt

Equations

• ConNF.instModelDataLt = { data := fun (x : ConNF.Λ) (x_1 : ConNF.LtLevel ↑x) => inferInstance }

instance ConNF.instPositionedTanglesLt [ConNF.Params] [ConNF.Level] : ConNF.PositionedTanglesLt

Equations

• ConNF.instPositionedTanglesLt = { data := fun (x : ConNF.Λ) (x_1 : ConNF.LtLevel ↑x) => inferInstance }

instance ConNF.instTypedObjectsLt [ConNF.Params] [ConNF.Level] : ConNF.TypedObjectsLt

Equations

• ConNF.instTypedObjectsLt x✝ = inferInstance

instance ConNF.instPositionedObjectsLt [ConNF.Params] [ConNF.Level] : ConNF.PositionedObjectsLt

Equations

• ⋯ = ⋯

theorem ConNF.modelData_eq [ConNF.Params] (α : ConNF.Λ) : ConNF.modelData α = (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).modelData

theorem ConNF.positionedTangles_heq [ConNF.Params] (α : ConNF.Λ) : HEq (ConNF.positionedTangles α) (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).positionedTangles

theorem ConNF.typedObjects_heq [ConNF.Params] (α : ConNF.Λ) : HEq (ConNF.typedObjects α) (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).typedObjects

theorem ConNF.positionedObjects_heq [ConNF.Params] (α : ConNF.Λ) : HEq ⋯ ⋯

def ConNF.tSetEquiv [ConNF.Params] (α : ConNF.Λ) : ConNF.TSet ↑α ≃ (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).TSet

Equations

• ConNF.tSetEquiv α = Equiv.cast ⋯

def ConNF.tangleEquiv [ConNF.Params] (α : ConNF.Λ) : ConNF.Tangle ↑α ≃ (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).Tangle

Equations

• ConNF.tangleEquiv α = Equiv.cast ⋯

def ConNF.allowableEquiv [ConNF.Params] (α : ConNF.Λ) : ConNF.Allowable ↑α ≃ (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).Allowable

Equations

• ConNF.allowableEquiv α = Equiv.cast ⋯

theorem ConNF.allowableEquiv_one [ConNF.Params] (α : ConNF.Λ) : (ConNF.allowableEquiv α) 1 = 1

theorem ConNF.allowableEquiv_mul [ConNF.Params] (α : ConNF.Λ) (ρ₁ : ConNF.Allowable ↑α) (ρ₂ : ConNF.Allowable ↑α) : (ConNF.allowableEquiv α) (ρ₁ * ρ₂) = (ConNF.allowableEquiv α) ρ₁ * (ConNF.allowableEquiv α) ρ₂

def ConNF.allowableIso [ConNF.Params] (α : ConNF.Λ) : ConNF.Allowable ↑α ≃* (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).Allowable

Equations

• ConNF.allowableIso α = let __spread.0 := ConNF.allowableEquiv α; { toEquiv := __spread.0, map_mul' := ⋯ }

theorem ConNF.allowableIso_toStructPerm [ConNF.Params] (α : ConNF.Λ) (ρ : ConNF.Allowable ↑α) : (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).allowableToStructPerm ((ConNF.allowableIso α) ρ) = ConNF.Allowable.toStructPerm ρ

@[simp]

theorem ConNF.tSetEquiv_toStructSet [ConNF.Params] (α : ConNF.Λ) (t : ConNF.TSet ↑α) : (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).toStructSet ((ConNF.tSetEquiv α) t) = ConNF.toStructSet t

@[simp]

theorem ConNF.tSetEquiv_smul [ConNF.Params] (α : ConNF.Λ) (ρ : ConNF.Allowable ↑α) (t : ConNF.TSet ↑α) : (ConNF.tSetEquiv α) (ρ • t) = (ConNF.allowableIso α) ρ • (ConNF.tSetEquiv α) t

@[simp]

theorem ConNF.tangleEquiv_smul [ConNF.Params] (α : ConNF.Λ) (ρ : ConNF.Allowable ↑α) (t : ConNF.Tangle ↑α) : (ConNF.tangleEquiv α) (ρ • t) = (ConNF.allowableIso α) ρ • (ConNF.tangleEquiv α) t

Because we already defined names for things like Tangle.set in the inductive step, we can't give them the same names here.

def ConNF.Tangle.toSet [ConNF.Params] {β : ConNF.TypeIndex} : ConNF.Tangle β → ConNF.TSet β

Equations

• x.toSet = match x✝, x with | some β, t => t.set | none, a => a

@[simp]

theorem ConNF.Tangle.bot_toSet [ConNF.Params] (t : ConNF.Tangle ⊥) : t.toSet = t

@[simp]

theorem ConNF.Tangle.coe_toSet [ConNF.Params] (β : ConNF.Λ) (t : ConNF.Tangle ↑β) : t.toSet = t.set

theorem ConNF.Tangle.ext' [ConNF.Params] {β : ConNF.TypeIndex} (t₁ : ConNF.Tangle β) (t₂ : ConNF.Tangle β) (hs : t₁.toSet = t₂.toSet) (hS : t₁.support = t₂.support) : t₁ = t₂

@[simp]

theorem ConNF.Tangle.smul_toSet [ConNF.Params] {β : ConNF.TypeIndex} (t : ConNF.Tangle β) (ρ : ConNF.Allowable β) : (ρ • t).toSet = ρ • t.toSet

@[simp]

theorem ConNF.tangleEquiv_toSet [ConNF.Params] (α : ConNF.Λ) (t : ConNF.Tangle ↑α) : ((ConNF.tangleEquiv α) t).set = (ConNF.tSetEquiv α) t.toSet

@[simp]

theorem ConNF.tangleEquiv_support [ConNF.Params] (α : ConNF.Λ) (t : ConNF.Tangle ↑α) : ((ConNF.tangleEquiv α) t).support = t.support

@[simp]

theorem ConNF.tSetEquiv_typedNearLitter [ConNF.Params] (α : ConNF.Λ) (N : ConNF.NearLitter) : (ConNF.tSetEquiv α) (ConNF.typedNearLitter N) = (ConNF.MainInduction.buildStep α (fun (β : ConNF.Λ) (x : β < α) => ConNF.constructionIH β) ⋯).typedNearLitter N

def ConNF.cons'Coe [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : ↑β < ↑α) : ConNF.Allowable ↑α → ConNF.Allowable ↑β

Equations

• ConNF.cons'Coe hβ = ⇑(Equiv.cast ⋯) ∘ ⇑⋯.choose

theorem ConNF.cons'Coe_spec [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : ↑β < ↑α) (ρ : ConNF.Allowable ↑α) : ConNF.Tree.comp (Quiver.Hom.toPath hβ) (ConNF.Allowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm (ConNF.cons'Coe hβ ρ)

def ConNF.cons'Bot [ConNF.Params] {α : ConNF.Λ} : ConNF.Allowable ↑α → ConNF.BasePerm

Equations

• ConNF.cons'Bot = ⇑⋯.choose

theorem ConNF.cons'Bot_spec [ConNF.Params] {α : ConNF.Λ} (ρ : ConNF.Allowable ↑α) : ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) = ConNF.cons'Bot ρ

def ConNF.cons'' [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (h : β < α) : ConNF.Allowable α → ConNF.Allowable β

Equations

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

theorem ConNF.cons''_one [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (h : β < α) : ConNF.cons'' h 1 = 1

theorem ConNF.cons'_mul [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (h : β < α) (ρ₁ : ConNF.Allowable α) (ρ₂ : ConNF.Allowable α) : ConNF.cons'' h (ρ₁ * ρ₂) = ConNF.cons'' h ρ₁ * ConNF.cons'' h ρ₂

def ConNF.cons' [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (h : β < α) : ConNF.Allowable α →* ConNF.Allowable β

Equations

• ConNF.cons' h = { toFun := ConNF.cons'' h, map_one' := ⋯, map_mul' := ⋯ }

theorem ConNF.cons'_spec [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (hβ : β < α) (ρ : ConNF.Allowable α) : ConNF.Tree.comp (Quiver.Hom.toPath hβ) (ConNF.Allowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm ((ConNF.cons' hβ) ρ)

@[simp]

theorem ConNF.allowableIso_val [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (hβ : β < α) (ρ : ConNF.Allowable ↑α) : ↑((ConNF.allowableIso α) ρ) ↑β = (ConNF.cons' ⋯) ρ

def ConNF.comp [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (A : Quiver.Path α β) : ConNF.Allowable α →* ConNF.Allowable β

Equations

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

@[simp]

theorem ConNF.comp_nil [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.comp Quiver.Path.nil = MonoidHom.id (ConNF.Allowable α)

@[simp]

theorem ConNF.comp_toPath [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (h : β < α) : ConNF.comp (Quiver.Hom.toPath h) = ConNF.cons' h

@[simp]

theorem ConNF.comp_cons [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} (A : Quiver.Path α β) (h : γ < β) : ConNF.comp (A.cons h) = (ConNF.cons' h).comp (ConNF.comp A)

@[simp]

theorem ConNF.comp_comp [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} (A : Quiver.Path α β) (B : Quiver.Path β γ) : ConNF.comp (A.comp B) = (ConNF.comp B).comp (ConNF.comp A)

@[simp]

theorem ConNF.comp_toStructPerm [ConNF.Params] {α : ConNF.TypeIndex} {β : ConNF.TypeIndex} (A : Quiver.Path α β) (ρ : ConNF.Allowable α) : ConNF.Allowable.toStructPerm ((ConNF.comp A) ρ) = ConNF.Tree.comp A (ConNF.Allowable.toStructPerm ρ)

@[simp]

theorem ConNF.allowableIso_smul_address [ConNF.Params] {α : ConNF.Λ} (ρ : ConNF.Allowable ↑α) (c : ConNF.Address ↑α) : (ConNF.allowableIso α) ρ • c = ρ • c

theorem ConNF.allowableIso_apply_eq [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (h : ↑β < ↑α) (ρ : ConNF.Allowable ↑α) : ↑((ConNF.allowableIso α) ρ) ↑β = (ConNF.comp (Quiver.Hom.toPath h)) ρ

def ConNF.cons [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (h : β < α) : ConNF.Allowable ↑α →* ConNF.Allowable ↑β

Equations

• ConNF.cons h = ConNF.cons' ⋯

@[simp]

theorem ConNF.cons'_eq_cons [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (h : ↑β < ↑α) : ConNF.cons' h = ConNF.cons ⋯

@[simp]

theorem ConNF.cons_toStructPerm [ConNF.Params] {α : ConNF.Λ} {β : ConNF.Λ} (h : β < α) (ρ : ConNF.Allowable ↑α) : ConNF.Allowable.toStructPerm ((ConNF.cons h) ρ) = ConNF.Tree.comp (Quiver.Hom.toPath ⋯) (ConNF.Allowable.toStructPerm ρ)