Construction of t-sets

In this file, we construct the type of t-sets at level α, assuming they exist at all levels β < α.

Main declarations

• ConNF.Extensions: The type of extensions of a t-set at level α.
• ConNF.Preference: A preferred extension of a extensional set.
• ConNF.ExtensionalSet: An extension for each β < α, with one chosen as its preferred extension. The non-preferred extensions can be derived from the preferred extension.
• ConNF.NewTangle: The type of t-sets at level α.

@[reducible, inline]

abbrev ConNF.Extensions [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Type u

Equations

• ConNF.Extensions = ((β : ConNF.Λ) → [inst_1 : ConNF.LtLevel ↑β] → Set (ConNF.TSet ↑β))

theorem ConNF.Extensions.ext [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {e₁ : ConNF.Extensions} {e₂ : ConNF.Extensions} (h : ∀ (β : ConNF.Λ) [inst : ConNF.LtLevel ↑β], e₁ β = e₂ β) : e₁ = e₂

Extensional sets

inductive ConNF.ExtensionalSet.Preference [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (members : ConNF.Extensions) : Type u

Keeps track of the preferred extension of a extensional set, along with coherence conditions relating each extension of the extensional set. In particular, each non-preferred extension can be obtained by applying the cloud map to the preferred extension.

• base: [inst : ConNF.Params] → [inst_1 : ConNF.Level] → [inst_2 : ConNF.BasePositions] → [inst_3 : ConNF.ModelDataLt] → [inst_4 : ConNF.PositionedTanglesLt] → [inst_5 : ConNF.TypedObjectsLt] → {members : ConNF.Extensions} → (atoms : Set (ConNF.Tangle ⊥)) → (∀ (γ : ConNF.Λ) [inst_6 : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ atoms = members γ) → ConNF.ExtensionalSet.Preference members
• proper: [inst : ConNF.Params] → [inst_1 : ConNF.Level] → [inst_2 : ConNF.BasePositions] → [inst_3 : ConNF.ModelDataLt] → [inst_4 : ConNF.PositionedTanglesLt] → [inst_5 : ConNF.TypedObjectsLt] → {members : ConNF.Extensions} → (β : ConNF.Λ) → [inst_6 : ConNF.LtLevel ↑β] → (ConNF.Code.mk (↑β) (members β)).IsEven → (∀ (γ : ConNF.Λ) [inst_7 : ConNF.LtLevel ↑γ] (hβγ : ↑β ≠ ↑γ), ConNF.cloud hβγ (members β) = members γ) → ConNF.ExtensionalSet.Preference members

def ConNF.ExtensionalSet.Preference.atoms [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {members : ConNF.Extensions} : ConNF.ExtensionalSet.Preference members → Set ConNF.Atom

The ⊥-extension in a given extensional set, if it exists.

Equations

• x.atoms = match x with | ConNF.ExtensionalSet.Preference.base atoms a => atoms | ConNF.ExtensionalSet.Preference.proper β a a_1 => ∅

theorem ConNF.ExtensionalSet.Preference.base_heq_base [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {m₁ : ConNF.Extensions} {m₂ : ConNF.Extensions} {s₁ : Set (ConNF.Tangle ⊥)} {s₂ : Set (ConNF.Tangle ⊥)} {h₁ : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ s₁ = m₁ γ} {h₂ : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ s₂ = m₂ γ} (hm : m₁ = m₂) (hs : s₁ = s₂) : HEq (ConNF.ExtensionalSet.Preference.base s₁ h₁) (ConNF.ExtensionalSet.Preference.base s₂ h₂)

theorem ConNF.ExtensionalSet.Preference.proper_heq_proper [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {m₁ : ConNF.Extensions} {m₂ : ConNF.Extensions} {β₁ : ConNF.Λ} {β₂ : ConNF.Λ} [ConNF.LtLevel ↑β₁] [ConNF.LtLevel ↑β₂] {h₁ : (ConNF.Code.mk (↑β₁) (m₁ β₁)).IsEven} {h₂ : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ] (hβγ : ↑β₁ ≠ ↑γ), ConNF.cloud hβγ (m₁ β₁) = m₁ γ} {h₃ : (ConNF.Code.mk (↑β₂) (m₂ β₂)).IsEven} {h₄ : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ] (hβγ : ↑β₂ ≠ ↑γ), ConNF.cloud hβγ (m₂ β₂) = m₂ γ} (hm : m₁ = m₂) (hs : β₁ = β₂) : HEq (ConNF.ExtensionalSet.Preference.proper β₁ h₁ h₂) (ConNF.ExtensionalSet.Preference.proper β₂ h₃ h₄)

structure ConNF.ExtensionalSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] : Type u

A extensional set is a collection of β-tangles for each lower level β < α, together with a preference for one of these extensions.

• members : ConNF.Extensions
• pref : ConNF.ExtensionalSet.Preference self.members

def ConNF.ExtensionalSet.reprCode [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] : ConNF.ExtensionalSet → ConNF.Code

The even code associated to a extensional set.

Equations

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

@[simp]

theorem ConNF.ExtensionalSet.reprCode_base [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (exts : ConNF.Extensions) (atoms : Set (ConNF.Tangle ⊥)) (hA : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ atoms = exts γ) : { members := exts, pref := ConNF.ExtensionalSet.Preference.base atoms hA }.reprCode = ConNF.Code.mk ⊥ atoms

@[simp]

theorem ConNF.ExtensionalSet.reprCode_proper [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (exts : ConNF.Extensions) (β : ConNF.Λ) [ConNF.LtLevel ↑β] (rep : (ConNF.Code.mk (↑β) (exts β)).IsEven) (hA : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ] (hβγ : ↑β ≠ ↑γ), ConNF.cloud hβγ (exts β) = exts γ) : { members := exts, pref := ConNF.ExtensionalSet.Preference.proper β rep hA }.reprCode = ConNF.Code.mk (↑β) (exts β)

theorem ConNF.ExtensionalSet.reprCodeSpec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (t : ConNF.ExtensionalSet) : t.reprCode.IsEven

theorem ConNF.ExtensionalSet.reprCode_members_ne [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (t : ConNF.ExtensionalSet) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] : t.reprCode.β ≠ ↑γ → (ConNF.cloudCode γ t.reprCode).members = t.members γ

theorem ConNF.ExtensionalSet.ext_core [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t₁ : ConNF.ExtensionalSet) (t₂ : ConNF.ExtensionalSet) : Nonempty ((γ : ConNF.Λ) ×' ConNF.LtLevel ↑γ) → t₁.members = t₂.members → t₁ = t₂

One form of extensionality: If there is a proper type index γ < α, then two extensional sets with the same elements have the same preference.

This formulation of extensionality holds only for types larger than type zero, since it doesn't take into account any ⊥-extension.

theorem ConNF.ExtensionalSet.ext_code [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {t₁ : ConNF.ExtensionalSet} {t₂ : ConNF.ExtensionalSet} : t₁.reprCode ≡ t₂.reprCode → t₁ = t₂

One useful form of extensionality in tangled type theory. Two extensional sets are equal if their even codes are equivalent (and hence equal, by uniqueness).

theorem ConNF.ExtensionalSet.ext [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t₁ : ConNF.ExtensionalSet) (t₂ : ConNF.ExtensionalSet) (h : t₁.members γ = t₂.members γ) : t₁ = t₂

Extensionality in tangled type theory. Two extensional sets are equal if their β-extensions are equal for any choice of γ < α. TODO: This proof can be golfed quite a bit just by cleaning up the simp calls.

theorem ConNF.ExtensionalSet.ext_zero [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (t₁ : ConNF.ExtensionalSet) (t₂ : ConNF.ExtensionalSet) (α_zero : IsMin ConNF.α) (h : t₁.pref.atoms = t₂.pref.atoms) : t₁ = t₂

Extensionality at the lowest level of tangled type theory. At type 0, all extensional sets have a ⊥-extension. Therefore, the extensionality principle in this case applies to the ⊥-extensions.

def ConNF.ExtensionalSet.intro [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {β : ConNF.TypeIndex} [inst : ConNF.LtLevel β] (s : Set (ConNF.TSet β)) (heven : (ConNF.Code.mk β s).IsEven) : ConNF.ExtensionalSet

Construct a extensional set from an even code.

Equations

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

@[simp]

theorem ConNF.ExtensionalSet.exts_intro [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (s : Set (ConNF.TSet β)) (heven : (ConNF.Code.mk β s).IsEven) : (ConNF.ExtensionalSet.intro s heven).members = ConNF.extension s

noncomputable def ConNF.ExtensionalSet.intro' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {β : ConNF.TypeIndex} [inst : ConNF.LtLevel β] (s : Set (ConNF.TSet β)) : ConNF.ExtensionalSet

Construct an extensional set from any set of t-sets of a smaller level. This uses choice to find the even code representing the given set.

Equations

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

@[simp]

theorem ConNF.ExtensionalSet.ext_intro' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] (s : Set (ConNF.TSet ↑β)) : (ConNF.ExtensionalSet.intro' s).members β = s

Allowable permutations on extensional sets

We now establish that allowable permutations can act on extensional sets.

@[simp]

theorem ConNF.NewAllowable.smul_extension_apply [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (ρ : ConNF.NewAllowable) (s : Set (ConNF.TSet β)) : ↑ρ ↑γ • ConNF.extension s γ = ConNF.extension (↑ρ β • s) γ

instance ConNF.NewAllowable.instMulActionDerivativesExtensions [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : MulAction ConNF.Derivatives ConNF.Extensions

Equations

• ConNF.NewAllowable.instMulActionDerivativesExtensions = MulAction.mk ⋯ ⋯

@[simp]

theorem ConNF.NewAllowable.smul_extension [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] {β : ConNF.TypeIndex} [ConNF.LtLevel β] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (ρ : ConNF.NewAllowable) (s : Set (ConNF.TSet β)) : ρ • ConNF.extension s = ConNF.extension (↑ρ β • s)

theorem ConNF.NewAllowable.smul_aux₁ [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {ρ : ConNF.NewAllowable} {e : ConNF.Extensions} {s : Set (ConNF.TSet ⊥)} (h : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ s = e γ) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] : ConNF.cloud ⋯ (↑ρ ⊥ • s) = (ρ • e) γ

theorem ConNF.NewAllowable.smul_aux₂ [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {ρ : ConNF.NewAllowable} {e : ConNF.Extensions} (h : ∀ (δ : ConNF.Λ) [inst : ConNF.LtLevel ↑δ] (hγδ : ↑γ ≠ ↑δ), ConNF.cloud hγδ (e γ) = e δ) (δ : ConNF.Λ) [ConNF.LtLevel ↑δ] (hγδ : ↑γ ≠ ↑δ) : ConNF.cloud hγδ ((ρ • e) γ) = (ρ • e) δ

instance ConNF.NewAllowable.instSMulExtensionalSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : SMul ConNF.NewAllowable ConNF.ExtensionalSet

Equations

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

@[simp]

theorem ConNF.NewAllowable.members_smul' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (ρ : ConNF.NewAllowable) (t : ConNF.ExtensionalSet) : (ρ • t).members = ρ • t.members

@[simp]

theorem ConNF.NewAllowable.smul_base [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (ρ : ConNF.NewAllowable) (e : ConNF.Extensions) (s : Set (ConNF.Tangle ⊥)) (h : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ s = e γ) : ρ • { members := e, pref := ConNF.ExtensionalSet.Preference.base s h } = { members := ρ • e, pref := ConNF.ExtensionalSet.Preference.base (↑ρ ⊥ • s) ⋯ }

@[simp]

theorem ConNF.NewAllowable.smul_proper [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (ρ : ConNF.NewAllowable) (e : ConNF.Extensions) (γ : ConNF.Λ) [ConNF.LtLevel ↑γ] (ht : (ConNF.Code.mk (↑γ) (e γ)).IsEven) (h : ∀ (γ_1 : ConNF.Λ) [inst : ConNF.LtLevel ↑γ_1] (hβγ : ↑γ ≠ ↑γ_1), ConNF.cloud hβγ (e γ) = e γ_1) : ρ • { members := e, pref := ConNF.ExtensionalSet.Preference.proper γ ht h } = { members := ρ • e, pref := ConNF.ExtensionalSet.Preference.proper γ ⋯ ⋯ }

instance ConNF.NewAllowable.instMulActionExtensionalSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : MulAction ConNF.NewAllowable ConNF.ExtensionalSet

Allowable permutations act on extensional sets.

Equations

• ConNF.NewAllowable.instMulActionExtensionalSet = MulAction.mk ⋯ ⋯

def ConNF.ExtensionalSet.toStructSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (t : ConNF.ExtensionalSet) : ConNF.StructSet ↑ConNF.α

Extensional sets can easily be turned into structural sets.

Equations

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

theorem ConNF.ExtensionalSet.toStructSet_ofCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (t : ConNF.ExtensionalSet) : ConNF.StructSet.ofCoe t.toStructSet = fun (β : ConNF.TypeIndex) (hβ : β < ↑ConNF.α) => match β, hβ with | none, hβ => {a : ConNF.StructSet ⊥ | ∃ (s : Set ConNF.Atom) (h : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ s = t.members γ), t.pref = ConNF.ExtensionalSet.Preference.base s h ∧ ConNF.StructSet.ofBot a ∈ s} | some β, hβ => {p : ConNF.StructSet ↑β | ∃ s ∈ t.members β, ConNF.toStructSet s = p}

theorem ConNF.ExtensionalSet.members_eq_of_toStructSet_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] (t₁ : ConNF.ExtensionalSet) (t₂ : ConNF.ExtensionalSet) (h : t₁.toStructSet = t₂.toStructSet) : t₁.members = t₂.members

The members of extensional sets are determined by their underlying structural sets.

theorem ConNF.ExtensionalSet.toStructSet_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : Function.Injective ConNF.ExtensionalSet.toStructSet

theorem ConNF.ExtensionalSet.toStructSet_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (ρ : ConNF.NewAllowable) (t : ConNF.ExtensionalSet) : ρ • t.toStructSet = (ρ • t).toStructSet

theorem ConNF.ExtensionalSet.smul_intro' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {β : ConNF.Λ} [inst : ConNF.LtLevel ↑β] (s : Set (ConNF.TSet ↑β)) (ρ : ConNF.NewAllowable) : ConNF.ExtensionalSet.intro' (↑ρ ↑β • s) = ρ • ConNF.ExtensionalSet.intro' s

Defining t-sets

@[reducible, inline]

abbrev ConNF.NewTSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : Type u

A tangle at the new level α is a extensional set supported by a small support. This is τ_α in the blueprint. Unlike the type tangle, this is not an opaque definition, and we can inspect and unfold it.

Equations

• ConNF.NewTSet = { t : ConNF.ExtensionalSet // ∃ (S : ConNF.Support ↑ConNF.α), MulAction.Supports ConNF.NewAllowable (ConNF.Enumeration.carrier S) t }

theorem ConNF.Code.Equiv.supports [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} {S : Set (ConNF.Address ↑ConNF.α)} (hcd : c ≡ d) (hS : MulAction.Supports ConNF.NewAllowable S c) : MulAction.Supports ConNF.NewAllowable S d

If a set of addresses supports a code, it supports all equivalent codes.

theorem ConNF.Code.Equiv.supports_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} {S : Set (ConNF.Address ↑ConNF.α)} (hcd : c ≡ d) : MulAction.Supports ConNF.NewAllowable S c ↔ MulAction.Supports ConNF.NewAllowable S d

theorem ConNF.Code.Equiv.supported_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {c : ConNF.Code} {d : ConNF.Code} (hcd : c ≡ d) : (∃ (S : ConNF.Support ↑ConNF.α), MulAction.Supports ConNF.NewAllowable (ConNF.Enumeration.carrier S) c) ↔ ∃ (S : ConNF.Support ↑ConNF.α), MulAction.Supports ConNF.NewAllowable (ConNF.Enumeration.carrier S) d

If two codes are equivalent, one is supported if and only if the other is.

@[simp]

theorem ConNF.smul_intro [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {β : ConNF.TypeIndex} [inst : ConNF.LtLevel β] (ρ : ConNF.NewAllowable) (s : Set (ConNF.TSet β)) (hs : (ConNF.Code.mk β s).IsEven) : ρ • ConNF.ExtensionalSet.intro s hs = ConNF.ExtensionalSet.intro (↑ρ β • s) ⋯

theorem ConNF.NewAllowable.smul_address [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {ρ : ConNF.NewAllowable} {c : ConNF.Address ↑ConNF.α} : ρ • c = { path := c.path, value := ConNF.NewAllowable.toStructPerm ρ c.path • c.value }

@[simp]

theorem ConNF.NewAllowable.smul_address_eq_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {ρ : ConNF.NewAllowable} {c : ConNF.Address ↑ConNF.α} : ρ • c = c ↔ ConNF.NewAllowable.toStructPerm ρ c.path • c.value = c.value

@[simp]

theorem ConNF.NewAllowable.smul_address_eq_smul_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] {ρ : ConNF.NewAllowable} {ρ' : ConNF.NewAllowable} {c : ConNF.Address ↑ConNF.α} : ρ • c = ρ' • c ↔ ConNF.NewAllowable.toStructPerm ρ c.path • c.value = ConNF.NewAllowable.toStructPerm ρ' c.path • c.value

def ConNF.newTypedNearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (N : ConNF.NearLitter) : ConNF.NewTSet

For any near-litter N, the code (α, ⊥, N) is a tangle at level α. This is called a typed near-litter.

Equations

• ConNF.newTypedNearLitter N = ⟨ConNF.ExtensionalSet.intro (let_fun this := ↑N.snd; this) ⋯, ⋯⟩

theorem ConNF.preferenceBase_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] {a₁ : Set ConNF.Atom} {a₂ : Set ConNF.Atom} {e₁ : (γ : ConNF.Λ) → [inst : ConNF.LtLevel ↑γ] → Set (ConNF.TSet ↑γ)} {e₂ : (γ : ConNF.Λ) → [inst : ConNF.LtLevel ↑γ] → Set (ConNF.TSet ↑γ)} (he : e₁ = e₂) {h₁ : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ a₁ = e₁ γ} {h₂ : ∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ], ConNF.cloud ⋯ a₂ = e₂ γ} (h : HEq (ConNF.ExtensionalSet.Preference.base a₁ h₁) (ConNF.ExtensionalSet.Preference.base a₂ h₂)) : a₁ = a₂

theorem ConNF.newTypedNearLitter_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : Function.Injective ConNF.newTypedNearLitter

def ConNF.newSingleton' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (β : ConNF.TypeIndex) [i : ConNF.LtLevel β] (t : ConNF.Tangle β) : ConNF.NewTSet

Equations

• ConNF.newSingleton' β t = ⟨ConNF.ExtensionalSet.intro {t.set_lt} ⋯, ⋯⟩

noncomputable def ConNF.newSingleton [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (β : ConNF.TypeIndex) [ConNF.LtLevel β] (t : ConNF.TSet β) : ConNF.NewTSet

Equations

• ConNF.newSingleton β t = ConNF.newSingleton' β ⋯.choose

instance ConNF.NewAllowable.hasSmulNewTSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : SMul ConNF.NewAllowable ConNF.NewTSet

Equations

• ConNF.NewAllowable.hasSmulNewTSet = { smul := fun (ρ : ConNF.NewAllowable) (t : ConNF.NewTSet) => ⟨ρ • ↑t, ⋯⟩ }

@[simp]

theorem ConNF.NewAllowable.coe_smul_newTangle [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (ρ : ConNF.NewAllowable) (t : ConNF.NewTSet) : ρ • ↑t = ρ • ↑t

@[simp]

theorem ConNF.NewAllowable.smul_newTangle_t [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (ρ : ConNF.NewAllowable) (t : ConNF.NewTSet) : ↑(ρ • t) = ρ • ↑t

instance ConNF.NewAllowable.instMulActionNewTSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : MulAction ConNF.NewAllowable ConNF.NewTSet

Allowable permutations act on t-sets at level α.

Equations

• ConNF.NewAllowable.instMulActionNewTSet = MulAction.mk ⋯ ⋯

theorem ConNF.NewAllowable.smul_newTypedNearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (N : ConNF.NearLitter) (ρ : ConNF.NewAllowable) : ρ • ConNF.newTypedNearLitter N = ConNF.newTypedNearLitter (ConNF.NewAllowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • N)

def ConNF.NewTSet.toStructSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t : ConNF.NewTSet) : ConNF.StructSet ↑ConNF.α

Equations

• t.toStructSet = (↑t).toStructSet

theorem ConNF.NewTSet.toStructSet_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] : Function.Injective ConNF.NewTSet.toStructSet

theorem ConNF.NewTSet.toStructSet_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (ρ : ConNF.NewAllowable) (t : ConNF.NewTSet) : (ρ • t).toStructSet = ρ • t.toStructSet

theorem ConNF.NewTSet.ext [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (γ : ConNF.Λ) [iγ : ConNF.LtLevel ↑γ] (t₁ : ConNF.NewTSet) (t₂ : ConNF.NewTSet) (h : ∀ (p : ConNF.StructSet ↑γ), p ∈ ConNF.StructSet.ofCoe t₁.toStructSet ↑γ ⋯ ↔ p ∈ ConNF.StructSet.ofCoe t₂.toStructSet ↑γ ⋯) : t₁ = t₂

The t-sets at level α are extensional at all lower proper type indices.

theorem ConNF.NewTSet.newSingleton'_toStructSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (β : ConNF.TypeIndex) [i : ConNF.LtLevel β] (t : ConNF.Tangle β) : ConNF.StructSet.ofCoe (ConNF.newSingleton' β t).toStructSet β ⋯ = {ConNF.toStructSet t.set_lt}

theorem ConNF.NewTSet.newSingleton_toStructSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (β : ConNF.TypeIndex) [i : ConNF.LtLevel β] (t : ConNF.TSet β) : ConNF.StructSet.ofCoe (ConNF.newSingleton β t).toStructSet β ⋯ = {ConNF.toStructSet t}

noncomputable def ConNF.NewTSet.intro [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] (s : Set (ConNF.TSet ↑β)) (hs : ∃ (S : Set (ConNF.Address ↑ConNF.α)), ConNF.Small S ∧ ∀ (ρ : ConNF.NewAllowable), (∀ c ∈ S, ρ • c = c) → ↑ρ ↑β • s = s) : ConNF.NewTSet

The main introduction rule for t-sets at level α.

Equations

• ConNF.NewTSet.intro s hs = ⟨ConNF.ExtensionalSet.intro' s, ⋯⟩

@[simp]

theorem ConNF.NewTSet.intro_members [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] (s : Set (ConNF.TSet ↑β)) (hs : ∃ (S : Set (ConNF.Address ↑ConNF.α)), ConNF.Small S ∧ ∀ (ρ : ConNF.NewAllowable), (∀ c ∈ S, ρ • c = c) → ↑ρ ↑β • s = s) : (↑(ConNF.NewTSet.intro s hs)).members β = s