Externalisation

In this file, we convert many of our internal results (i.e. inside the induction) to external ones (i.e. defined using the global TSet/AllPerm definitions).

Main declarations

• ConNF.foo: Something new.

instance ConNF.globalModelData [Params] {α : TypeIndex} : ModelData α

Equations

• ConNF.globalModelData = (ConNF.motive α).data
• ConNF.globalModelData = ConNF.botModelData

instance ConNF.globalPosition [Params] {α : TypeIndex} : Position (Tangle α)

Equations

• ConNF.globalPosition = (ConNF.motive α).pos
• ConNF.globalPosition = ConNF.botPosition

instance ConNF.globalTypedNearLitters [Params] {α : Λ} : TypedNearLitters α

Equations

• ConNF.globalTypedNearLitters = (ConNF.motive α).typed

instance ConNF.globalLtData [Params] [Level] : LtData

Equations

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

instance ConNF.globalLeData [Params] [Level] : LeData

Equations

• ConNF.globalLeData = { data := fun (β : ConNF.TypeIndex) [ConNF.LeLevel β] => ConNF.globalModelData, positions := fun (β : ConNF.TypeIndex) [ConNF.LtLevel β] => ConNF.globalPosition }

theorem ConNF.heq_funext {α : Sort u_1} {β γ : α → Sort u_2} {f : (x : α) → β x} {g : (x : α) → γ x} (h : ∀ (x : α), f x ≍ g x) : f ≍ g

theorem ConNF.globalLtData_eq [Params] [Level] : globalLtData = ltData fun (β : Λ) (x : ↑β < ↑α) => motive β

theorem ConNF.globalLeData_eq [Params] [Level] : globalLeData = leData fun (β : Λ) (x : ↑β < ↑α) => motive β

instance ConNF.globalPreCoherentData [Params] [Level] : PreCoherentData

Equations

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

@[simp]

theorem ConNF.heq_cast_eq_iff {α β γ : Type u_1} {x : α} {y : β} {h : α = γ} : cast h x ≍ y ↔ x ≍ y

theorem ConNF.globalPreCoherentData_eq [Params] [Level] : globalPreCoherentData = preCoherentData (fun (β : Λ) (x : ↑β < ↑α) => motive β) fun (β : Λ) (x : ↑β < ↑α) => hypothesis β

instance ConNF.globalCoherentData [Params] [Level] : CoherentData

Equations

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