Hypotheses

class ConNF.CountingAssumptions [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] extends ConNF.FOAAssumptions : Type (u + 1)

• lowerModelData : (β : ConNF.Λ) → [inst : ConNF.LeLevel ↑β] → ConNF.ModelData ↑β
• lowerPositionedTangles : (β : ConNF.Λ) → [inst : ConNF.LtLevel ↑β] → ConNF.PositionedTangles ↑β
• lowerTypedObjects : (β : ConNF.Λ) → [inst : ConNF.LeLevel ↑β] → ConNF.TypedObjects β
• lowerPositionedObjects : ∀ (β : ConNF.Λ) [inst : ConNF.LtLevel ↑β], ConNF.PositionedObjects β
• allowableCons : {β : ConNF.TypeIndex} → [inst : ConNF.LeLevel β] → {γ : ConNF.TypeIndex} → [inst_1 : ConNF.LeLevel γ] → γ < β → ConNF.Allowable β →* ConNF.Allowable γ
• allowableCons_eq : ∀ (β : ConNF.TypeIndex) [inst : ConNF.LeLevel β] (γ : ConNF.TypeIndex) [inst_1 : ConNF.LeLevel γ] (hγ : γ < β) (ρ : ConNF.Allowable β), ConNF.Tree.comp (Quiver.Path.nil.cons hγ) (ConNF.Allowable.toStructPerm ρ) = ConNF.Allowable.toStructPerm ((ConNF.allowableCons hγ) ρ)
• pos_lt_pos_atom : ∀ {β : ConNF.Λ} [inst : ConNF.LtLevel ↑β] (t : ConNF.Tangle ↑β) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom}, { path := A, value := Sum.inl a } ∈ t.support → ConNF.pos a < ConNF.pos t
• pos_lt_pos_nearLitter : ∀ {β : ConNF.Λ} [inst : ConNF.LtLevel ↑β] (t : ConNF.Tangle ↑β) {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter}, { path := A, value := Sum.inr N } ∈ t.support → t.set ≠ ConNF.typedNearLitter N → ConNF.pos N < ConNF.pos t
• smul_fuzz : ∀ {β : ConNF.TypeIndex} [inst : ConNF.LeLevel β] {γ : ConNF.TypeIndex} [inst_1 : ConNF.LtLevel γ] {δ : ConNF.Λ} [inst_2 : ConNF.LtLevel ↑δ] (hγ : γ < β) (hδ : ↑δ < β) (hγδ : γ ≠ ↑δ) (ρ : ConNF.Allowable β) (t : ConNF.Tangle γ), ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).cons ⋯) • ConNF.fuzz hγδ t = ConNF.fuzz hγδ ((ConNF.allowableCons hγ) ρ • t)
• allowable_of_smulFuzz : ∀ (β : ConNF.Λ) [inst : ConNF.LeLevel ↑β] (ρs : (γ : ConNF.TypeIndex) → [inst : ConNF.LtLevel γ] → γ < ↑β → ConNF.Allowable γ), (∀ (γ : ConNF.TypeIndex) [inst : ConNF.LtLevel γ] (δ : ConNF.Λ) [inst_1 : ConNF.LtLevel ↑δ] (hγ : γ < ↑β) (hδ : ↑δ < ↑β) (hγδ : γ ≠ ↑δ) (t : ConNF.Tangle γ), ConNF.Allowable.toStructPerm (ρs (↑δ) hδ) (Quiver.Hom.toPath ⋯) • ConNF.fuzz hγδ t = ConNF.fuzz hγδ (ρs γ hγ • t)) → ∃ (ρ : ConNF.Allowable ↑β), ∀ (γ : ConNF.TypeIndex) [inst_1 : ConNF.LtLevel γ] (hγ : γ < ↑β), (ConNF.allowableCons hγ) ρ = ρs γ hγ
• eq_toStructSet_of_mem : ∀ (β : ConNF.Λ) [inst : ConNF.LeLevel ↑β] (γ : ConNF.Λ) [inst_1 : ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) (t₁ : ConNF.TSet ↑β), ∀ t₂ ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₁) (↑γ) h, ∃ (t₂' : ConNF.TSet ↑γ), t₂ = ConNF.toStructSet t₂'

  Tangles contain only tangles.

• toStructSet_ext : ∀ (β γ : ConNF.Λ) [inst : ConNF.LeLevel ↑β] [inst_1 : ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) (t₁ t₂ : ConNF.TSet ↑β), (∀ (t : ConNF.StructSet ↑γ), t ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₁) (↑γ) h ↔ t ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₂) (↑γ) h) → ConNF.toStructSet t₁ = ConNF.toStructSet t₂

  Tangles are extensional at every proper level γ < β.

• singleton : (β : ConNF.Λ) → [inst : ConNF.LeLevel ↑β] → (γ : ConNF.Λ) → [inst_1 : ConNF.LeLevel ↑γ] → ↑γ < ↑β → ConNF.TSet ↑γ → ConNF.TSet ↑β

  Any γ-tangle can be treated as a singleton at level β if γ < β.

• singleton_toStructSet : ∀ (β : ConNF.Λ) [inst : ConNF.LeLevel ↑β] (γ : ConNF.Λ) [inst_1 : ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) (t : ConNF.TSet ↑γ), ConNF.StructSet.ofCoe (ConNF.toStructSet (ConNF.singleton β γ h t)) (↑γ) h = {ConNF.toStructSet t}

theorem ConNF.CountingAssumptions.eq_toStructSet_of_mem [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.CountingAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] (γ : ConNF.Λ) [ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.StructSet ↑γ) : t₂ ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₁) (↑γ) h → ∃ (t₂' : ConNF.TSet ↑γ), t₂ = ConNF.toStructSet t₂'

Tangles contain only tangles.

theorem ConNF.CountingAssumptions.toStructSet_ext [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.CountingAssumptions] (β : ConNF.Λ) (γ : ConNF.Λ) [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) (t₁ : ConNF.TSet ↑β) (t₂ : ConNF.TSet ↑β) : (∀ (t : ConNF.StructSet ↑γ), t ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₁) (↑γ) h ↔ t ∈ ConNF.StructSet.ofCoe (ConNF.toStructSet t₂) (↑γ) h) → ConNF.toStructSet t₁ = ConNF.toStructSet t₂

Tangles are extensional at every proper level γ < β.

theorem ConNF.CountingAssumptions.singleton_toStructSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [self : ConNF.CountingAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] (γ : ConNF.Λ) [ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) (t : ConNF.TSet ↑γ) : ConNF.StructSet.ofCoe (ConNF.toStructSet (ConNF.singleton β γ h t)) (↑γ) h = {ConNF.toStructSet t}

theorem ConNF.singleton_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.CountingAssumptions] (β : ConNF.Λ) (γ : ConNF.Λ) [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) (t : ConNF.TSet ↑γ) (ρ : ConNF.Allowable ↑β) : ρ • ConNF.singleton β γ h t = ConNF.singleton β γ h ((ConNF.Allowable.comp (Quiver.Hom.toPath h)) ρ • t)

theorem ConNF.singleton_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.CountingAssumptions] (β : ConNF.Λ) (γ : ConNF.Λ) [ConNF.LeLevel ↑β] [ConNF.LeLevel ↑γ] (h : ↑γ < ↑β) : Function.Injective (ConNF.singleton β γ h)