New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

theorem ConNF.constructMotive_allPerm_of_smul_fuzz [Params] {α : Λ} (M : (β : Λ) → ↑β < ↑α → Motive β) (H : (β : Λ) → (h : ↑β < ↑α) → Hypothesis (M β h) fun (γ : Λ) (h' : ↑γ < ↑β) => M γ ⋯) (ρs : {β : Λ} → (hβ : ↑β < ↑α) → AllPerm ↑β) (π : AllPerm ⊥) : (∀ {β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑α) (hδε : ↑β ≠ ↑γ) (t : Tangle ↑β), (ρs hγ)ᵁ ↘. • fuzz hδε t = fuzz hδε (ρs hβ • t)) → (∀ {γ : Λ} (hγ : ↑γ < ↑α) (t : Tangle ⊥), (ρs hγ)ᵁ ↘. • fuzz ⋯ t = fuzz ⋯ (π • t)) → ∃ (ρ : AllPerm ↑α), (∀ (β : Λ) (hβ : ↑β < ↑α), constructAllPermSderiv M H hβ ρ = ρs hβ) ∧ constructAllPermBotSderiv M H ρ = π

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

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

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

Equations

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