New file

In this file...

Main declarations

• ConNF.foo: Something new.

structure ConNF.InflexiblePath [ConNF.Params] (β : ConNF.TypeIndex) : Type u

• γ : ConNF.Λ
• δ : ConNF.TypeIndex
• ε : ConNF.Λ
• hδ : self.δ < ↑self.γ
• hε : ↑self.ε < ↑self.γ
• hδε : self.δ ≠ ↑self.ε
• A : β ↝ ↑self.γ

theorem ConNF.InflexiblePath.ext {inst✝ : ConNF.Params} {β : ConNF.TypeIndex} {x y : ConNF.InflexiblePath β} (γ : x.γ = y.γ) (δ : x.δ = y.δ) (ε : x.ε = y.ε) (A : HEq x.A y.A) : x = y

instance ConNF.instCoderivativeInflexiblePath [ConNF.Params] {β β' : ConNF.TypeIndex} : ConNF.Coderivative (ConNF.InflexiblePath β) (ConNF.InflexiblePath β') β' β

Equations

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

@[simp]

theorem ConNF.InflexiblePath.coderiv_A [ConNF.Params] {β β' : ConNF.TypeIndex} (P : ConNF.InflexiblePath β) (B : β' ↝ β) : (P ⇗ B).A = B ⇘ P.A

theorem ConNF.instLeLevelSomeΛγ [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.LeLevel β] (P : ConNF.InflexiblePath β) : ConNF.LeLevel ↑P.γ

theorem ConNF.instLtLevelδOfLeLevel [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.LeLevel β] (P : ConNF.InflexiblePath β) : ConNF.LtLevel P.δ

theorem ConNF.instLtLevelSomeΛεOfLeLevel [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.LeLevel β] (P : ConNF.InflexiblePath β) : ConNF.LtLevel ↑P.ε

def ConNF.Inflexible [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (A : β ↝ ⊥) (L : ConNF.Litter) : Prop

Equations

• ConNF.Inflexible A L = ∃ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ L = ConNF.fuzz ⋯ t

theorem ConNF.inflexible_iff [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (A : β ↝ ⊥) (L : ConNF.Litter) : ConNF.Inflexible A L ↔ ∃ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ L = ConNF.fuzz ⋯ t

theorem ConNF.not_inflexible_iff [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (A : β ↝ ⊥) (L : ConNF.Litter) : ¬ConNF.Inflexible A L ↔ ∀ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. → L ≠ ConNF.fuzz ⋯ t

theorem ConNF.inflexible_deriv [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {A : β ↝ ⊥} {L : ConNF.Litter} (h : ConNF.Inflexible A L) {β' : ConNF.TypeIndex} [ConNF.LeLevel β'] (B : β' ↝ β) : ConNF.Inflexible (B ⇘ A) L

theorem ConNF.inflexible_cases [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (A : β ↝ ⊥) (L : ConNF.Litter) : (∃ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ L = ConNF.fuzz ⋯ t) ∨ ¬ConNF.Inflexible A L

theorem ConNF.inflexiblePath_subsingleton [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {A : β ↝ ⊥} {L : ConNF.Litter} {P₁ P₂ : ConNF.InflexiblePath β} {t₁ : ConNF.Tangle P₁.δ} {t₂ : ConNF.Tangle P₂.δ} (hP₁ : A = P₁.A ↘ ⋯ ↘.) (hP₂ : A = P₂.A ↘ ⋯ ↘.) (ht₁ : L = ConNF.fuzz ⋯ t₁) (ht₂ : L = ConNF.fuzz ⋯ t₂) : P₁ = P₂

def ConNF.inflexiblePathEmbedding [ConNF.Params] {β : ConNF.TypeIndex} : ConNF.InflexiblePath β ↪ ↑(Set.Iic β) × ↑(Set.Iic β) × (γ : ConNF.TypeIndex) × β ↝ γ

Equations

• ConNF.inflexiblePathEmbedding = { toFun := fun (P : ConNF.InflexiblePath β) => (⟨P.δ, ⋯⟩, ⟨↑P.ε, ⋯⟩, ⟨↑P.γ, P.A⟩), inj' := ⋯ }

theorem ConNF.card_inflexiblePath_lt [ConNF.Params] (β : ConNF.TypeIndex) : Cardinal.mk (ConNF.InflexiblePath β) < (Cardinal.mk ConNF.μ).ord.cof