Codes

In this file, we define codes representing t-sets of type α.

Main declarations

• ConNF.Code: Codes representing t-sets at type α.
• ConNF.NonemptyCode: Nonempty α-codes.

theorem ConNF.Code.ext_iff : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} {inst_2 : ConNF.ModelDataLt} (x y : ConNF.Code), x = y ↔ x.β = y.β ∧ HEq x.members y.members

theorem ConNF.Code.ext : ∀ {inst : ConNF.Params} {inst_1 : ConNF.Level} {inst_2 : ConNF.ModelDataLt} (x y : ConNF.Code), x.β = y.β → HEq x.members y.members → x = y

structure ConNF.Code [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Type u

An α code is a type index β < α together with a set of tangles of type β. There is at most one t-set with this code. Any t-set has exactly one code for each proper type index β < α, and possibly a code for β = ⊥.

• β : ConNF.TypeIndex
• inst : ConNF.LtLevel self.β
• members : Set (ConNF.TSet self.β)

theorem ConNF.Code.inst [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (self : ConNF.Code) : ConNF.LtLevel self.β

instance ConNF.instLtLevelβ [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (c : ConNF.Code) : ConNF.LtLevel c.β

Equations

• ⋯ = ⋯

instance ConNF.instInhabitedCode [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Inhabited ConNF.Code

Equations

• ConNF.instInhabitedCode = { default := ConNF.Code.mk ⊥ ∅ }

@[reducible, inline]

abbrev ConNF.NonemptyCode [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] : Type u

Nonempty codes.

Equations

• ConNF.NonemptyCode = { c : ConNF.Code // c.members.Nonempty }

def ConNF.Code.IsEmpty [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] (c : ConNF.Code) : Prop

A code is empty if it has no element.

Equations

• c.IsEmpty = (c.members = ∅)

theorem ConNF.Code.IsEmpty.eq [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {c : ConNF.Code} : c.IsEmpty → c.members = ∅

@[simp]

theorem ConNF.Code.isEmpty_mk [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {s : Set (ConNF.TSet ↑β)} : (ConNF.Code.mk (↑β) s).IsEmpty ↔ s = ∅

@[simp]

theorem ConNF.Code.mk_inj [ConNF.Params] [ConNF.Level] [ConNF.ModelDataLt] {β : ConNF.Λ} [ConNF.LtLevel ↑β] {s : Set (ConNF.TSet ↑β)} {t : Set (ConNF.TSet ↑β)} : ConNF.Code.mk (↑β) s = ConNF.Code.mk (↑β) t ↔ s = t