New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

Equations

• ConNF.constructAllPermSderiv M H h ρ = ρ.sderiv ↑β

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

Equations

• ConNF.constructAllPermBotSderiv M H ρ = ρ.sderiv ⊥

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

Equations

• ConNF.constructSingleton M H h x = some (ConNF.newSingleton x)

theorem ConNF.constructMotive_allPermSderiv_forget [ConNF.Params] {α : ConNF.Λ} (M : (β : ConNF.Λ) → ↑β < ↑α → ConNF.Motive β) (H : (β : ConNF.Λ) → (h : ↑β < ↑α) → ConNF.Hypothesis (M β h) fun (γ : ConNF.Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β : ConNF.Λ} (h : ↑β < ↑α) (ρ : ConNF.AllPerm ↑α) : ConNF.PreModelData.allPermForget (ConNF.constructAllPermSderiv M H h ρ) = ConNF.PreModelData.allPermForget ρ ↘ h

theorem ConNF.constructMotive_allPermBotSderiv_forget [ConNF.Params] {α : ConNF.Λ} (M : (β : ConNF.Λ) → ↑β < ↑α → ConNF.Motive β) (H : (β : ConNF.Λ) → (h : ↑β < ↑α) → ConNF.Hypothesis (M β h) fun (γ : ConNF.Λ) (h' : ↑γ < ↑β) => M γ ⋯) (ρ : ConNF.AllPerm ↑α) : ConNF.PreModelData.allPermForget (ConNF.constructAllPermBotSderiv M H ρ) = ConNF.PreModelData.allPermForget ρ ↘ ⋯

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

theorem ConNF.constructMotive_pos_nearLitter_lt_pos [ConNF.Params] {α : ConNF.Λ} (M : (β : ConNF.Λ) → ↑β < ↑α → ConNF.Motive β) (H : (β : ConNF.Λ) → (h : ↑β < ↑α) → ConNF.Hypothesis (M β h) fun (γ : ConNF.Λ) (h' : ↑γ < ↑β) => M γ ⋯) (t : ConNF.Tangle ↑α) (A : ↑α ↝ ⊥) (M✝ : ConNF.NearLitter) : M✝ ∈ (t.support ⇘. A)ᴺ → ConNF.pos M✝ < ConNF.pos t

theorem ConNF.constructMotive_smul_fuzz [ConNF.Params] {α : ConNF.Λ} (M : (β : ConNF.Λ) → ↑β < ↑α → ConNF.Motive β) (H : (β : ConNF.Λ) → (h : ↑β < ↑α) → ConNF.Hypothesis (M β h) fun (γ : ConNF.Λ) (h' : ↑γ < ↑β) => M γ ⋯) {β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑α) (hβγ : ↑β ≠ ↑γ) (ρ : ConNF.AllPerm ↑α) (t : ConNF.Tangle ↑β) : ConNF.PreModelData.allPermForget ρ ↘ hγ ↘. • ConNF.fuzz hβγ t = ConNF.fuzz hβγ (ConNF.constructAllPermSderiv M H hβ ρ • t)

theorem ConNF.constructMotive_smul_fuzz_bot [ConNF.Params] {α : ConNF.Λ} (M : (β : ConNF.Λ) → ↑β < ↑α → ConNF.Motive β) (H : (β : ConNF.Λ) → (h : ↑β < ↑α) → ConNF.Hypothesis (M β h) fun (γ : ConNF.Λ) (h' : ↑γ < ↑β) => M γ ⋯) {γ : ConNF.Λ} (hγ : ↑γ < ↑α) (ρ : ConNF.AllPerm ↑α) (t : ConNF.Tangle ⊥) : ConNF.PreModelData.allPermForget ρ ↘ hγ ↘. • ConNF.fuzz ⋯ t = ConNF.fuzz ⋯ (ConNF.constructAllPermBotSderiv M H ρ • t)

theorem ConNF.constructMotive_allPerm_of_smul_fuzz [ConNF.Params] {α : ConNF.Λ} (M : (β : ConNF.Λ) → ↑β < ↑α → ConNF.Motive β) (H : (β : ConNF.Λ) → (h : ↑β < ↑α) → ConNF.Hypothesis (M β h) fun (γ : ConNF.Λ) (h' : ↑γ < ↑β) => M γ ⋯) (ρ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β : ↑β < ↑α), ConNF.constructAllPermSderiv M H hβ ρ = ρs hβ) ∧ ConNF.constructAllPermBotSderiv M H ρ = π

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

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

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

Equations

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