Documentation

ConNF.Coherent.CoherentData

Coherent data #

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

Main declarations #

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

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

A convenience typeclass to hold data below the current level.

Instances
    source
    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
    source
    instance ConNF.instModelDataOfLeDataOfLeLevel [ConNF.Params] [ConNF.Level] [ConNF.LeData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] :
    ConNF.ModelData β
    Equations
    • ConNF.instModelDataOfLeDataOfLeLevel = ConNF.LeData.data
    source
    instance ConNF.instPositionTangle [ConNF.Params] [ConNF.Level] [ConNF.LeData] (β : ConNF.TypeIndex) [ConNF.LtLevel β] :
    ConNF.Position (ConNF.Tangle β)
    Equations
    • ConNF.instPositionTangle = ConNF.LeData.positions
    source
    class ConNF.PreCoherentData [ConNF.Params] [ConNF.Level] extends ConNF.LeData :
    Type (u + 1)
    Instances
      source
      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
      source
      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.
      source
      @[simp]
      theorem ConNF.allPerm_deriv_nil [ConNF.Params] [ConNF.Level] [ConNF.PreCoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ρ : ConNF.AllPerm β) :
      ρ ⇘ ConNF.Path.nil = ρ
      source
      @[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
      source
      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ᵁ
      Instances
        source
        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
        source
        @[simp]
        theorem ConNF.allPermDeriv_forget [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.TypeIndex} [ConNF.LeLevel β] [iγ : ConNF.LeLevel γ] (A : β ↝ γ) (ρ : ConNF.AllPerm β) :
        (ρ ⇘ A)ᵁ = ρᵁ ⇘ A
        source
        theorem ConNF.allPerm_inv_sderiv [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β γ : ConNF.TypeIndex} [ConNF.LeLevel β] [iγ : ConNF.LeLevel γ] (h : γ < β) (ρ : ConNF.AllPerm β) :
        ρ⁻¹ ↘ h = (ρ ↘ h)⁻¹
        source
        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