New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

Equations

• ConNF.ltData M = ConNF.LtData.mk

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

Equations

• ConNF.newModelData' M = ConNF.newModelData

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

Equations

• ConNF.leData M = ConNF.LeData.mk

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

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

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

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

Equations

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

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

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

Equations

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