Atoms #

In this file, we define atoms: the elements of the base type of our model. They are not atoms in the ZFU sense (for example), they are simply the elements of the model which are in type τ₋₁.

This base type does not appear in the final construction, it is just used as the foundation on which the subsequent layers can be built.

Main declarations #

ConNF.Atom: The type of atoms.

source

def ConNF.Atom [ConNF.Params] :

Type u

The base type of the construction, denoted by τ₋₁ in various papers. Instead of declaring it as an arbitrary type of cardinality μ and partitioning it into suitable sets of litters afterwards, we define it as Litter × κ, which has the correct cardinality and comes with a natural partition.

These are not 'atoms' in the ZFU, TTTU or NFU sense; they are simply the elements of the model which are in type τ₋₁.

Equations

ConNF.Atom = (ConNF.Litter × ConNF.κ)

Instances For

source

instance ConNF.instNonemptyAtom [ConNF.Params] :

Nonempty ConNF.Atom

Equations

⋯ = ⋯

source

@[simp]

theorem ConNF.mk_atom [ConNF.Params] :

Cardinal.mk ConNF.Atom = Cardinal.mk ConNF.μ

The cardinality of Atom is the cardinality of μ. We will prove that all types constructed in our model have cardinality equal to μ.

source

def ConNF.litterSet [ConNF.Params] (L : ConNF.Litter) :

Set ConNF.Atom

The set corresponding to litter L. We define a litter set as the set of atoms with first projection L.

Equations

ConNF.litterSet L = {a : ConNF.Atom | a.1 = L}

Instances For

source

@[simp]

theorem ConNF.mem_litterSet [ConNF.Params] {a : ConNF.Atom} {L : ConNF.Litter} :

a ∈ ConNF.litterSet L ↔ a.1 = L

source

def ConNF.litterSetEquiv [ConNF.Params] (L : ConNF.Litter) :

↑(ConNF.litterSet L) ≃ ConNF.κ

Each litter set is equivalent as a type to κ.

Equations

ConNF.litterSetEquiv L = { toFun := fun (x : ↑(ConNF.litterSet L)) => (↑x).2, invFun := fun (k : ConNF.κ) => ⟨(L, k), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }