Structural sets

A structural set is an object of the supertype structure that our model resides inside. In this file, we define structural sets.

Main declarations

• ConNF.StructSet: The type of structural sets.

@[irreducible]

def ConNF.StructSet [ConNF.Params] : ConNF.TypeIndex → Type u

A structural set is an object that may become a t-set, an element of the model. The type of structural sets forms a model of TTT without extensionality.

Equations

• ConNF.StructSet none = ConNF.Atom
• ConNF.StructSet (some α) = ((β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StructSet β))

def ConNF.StructSet.toBot [ConNF.Params] : ConNF.Atom ≃ ConNF.StructSet ⊥

The "identity" equivalence between Atom and StructSet ⊥.

Equations

• ConNF.StructSet.toBot = Equiv.cast ⋯

def ConNF.StructSet.ofBot [ConNF.Params] : ConNF.StructSet ⊥ ≃ ConNF.Atom

The "identity" equivalence between StructSet ⊥ and Atom.

Equations

• ConNF.StructSet.ofBot = Equiv.cast ⋯

def ConNF.StructSet.toCoe [ConNF.Params] {α : ConNF.Λ} : ((β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StructSet β)) ≃ ConNF.StructSet ↑α

The "identity" equivalence between ∀ β < α, Set (StructSet β) and StructSet α.

Equations

• ConNF.StructSet.toCoe = Equiv.cast ⋯

def ConNF.StructSet.ofCoe [ConNF.Params] {α : ConNF.Λ} : ConNF.StructSet ↑α ≃ ((β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StructSet β))

The "identity" equivalence between StructSet α and ∀ β < α, Set (StructSet β).

Equations

• ConNF.StructSet.ofCoe = Equiv.cast ⋯

@[simp]

theorem ConNF.StructSet.toBot_symm [ConNF.Params] : ConNF.StructSet.toBot.symm = ConNF.StructSet.ofBot

@[simp]

theorem ConNF.StructSet.ofBot_symm [ConNF.Params] : ConNF.StructSet.ofBot.symm = ConNF.StructSet.toBot

@[simp]

theorem ConNF.StructSet.toCoe_symm [ConNF.Params] {α : ConNF.Λ} : ConNF.StructSet.toCoe.symm = ConNF.StructSet.ofCoe

@[simp]

theorem ConNF.StructSet.ofCoe_symm [ConNF.Params] {α : ConNF.Λ} : ConNF.StructSet.ofCoe.symm = ConNF.StructSet.toCoe

@[simp]

theorem ConNF.StructSet.toBot_ofBot [ConNF.Params] (a : ConNF.StructSet ⊥) : ConNF.StructSet.toBot (ConNF.StructSet.ofBot a) = a

@[simp]

theorem ConNF.StructSet.ofBot_toBot [ConNF.Params] (a : ConNF.Atom) : ConNF.StructSet.ofBot (ConNF.StructSet.toBot a) = a

@[simp]

theorem ConNF.StructSet.toCoe_ofCoe [ConNF.Params] {α : ConNF.Λ} (a : ConNF.StructSet ↑α) : ConNF.StructSet.toCoe (ConNF.StructSet.ofCoe a) = a

@[simp]

theorem ConNF.StructSet.ofCoe_toCoe [ConNF.Params] {α : ConNF.Λ} (a : (β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StructSet β)) : ConNF.StructSet.ofCoe (ConNF.StructSet.toCoe a) = a

@[simp]

theorem ConNF.StructSet.toBot_inj [ConNF.Params] {a : ConNF.Atom} {b : ConNF.Atom} : ConNF.StructSet.toBot a = ConNF.StructSet.toBot b ↔ a = b

@[simp]

theorem ConNF.StructSet.ofBot_inj [ConNF.Params] {a : ConNF.StructSet ⊥} {b : ConNF.StructSet ⊥} : ConNF.StructSet.ofBot a = ConNF.StructSet.ofBot b ↔ a = b

@[simp]

theorem ConNF.StructSet.toCoe_inj [ConNF.Params] {α : ConNF.Λ} {a : (β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StructSet β)} {b : (β : ConNF.TypeIndex) → β < ↑α → Set (ConNF.StructSet β)} : ConNF.StructSet.toCoe a = ConNF.StructSet.toCoe b ↔ a = b

@[simp]

theorem ConNF.StructSet.ofCoe_inj [ConNF.Params] {α : ConNF.Λ} {a : ConNF.StructSet ↑α} {b : ConNF.StructSet ↑α} : ConNF.StructSet.ofCoe a = ConNF.StructSet.ofCoe b ↔ a = b

theorem ConNF.StructSet.toBot_eq_iff [ConNF.Params] {a : ConNF.Atom} {b : ConNF.StructSet ⊥} : ConNF.StructSet.toBot a = b ↔ a = ConNF.StructSet.ofBot b

theorem ConNF.StructSet.ofBot_eq_iff [ConNF.Params] {a : ConNF.StructSet ⊥} {b : ConNF.Atom} : ConNF.StructSet.ofBot a = b ↔ a = ConNF.StructSet.toBot b

theorem ConNF.StructSet.coe_ext [ConNF.Params] {α : ConNF.Λ} {a : ConNF.StructSet ↑α} {b : ConNF.StructSet ↑α} : a = b ↔ ∀ (β : ConNF.TypeIndex) (hβ : β < ↑α) (t : ConNF.StructSet β), t ∈ ConNF.StructSet.ofCoe a β hβ ↔ t ∈ ConNF.StructSet.ofCoe b β hβ

Extensionality for structural sets at proper type indices. If two structural sets have the same extensions at every lower type index, then they are the same.