Documentation

ConNF.Model.Externalise

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 #

source
instance ConNF.globalModelData [ConNF.Params] {α : ConNF.TypeIndex} :
ConNF.ModelData α
Equations
  • ConNF.globalModelData = (ConNF.motive α).data
  • ConNF.globalModelData = ConNF.botModelData
source
instance ConNF.globalPosition [ConNF.Params] {α : ConNF.TypeIndex} :
ConNF.Position (ConNF.Tangle α)
Equations
  • ConNF.globalPosition = (ConNF.motive α).pos
  • ConNF.globalPosition = ConNF.botPosition
source
instance ConNF.globalTypedNearLitters [ConNF.Params] {α : ConNF.Λ} :
ConNF.TypedNearLitters α
Equations
source
instance ConNF.globalLtData [ConNF.Params] [ConNF.Level] :
ConNF.LtData
Equations
  • ConNF.globalLtData = ConNF.LtData.mk
source
instance ConNF.globalLeData [ConNF.Params] [ConNF.Level] :
ConNF.LeData
Equations
  • ConNF.globalLeData = ConNF.LeData.mk
source
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
source
theorem ConNF.globalLtData_eq [ConNF.Params] [ConNF.Level] :
ConNF.globalLtData = ConNF.ltData fun (β : ConNF.Λ) (x : ↑β < ↑ConNF.α) => ConNF.motive β
source
theorem ConNF.globalLeData_eq [ConNF.Params] [ConNF.Level] :
ConNF.globalLeData = ConNF.leData fun (β : ConNF.Λ) (x : ↑β < ↑ConNF.α) => ConNF.motive β
source
instance ConNF.globalPreCoherentData [ConNF.Params] [ConNF.Level] :
ConNF.PreCoherentData
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem ConNF.heq_cast_eq_iff {α β γ : Type u_1} {x : α} {y : β} {h : α = γ} :
HEq (cast h x) y ↔ HEq x y
source
theorem ConNF.globalPreCoherentData_eq [ConNF.Params] [ConNF.Level] :
ConNF.globalPreCoherentData = ConNF.preCoherentData (fun (β : ConNF.Λ) (x : ↑β < ↑ConNF.α) => ConNF.motive β) fun (β : ConNF.Λ) (x : ↑β < ↑ConNF.α) => ConNF.hypothesis β
source
instance ConNF.globalCoherentData [ConNF.Params] [ConNF.Level] :
ConNF.CoherentData
Equations