Coherent data

In this file, we define the type of coherent data below a particular proper type index.

Main declarations

• ConNF.ModelDataData: Coherent data below a given level α.

TODO: We're going to try allowing model data at level ⊥ to vary. That is, we use (β : TypeIndex) → [LeLevel β] → ModelData β instead of (β : Λ) → [LeLevel β] → ModelData β.

class ConNF.LeData [ConNF.Params] [ConNF.Level] : Type (u + 1)

A convenience typeclass to hold data below the current level.

• data : (β : ConNF.TypeIndex) → [inst : ConNF.LeLevel β] → ConNF.ModelData β
• positions : (β : ConNF.TypeIndex) → [inst : ConNF.LtLevel β] → ConNF.Position (ConNF.Tangle β)

theorem ConNF.LeData.ext {inst✝ : ConNF.Params} {inst✝¹ : ConNF.Level} {x y : ConNF.LeData} (data : ConNF.LeData.data = ConNF.LeData.data) (positions : HEq ConNF.LeData.positions ConNF.LeData.positions) : x = y

instance ConNF.instModelDataOfLeDataOfLeLevel [ConNF.Params] [ConNF.Level] [ConNF.LeData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : ConNF.ModelData β

Equations

• ConNF.instModelDataOfLeDataOfLeLevel = ConNF.LeData.data

instance ConNF.instPositionTangle [ConNF.Params] [ConNF.Level] [ConNF.LeData] (β : ConNF.TypeIndex) [ConNF.LtLevel β] : ConNF.Position (ConNF.Tangle β)

Equations

• ConNF.instPositionTangle = ConNF.LeData.positions

class ConNF.PreCoherentData [ConNF.Params] [ConNF.Level] extends ConNF.LeData : Type (u + 1)

• data : (β : ConNF.TypeIndex) → [inst : ConNF.LeLevel β] → ConNF.ModelData β
• positions : (β : ConNF.TypeIndex) → [inst : ConNF.LtLevel β] → ConNF.Position (ConNF.Tangle β)
• allPermSderiv : {β γ : ConNF.TypeIndex} → [inst : ConNF.LeLevel β] → [inst_1 : ConNF.LeLevel γ] → γ < β → ConNF.AllPerm β → ConNF.AllPerm γ
• singleton : {β γ : ConNF.Λ} → [inst : ConNF.LeLevel ↑β] → [inst_1 : ConNF.LeLevel ↑γ] → ↑γ < ↑β → ConNF.TSet ↑γ → ConNF.TSet ↑β

theorem ConNF.PreCoherentData.ext {inst✝ : ConNF.Params} {inst✝¹ : ConNF.Level} {x y : ConNF.PreCoherentData} (data : ConNF.LeData.data = ConNF.LeData.data) (positions : HEq ConNF.LeData.positions ConNF.LeData.positions) (allPermSderiv : HEq (@ConNF.PreCoherentData.allPermSderiv inst✝ inst✝¹ x) (@ConNF.PreCoherentData.allPermSderiv inst✝ inst✝¹ y)) (singleton : HEq (@ConNF.singleton inst✝ inst✝¹ x) (@ConNF.singleton inst✝ inst✝¹ y)) : x = y

instance ConNF.instDerivativeAllPerm [ConNF.Params] [ConNF.Level] [ConNF.PreCoherentData] {β γ : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.LeLevel γ] : ConNF.Derivative (ConNF.AllPerm β) (ConNF.AllPerm γ) β γ

Equations

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

@[simp]

theorem ConNF.allPerm_deriv_nil [ConNF.Params] [ConNF.Level] [ConNF.PreCoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ρ : ConNF.AllPerm β) : ρ ⇘ ConNF.Path.nil = ρ

@[simp]

theorem ConNF.allPerm_deriv_sderiv [ConNF.Params] [ConNF.Level] [ConNF.PreCoherentData] {β γ δ : ConNF.TypeIndex} [ConNF.LeLevel β] [ConNF.LeLevel γ] [ConNF.LeLevel δ] (ρ : ConNF.AllPerm β) (A : β ↝ γ) (h : δ < γ) : ρ ⇘ (A ↘ h) = ρ ⇘ A ↘ h

class ConNF.CoherentData [ConNF.Params] [ConNF.Level] extends ConNF.PreCoherentData : Type (u + 1)

Note that in earlier versions of the proof we additionally used the following assumption.

typedMem_tSetForget {β : Λ} {γ : TypeIndex} [LeLevel β] [LeLevel γ]
  (hγ : γ < β) (x : TSet β) (y : StrSet γ) :
  y ∈[hγ] xᵁ → ∃ z : TSet γ, y = zᵁ

• data : (β : ConNF.TypeIndex) → [inst : ConNF.LeLevel β] → ConNF.ModelData β
• positions : (β : ConNF.TypeIndex) → [inst : ConNF.LtLevel β] → ConNF.Position (ConNF.Tangle β)
• allPermSderiv : {β γ : ConNF.TypeIndex} → [inst : ConNF.LeLevel β] → [inst_1 : ConNF.LeLevel γ] → γ < β → ConNF.AllPerm β → ConNF.AllPerm γ
• singleton : {β γ : ConNF.Λ} → [inst : ConNF.LeLevel ↑β] → [inst_1 : ConNF.LeLevel ↑γ] → ↑γ < ↑β → ConNF.TSet ↑γ → ConNF.TSet ↑β
• allPermSderiv_forget : ∀ {β γ : ConNF.TypeIndex} [inst : ConNF.LeLevel β] [inst_1 : ConNF.LeLevel γ] (h : γ < β) (ρ : ConNF.AllPerm β), (ρ ↘ h)ᵁ = ρᵁ ↘ h
• pos_atom_lt_pos : ∀ {β : ConNF.TypeIndex} [inst : ConNF.LtLevel β] (t : ConNF.Tangle β) (A : β ↝ ⊥), ∀ a ∈ (t.support ⇘. A)ᴬ, ConNF.pos a < ConNF.pos t
• pos_nearLitter_lt_pos : ∀ {β : ConNF.TypeIndex} [inst : ConNF.LtLevel β] (t : ConNF.Tangle β) (A : β ↝ ⊥), ∀ N ∈ (t.support ⇘. A)ᴺ, ConNF.pos N < ConNF.pos t
• smul_fuzz : ∀ {γ : ConNF.Λ} {δ : ConNF.TypeIndex} {ε : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] [inst_1 : ConNF.LtLevel δ] [inst_2 : ConNF.LtLevel ↑ε] (hδ : δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : δ ≠ ↑ε) (ρ : ConNF.AllPerm ↑γ) (t : ConNF.Tangle δ), ρᵁ ↘ hε ↘. • ConNF.fuzz hδε t = ConNF.fuzz hδε (ρ ↘ hδ • t)
• allPerm_of_basePerm : ∀ (π : ConNF.BasePerm), ∃ (ρ : ConNF.AllPerm ⊥), ρᵁ ConNF.Path.nil = π
• allPerm_of_smulFuzz : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (ρs : {δ : ConNF.TypeIndex} → [inst : ConNF.LtLevel δ] → δ < ↑γ → ConNF.AllPerm δ), (∀ {δ : ConNF.TypeIndex} {ε : ConNF.Λ} [inst : ConNF.LtLevel δ] [inst_1 : ConNF.LtLevel ↑ε] (hδ : δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : δ ≠ ↑ε) (t : ConNF.Tangle δ), (ρs hε)ᵁ ↘. • ConNF.fuzz hδε t = ConNF.fuzz hδε (ρs hδ • t)) → ∃ (ρ : ConNF.AllPerm ↑γ), ∀ (δ : ConNF.TypeIndex) [inst_1 : ConNF.LtLevel δ] (hδ : δ < ↑γ), ρ ↘ hδ = ρs hδ
• tSet_ext : ∀ {β γ : ConNF.Λ} [inst : ConNF.LeLevel ↑β] [inst_1 : ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (x y : ConNF.TSet ↑β), (∀ (z : ConNF.TSet ↑γ), z ∈[hγ] x ↔ z ∈[hγ] y) → x = y
• typedMem_singleton_iff : ∀ {β γ : ConNF.Λ} [inst : ConNF.LeLevel ↑β] [inst_1 : ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) (x y : ConNF.TSet ↑γ), y ∈[hγ] ConNF.singleton hγ x ↔ y = x

theorem ConNF.CoherentData.ext {inst✝ : ConNF.Params} {inst✝¹ : ConNF.Level} {x y : ConNF.CoherentData} (data : ConNF.LeData.data = ConNF.LeData.data) (positions : HEq ConNF.LeData.positions ConNF.LeData.positions) (allPermSderiv : HEq (@ConNF.PreCoherentData.allPermSderiv inst✝ inst✝¹ ConNF.CoherentData.toPreCoherentData) (@ConNF.PreCoherentData.allPermSderiv inst✝ inst✝¹ ConNF.CoherentData.toPreCoherentData)) (singleton : HEq (@ConNF.singleton inst✝ inst✝¹ ConNF.CoherentData.toPreCoherentData) (@ConNF.singleton inst✝ inst✝¹ ConNF.CoherentData.toPreCoherentData)) : x = y

@[simp]

theorem ConNF.allPermDeriv_forget [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.TypeIndex} [ConNF.LeLevel β] [iγ : ConNF.LeLevel γ] (A : β ↝ γ) (ρ : ConNF.AllPerm β) : (ρ ⇘ A)ᵁ = ρᵁ ⇘ A

theorem ConNF.allPerm_inv_sderiv [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.TypeIndex} [ConNF.LeLevel β] [iγ : ConNF.LeLevel γ] (h : γ < β) (ρ : ConNF.AllPerm β) : ρ⁻¹ ↘ h = (ρ ↘ h)⁻¹

theorem ConNF.TSet.mem_smul_iff [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.TypeIndex} [ConNF.LeLevel β] [iγ : ConNF.LeLevel γ] {x : ConNF.TSet γ} {y : ConNF.TSet β} (h : γ < β) (ρ : ConNF.AllPerm β) : x ∈[h] ρ • y ↔ ρ⁻¹ ↘ h • x ∈[h] y