Documentation

ConNF.Model.FOA

Restatement of freedom of action theorems #

source
def ConNF.MainInduction.FOA.instFOAData [ConNF.Params] [ConNF.Level] :
ConNF.FOAData
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev ConNF.MainInduction.FOA.foaAllowable [ConNF.Params] [ConNF.Level] (β : ConNF.TypeIndex) [ConNF.LeLevel β] :
    Type u

    Allowable β is defeq to foaAllowable β for every β : TypeIndex. However, it's not the case that Allowable is defeq to foaAllowable, because we need to pattern-match on its argument (i.e. check if it's ⊥) before we can establish the defeq.

    Equations
    Instances For
      source
      def ConNF.MainInduction.FOA.foaAllowableToStructPerm [ConNF.Params] [ConNF.Level] {β : ConNF.TypeIndex} [ConNF.LeLevel β] :
      ConNF.MainInduction.FOA.foaAllowable β →* ConNF.StructPerm β
      Equations
      • ConNF.MainInduction.FOA.foaAllowableToStructPerm = ConNF.ModelData.allowableToStructPerm
      Instances For
        source
        @[simp]
        theorem ConNF.MainInduction.FOA.foaAllowableToStructPerm_eq_coe [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [ConNF.LeLevel ↑β] :
        ConNF.MainInduction.FOA.foaAllowableToStructPerm = ConNF.Allowable.toStructPerm
        source
        @[simp]
        theorem ConNF.MainInduction.FOA.foaAllowableToStructPerm_eq_bot [ConNF.Params] [ConNF.Level] :
        ConNF.MainInduction.FOA.foaAllowableToStructPerm = ConNF.Allowable.toStructPerm
        source
        def ConNF.MainInduction.FOA.allowableCons [ConNF.Params] [ConNF.Level] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {γ : ConNF.TypeIndex} [ConNF.LeLevel γ] :
        γ < β → ConNF.MainInduction.FOA.foaAllowable β →* ConNF.MainInduction.FOA.foaAllowable γ
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem ConNF.MainInduction.FOA.allowableCons_eq_coe [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (hγ : ↑γ < ↑β) :
          ConNF.MainInduction.FOA.allowableCons hγ = ConNF.cons ⋯
          source
          @[simp]
          theorem ConNF.MainInduction.FOA.allowableCons_eq_bot [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [ConNF.LeLevel ↑β] :
          ConNF.MainInduction.FOA.allowableCons ⋯ = ConNF.cons' ⋯
          source
          theorem ConNF.MainInduction.FOA.allowableCons_eq [ConNF.Params] [ConNF.Level] (β : ConNF.TypeIndex) [iβ : ConNF.LeLevel β] (γ : ConNF.TypeIndex) [iγ : ConNF.LeLevel γ] (hγ : γ < β) (ρ : ConNF.MainInduction.FOA.foaAllowable β) :
          ConNF.Tree.comp (Quiver.Path.nil.cons hγ) (ConNF.MainInduction.FOA.foaAllowableToStructPerm ρ) = ConNF.MainInduction.FOA.foaAllowableToStructPerm ((ConNF.MainInduction.FOA.allowableCons hγ) ρ)
          source
          theorem ConNF.MainInduction.FOA.smul_fuzz_bot [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] (hδ : ↑δ < ↑β) (ρ : ConNF.MainInduction.FOA.foaAllowable ↑β) (t : ConNF.Tangle ⊥) :
          ConNF.MainInduction.FOA.foaAllowableToStructPerm ρ ((Quiver.Hom.toPath hδ).cons ⋯) • ConNF.fuzz ⋯ t = ConNF.fuzz ⋯ ((ConNF.MainInduction.FOA.allowableCons ⋯) ρ • t)
          source
          def ConNF.MainInduction.FOA.tangleEquiv' [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} (hγ : γ ≤ β) :
          ConNF.Tangle ↑γ ≃ ((ConNF.MainInduction.buildCumul β).ih γ hγ).Tangle
          Equations
          Instances For
            source
            def ConNF.MainInduction.FOA.allowableEquiv' [ConNF.Params] {β : ConNF.Λ} {γ : ConNF.Λ} (hγ : γ ≤ β) :
            ConNF.Allowable ↑γ ≃ ((ConNF.MainInduction.buildCumul β).ih γ hγ).Allowable
            Equations
            Instances For
              source
              theorem ConNF.MainInduction.FOA.smul_fuzz [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑β) (hγδ : ↑γ ≠ ↑δ) (ρ : ConNF.MainInduction.FOA.foaAllowable ↑β) (t : ConNF.Tangle ↑γ) :
              ConNF.MainInduction.FOA.foaAllowableToStructPerm ρ ((Quiver.Hom.toPath hδ).cons ⋯) • ConNF.fuzz hγδ t = ConNF.fuzz hγδ ((ConNF.MainInduction.FOA.allowableCons hγ) ρ • t)
              source
              theorem ConNF.MainInduction.FOA.allowable_of_smulFuzz [ConNF.Params] [ConNF.Level] (β : ConNF.Λ) [iβ : ConNF.LeLevel ↑β] (ρs : (γ : ConNF.Λ) → [inst : ConNF.LtLevel ↑γ] → ↑γ < ↑β → ConNF.MainInduction.FOA.foaAllowable ↑γ) (π : ConNF.BasePerm) :
              (∀ (γ : ConNF.Λ) [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.Λ) [inst : ConNF.LtLevel ↑δ] (hδ : ↑δ < ↑β) (a : ConNF.Atom), ConNF.Allowable.toStructPerm (ρs δ hδ) (Quiver.Hom.toPath ⋯) • ConNF.fuzz ⋯ a = ConNF.fuzz ⋯ (π • a)) → ∃ (ρ : ConNF.Allowable ↑β), (∀ (γ : ConNF.Λ) [inst : ConNF.LtLevel ↑γ] (hγ : ↑γ < ↑β), (ConNF.MainInduction.FOA.allowableCons hγ) ρ = ρs γ hγ) ∧ (ConNF.MainInduction.FOA.allowableCons ⋯) ρ = π
              source
              def ConNF.MainInduction.FOA.foaAssumptions [ConNF.Params] [ConNF.Level] :
              ConNF.FOAAssumptions
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem ConNF.MainInduction.FOA.exists_allowable_of_specifies [ConNF.Params] [ConNF.Level] {S : ConNF.Support ↑ConNF.α} {T : ConNF.Support ↑ConNF.α} (hS : S.Strong) (hT : T.Strong) {σ : ConNF.Spec ConNF.α} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT) :
                ∃ (ρ : ConNF.Allowable ↑ConNF.α), ρ • S = T