New file

In this file...

Main declarations

• ConNF.foo: Something new.

structure ConNF.Motive [ConNF.Params] (α : ConNF.Λ) : Type (u + 1)

• data : ConNF.ModelData ↑α
• pos : ConNF.Position (ConNF.Tangle ↑α)
• typed : ConNF.TypedNearLitters α

theorem ConNF.card_tangle_bot_le [ConNF.Params] [ConNF.ModelData ⊥] : Cardinal.mk (ConNF.Tangle ⊥) ≤ Cardinal.mk ConNF.μ

def ConNF.botPosition [ConNF.Params] [ConNF.ModelData ⊥] : ConNF.Position (ConNF.Tangle ⊥)

Equations

• ConNF.botPosition = { pos := { toFun := ConNF.funOfDeny ⋯ (fun (t : ConNF.Tangle ⊥) => ⇑ConNF.pos '' (t.supportᴬ.image Prod.snd).rel.codom) ⋯, inj' := ⋯ } }

theorem ConNF.pos_tangle_bot [ConNF.Params] {D : ConNF.ModelData ⊥} (t : ConNF.Tangle ⊥) (a : ConNF.Atom) (A : ⊥ ↝ ⊥) (ha : a ∈ (t.support ⇘. A)ᴬ) : ConNF.pos a < ConNF.pos t

structure ConNF.Hypothesis [ConNF.Params] {α : ConNF.Λ} (M : ConNF.Motive α) (N : (β : ConNF.Λ) → ↑β < ↑α → ConNF.Motive β) : Type u

• allPermSderiv : {β : ConNF.Λ} → (h : ↑β < ↑α) → ConNF.AllPerm ↑α → ConNF.AllPerm ↑β
• allPermBotSderiv : ConNF.AllPerm ↑α → ConNF.AllPerm ⊥
• singleton : {β : ConNF.Λ} → (h : ↑β < ↑α) → ConNF.TSet ↑β → ConNF.TSet ↑α
• allPermSderiv_forget : ∀ {β : ConNF.Λ} (h : ↑β < ↑α) (ρ : ConNF.AllPerm ↑α), ConNF.PreModelData.allPermForget (self.allPermSderiv h ρ) = ConNF.PreModelData.allPermForget ρ ↘ h
• allPermBotSderiv_forget : ∀ (ρ : ConNF.AllPerm ↑α), ConNF.PreModelData.allPermForget (self.allPermBotSderiv ρ) = ConNF.PreModelData.allPermForget ρ ↘ ⋯
• pos_atom_lt_pos : ∀ (t : ConNF.Tangle ↑α) (A : ↑α ↝ ⊥), ∀ a ∈ (t.support ⇘. A)ᴬ, ConNF.pos a < ConNF.pos t
• pos_nearLitter_lt_pos : ∀ (t : ConNF.Tangle ↑α) (A : ↑α ↝ ⊥), ∀ N ∈ (t.support ⇘. A)ᴺ, ConNF.pos N < ConNF.pos t
• smul_fuzz : ∀ {β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑α) (hβγ : ↑β ≠ ↑γ) (ρ : ConNF.AllPerm ↑α) (t : ConNF.Tangle ↑β), ConNF.PreModelData.allPermForget ρ ↘ hγ ↘. • ConNF.fuzz hβγ t = ConNF.fuzz hβγ (self.allPermSderiv hβ ρ • t)
• smul_fuzz_bot : ∀ {γ : ConNF.Λ} (hγ : ↑γ < ↑α) (ρ : ConNF.AllPerm ↑α) (t : ConNF.Tangle ⊥), ConNF.PreModelData.allPermForget ρ ↘ hγ ↘. • ConNF.fuzz ⋯ t = ConNF.fuzz ⋯ (self.allPermBotSderiv ρ • t)
• allPerm_of_smul_fuzz : ∀ (ρs : {β : ConNF.Λ} → (hβ : ↑β < ↑α) → ConNF.AllPerm ↑β) (π : ConNF.AllPerm ⊥), (∀ {β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑α) (hδε : ↑β ≠ ↑γ) (t : ConNF.Tangle ↑β), (ρs hγ)ᵁ ↘. • ConNF.fuzz hδε t = ConNF.fuzz hδε (ρs hβ • t)) → (∀ {γ : ConNF.Λ} (hγ : ↑γ < ↑α) (t : ConNF.Tangle ⊥), (ρs hγ)ᵁ ↘. • ConNF.fuzz ⋯ t = ConNF.fuzz ⋯ (π • t)) → ∃ (ρ : ConNF.AllPerm ↑α), (∀ (β : ConNF.Λ) (hβ : ↑β < ↑α), self.allPermSderiv hβ ρ = ρs hβ) ∧ self.allPermBotSderiv ρ = π
• tSet_ext : ∀ (β : ConNF.Λ) (hβ : ↑β < ↑α) (x y : ConNF.TSet ↑α), (∀ (z : ConNF.TSet ↑β), z ∈[hβ] x ↔ z ∈[hβ] y) → x = y
• typedMem_singleton_iff : ∀ {β : ConNF.Λ} (hβ : ↑β < ↑α) (x y : ConNF.TSet ↑β), y ∈[hβ] self.singleton hβ x ↔ y = x

def ConNF.castTSet [ConNF.Params] {α β : ConNF.TypeIndex} {D₁ : ConNF.ModelData α} {D₂ : ConNF.ModelData β} (h₁ : α = β) (h₂ : HEq D₁ D₂) : ConNF.TSet α ≃ ConNF.TSet β

Equations

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

def ConNF.castAllPerm [ConNF.Params] {α β : ConNF.TypeIndex} {D₁ : ConNF.ModelData α} {D₂ : ConNF.ModelData β} (h₁ : α = β) (h₂ : HEq D₁ D₂) : ConNF.AllPerm α ≃ ConNF.AllPerm β

Equations

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

def ConNF.castTangle [ConNF.Params] {α β : ConNF.TypeIndex} {D₁ : ConNF.ModelData α} {D₂ : ConNF.ModelData β} (h₁ : α = β) (h₂ : HEq D₁ D₂) : ConNF.Tangle α ≃ ConNF.Tangle β

Equations

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

theorem ConNF.castTSet_forget [ConNF.Params] {α : ConNF.TypeIndex} {D₁ D₂ : ConNF.ModelData α} (h₂ : HEq D₁ D₂) (ρ : ConNF.TSet α) : ConNF.PreModelData.tSetForget ((ConNF.castTSet ⋯ h₂) ρ) = ConNF.PreModelData.tSetForget ρ

theorem ConNF.castAllPerm_forget [ConNF.Params] {α : ConNF.TypeIndex} {D₁ D₂ : ConNF.ModelData α} (h₂ : HEq D₁ D₂) (ρ : ConNF.AllPerm α) : ConNF.PreModelData.allPermForget ((ConNF.castAllPerm ⋯ h₂) ρ) = ConNF.PreModelData.allPermForget ρ

theorem ConNF.castTangle_support [ConNF.Params] {α : ConNF.TypeIndex} {D₁ D₂ : ConNF.ModelData α} (h₂ : HEq D₁ D₂) (t : ConNF.Tangle α) : ((ConNF.castTangle ⋯ h₂) t).support = t.support

theorem ConNF.castAllPerm_smul [ConNF.Params] {α : ConNF.TypeIndex} {D₁ D₂ : ConNF.ModelData α} (h₂ : HEq D₁ D₂) (ρ : ConNF.AllPerm α) (t : ConNF.Tangle α) : ρ • (ConNF.castTangle ⋯ h₂) t = (ConNF.castTangle ⋯ h₂) ((ConNF.castAllPerm ⋯ h₂).symm ρ • t)

theorem ConNF.castTangle_pos [ConNF.Params] {α β : ConNF.TypeIndex} {D₁ : ConNF.ModelData α} {D₂ : ConNF.ModelData β} {E₁ : ConNF.Position (ConNF.Tangle α)} {E₂ : ConNF.Position (ConNF.Tangle β)} (h₁ : α = β) (h₂ : HEq D₁ D₂) (h₃ : HEq E₁ E₂) (t : ConNF.Tangle α) : ConNF.pos ((ConNF.castTangle h₁ h₂) t) = ConNF.pos t

theorem ConNF.castTangle_fuzz [ConNF.Params] {α : ConNF.TypeIndex} {D₁ D₂ : ConNF.ModelData α} {E₁ : ConNF.Position (ConNF.Tangle α)} {E₂ : ConNF.Position (ConNF.Tangle α)} (h₂ : HEq D₁ D₂) (h₃ : HEq E₁ E₂) (t : ConNF.Tangle α) {β : ConNF.Λ} (hαβ : α ≠ ↑β) : ConNF.fuzz hαβ ((ConNF.castTangle ⋯ h₂) t) = ConNF.fuzz hαβ t