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

• ConNF.globalLtData = ConNF.LtData.mk

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

Equations

• ConNF.globalLeData = ConNF.LeData.mk

theorem ConNF.heq_funext {α : Sort u_1} {β γ : α → Sort u_2} {f : (x : α) → β x} {g : (x : α) → γ x} (h : ∀ (x : α), HEq (f x) (g x)) : HEq 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 : α = γ} : HEq (cast h x) y ↔ HEq x y

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

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

Equations

• ConNF.globalCoherentData = ConNF.CoherentData.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯