New file

In this file...

Main declarations

• ConNF.foo: Something new.

def ConNF.ltData [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) : LtData

Equations

• ConNF.ltData M = ConNF.LtData.mk

def ConNF.newModelData' [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) : ModelData ↑α

Equations

• ConNF.newModelData' M = ConNF.newModelData

def ConNF.leData [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) : LeData

Equations

• ConNF.leData M = ConNF.LeData.mk

theorem ConNF.leData_data_bot [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) : LeData.data ⊥ = botModelData

theorem ConNF.leData_data_lt [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) : LeData.data ↑β = (M β hβ).data

theorem ConNF.leData_data_eq [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) : LeData.data ↑α = newModelData' M

@[reducible, inline]

abbrev ConNF.TSetLe [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (β : TypeIndex) (hβ : β ≤ ↑α) : Type u

Equations

• ConNF.TSetLe M β hβ = ConNF.TSet β

@[reducible, inline]

abbrev ConNF.AllPermLe [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (β : TypeIndex) (hβ : β ≤ ↑α) : Type u

Equations

• ConNF.AllPermLe M β hβ = ConNF.AllPerm β

@[reducible, inline]

abbrev ConNF.TangleLe [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (β : TypeIndex) (hβ : β ≤ ↑α) : Type u

Equations

• ConNF.TangleLe M β hβ = ConNF.Tangle β

def ConNF.castTSetLeLt [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) : TSetLe M ↑β ⋯ ≃ TSet ↑β

Equations

• ConNF.castTSetLeLt M hβ = ConNF.castTSet ⋯ ⋯

def ConNF.castTSetLeEq [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β = ↑α) : TSetLe M ↑β ⋯ ≃ TSet ↑α

Equations

• ConNF.castTSetLeEq M hβ = ConNF.castTSet hβ ⋯

def ConNF.castAllPermLeLt [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) : AllPermLe M ↑β ⋯ ≃ AllPerm ↑β

Equations

• ConNF.castAllPermLeLt M hβ = ConNF.castAllPerm ⋯ ⋯

def ConNF.castAllPermLeEq [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β = ↑α) : AllPermLe M ↑β ⋯ ≃ AllPerm ↑α

Equations

• ConNF.castAllPermLeEq M hβ = ConNF.castAllPerm hβ ⋯

def ConNF.castTangleLeLt [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) : TangleLe M ↑β ⋯ ≃ Tangle ↑β

Equations

• ConNF.castTangleLeLt M hβ = ConNF.castTangle ⋯ ⋯

def ConNF.castTangleLeEq [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β = ↑α) : TangleLe M ↑β ⋯ ≃ Tangle ↑α

Equations

• ConNF.castTangleLeEq M hβ = ConNF.castTangle hβ ⋯

theorem ConNF.castTSetLeLt_forget [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (x : TSetLe M ↑β ⋯) : PreModelData.tSetForget ((castTSetLeLt M hβ) x) = PreModelData.tSetForget x

theorem ConNF.castTSetLeEq_forget [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (x : TSetLe M ↑α ⋯) : PreModelData.tSetForget ((castTSetLeEq M ⋯) x) = PreModelData.tSetForget x

theorem ConNF.castAllPermLeLt_forget [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (ρ : AllPermLe M ↑β ⋯) : PreModelData.allPermForget ((castAllPermLeLt M hβ) ρ) = PreModelData.allPermForget ρ

theorem ConNF.castAllPermLeEq_forget [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (ρ : AllPermLe M ↑α ⋯) : PreModelData.allPermForget ((castAllPermLeEq M ⋯) ρ) = PreModelData.allPermForget ρ

theorem ConNF.castTangleLeLt_support [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (t : TangleLe M ↑β ⋯) : ((castTangleLeLt M hβ) t).support = t.support

theorem ConNF.castAllPermLeLt_smul [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (ρ : AllPerm ↑β) (t : TangleLe M ↑β ⋯) : ρ • (castTangleLeLt M hβ) t = (castTangleLeLt M hβ) ((castAllPermLeLt M hβ).symm ρ • t)

theorem ConNF.castAllPermLeLt_smul' [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (ρ : AllPermLe M ↑β ⋯) (t : TangleLe M ↑β ⋯) : (castTangleLeLt M hβ) (ρ • t) = (castAllPermLeLt M hβ) ρ • (castTangleLeLt M hβ) t

theorem ConNF.castAllPermLeLt_smul'' [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (ρ : AllPermLe M ↑β ⋯) (t : Tangle ↑β) : (castAllPermLeLt M hβ) ρ • t = (castTangleLeLt M hβ) (ρ • (castTangleLeLt M hβ).symm t)

theorem ConNF.castTangleLeLt_pos [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (t : TangleLe M ↑β ⋯) : pos ((castTangleLeLt M hβ) t) = pos t

theorem ConNF.castTangleLeLt_fuzz [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) {β : Λ} (hβ : ↑β < ↑α) (t : TangleLe M ↑β ⋯) {γ : Λ} (hβγ : ↑β ≠ ↑γ) : fuzz hβγ ((castTangleLeLt M hβ) t) = fuzz hβγ t

def ConNF.preCoherentData [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) : PreCoherentData

Equations

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

theorem ConNF.preCoherentData_allPermSderiv_forget [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β γ : TypeIndex} [iβ : LeLevel β] [iγ : LeLevel γ] (hγ : γ < β) (ρ : AllPermLe M β ⋯) : PreModelData.allPermForget (PreCoherentData.allPermSderiv hγ ρ) = PreModelData.allPermForget ρ ↘ hγ

theorem ConNF.preCoherentData_pos_atom_lt_pos [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β : TypeIndex} [iβ : LtLevel β] (t : TangleLe M β ⋯) (A : β ↝ ⊥) (a : Atom) (ha : a ∈ (t.support ⇘. A)ᴬ) : pos a < pos t

theorem ConNF.preCoherentData_pos_nearLitter_lt_pos [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β : TypeIndex} [iβ : LtLevel β] (t : TangleLe M β ⋯) (A : β ↝ ⊥) (N : NearLitter) (hN : N ∈ (t.support ⇘. A)ᴺ) : pos N < pos t

theorem ConNF.preCoherentData_smul_fuzz [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β : Λ} {γ : TypeIndex} {δ : Λ} [iβ : LeLevel ↑β] [iγ : LtLevel γ] [iδ : LtLevel ↑δ] (hγ : γ < ↑β) (hδ : ↑δ < ↑β) (hγδ : γ ≠ ↑δ) (ρ : AllPermLe M ↑β ⋯) (t : TangleLe M γ ⋯) : PreModelData.allPermForget ρ ↘ hδ ↘. • fuzz hγδ t = fuzz hγδ (PreCoherentData.allPermSderiv hγ ρ • t)

theorem ConNF.preCoherentData_allPerm_of_smulFuzz [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β : Λ} [iβ : LeLevel ↑β] (ρs : {γ : TypeIndex} → [inst : LtLevel γ] → γ < ↑β → AllPermLe M γ ⋯) (hρs : ∀ {γ : TypeIndex} {δ : Λ} [inst : LtLevel γ] [inst_1 : LtLevel ↑δ] (hγ : γ < ↑β) (hδ : ↑δ < ↑β) (hγδ : γ ≠ ↑δ) (t : TangleLe M γ ⋯), PreModelData.allPermForget (ρs hδ) ↘. • fuzz hγδ t = fuzz hγδ (ρs hγ • t)) : ∃ (ρ : AllPermLe M ↑β ⋯), ∀ (γ : TypeIndex) [inst : LtLevel γ] (hγ : γ < ↑β), PreCoherentData.allPermSderiv hγ ρ = ρs hγ

theorem ConNF.preCoherent_tSet_ext [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β γ : Λ} [iβ : LeLevel ↑β] [iγ : LeLevel ↑γ] (hγ : ↑γ < ↑β) (x y : TSetLe M ↑β ⋯) (hxy : ∀ (z : TSetLe M ↑γ ⋯), z ∈[hγ] x ↔ z ∈[hγ] y) : x = y

theorem ConNF.typedMem_singleton_iff [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β γ : Λ} [iβ : LeLevel ↑β] [iγ : LeLevel ↑γ] (hγ : ↑γ < ↑β) (x y : TSetLe M ↑γ ⋯) : y ∈[hγ] singleton hγ x ↔ y = x

def ConNF.coherentData [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) : CoherentData

Equations

• ConNF.coherentData M H = ConNF.CoherentData.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem ConNF.newModelData_card_tangle_le [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) : Cardinal.mk (Tangle ↑α) ≤ Cardinal.mk μ

def ConNF.constructMotive [Params] (α : Λ) (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) : Motive α

Equations

• ConNF.constructMotive α M H = { data := ConNF.newModelData, pos := ConNF.newPosition ⋯, typed := ConNF.newTypedNearLitters ⋯ }