Model parameters

In this file, we define the parameters that we will use to construct our model of tangled type theory.

Main declarations

• ConNF.Params: The type of model parameters.

class ConNF.Params : Type (u + 1)

• Λ : Type u
• κ : Type u
• μ : Type u
• Λ_nonempty : Nonempty ConNF.Λ
• ΛWellOrder : LtWellOrder ConNF.Λ
• Λ_noMaxOrder : NoMaxOrder ConNF.Λ
• aleph0_lt_κ : Cardinal.aleph0 < Cardinal.mk ConNF.κ
• κ_isRegular : (Cardinal.mk ConNF.κ).IsRegular
• μ_isStrongLimit : (Cardinal.mk ConNF.μ).IsStrongLimit
• κ_lt_μ : Cardinal.mk ConNF.κ < Cardinal.mk ConNF.μ
• κ_le_μ_ord_cof : Cardinal.mk ConNF.κ ≤ (Cardinal.mk ConNF.μ).ord.cof
• Λ_type_le_μ_ord_cof : (Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2) ≤ (Cardinal.mk ConNF.μ).ord.cof.ord

def ConNF.Params.minimal : ConNF.Params

Equations

• One or more equations did not get rendered due to their size.

def ConNF.Params.inaccessible : ConNF.Params

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.instNonemptyΛ [ConNF.Params] : Nonempty ConNF.Λ

instance ConNF.instLtWellOrderΛ [ConNF.Params] : LtWellOrder ConNF.Λ

Equations

• ConNF.instLtWellOrderΛ = ConNF.Params.ΛWellOrder

theorem ConNF.instNoMaxOrderΛ [ConNF.Params] : NoMaxOrder ConNF.Λ

instance ConNF.instWellFoundedRelationΛ [ConNF.Params] : WellFoundedRelation ConNF.Λ

Allows us to use termination_by clauses with Λ.

Equations

• ConNF.instWellFoundedRelationΛ = { rel := fun (x1 x2 : ConNF.Λ) => x1 < x2, wf := ⋯ }

theorem ConNF.aleph0_lt_μ [ConNF.Params] : Cardinal.aleph0 < Cardinal.mk ConNF.μ

theorem ConNF.aleph0_lt_μ_ord_cof [ConNF.Params] : Cardinal.aleph0 < (Cardinal.mk ConNF.μ).ord.cof

theorem ConNF.Λ_type_le_μ_ord [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2) ≤ (Cardinal.mk ConNF.μ).ord

theorem ConNF.Λ_le_cof_μ [ConNF.Params] : Cardinal.mk ConNF.Λ ≤ (Cardinal.mk ConNF.μ).ord.cof

theorem ConNF.Λ_le_μ [ConNF.Params] : Cardinal.mk ConNF.Λ ≤ Cardinal.mk ConNF.μ

theorem ConNF.κ_le_μ [ConNF.Params] : Cardinal.mk ConNF.κ ≤ Cardinal.mk ConNF.μ

@[irreducible]

def ConNF.κEquiv [ConNF.Params] : ConNF.κ ≃ ↑(Set.Iio (Cardinal.mk ConNF.κ).ord)

Equations

• ConNF.κEquiv = Equiv.ulift.symm.trans ⋯.some

@[irreducible]

def ConNF.μEquiv [ConNF.Params] : ConNF.μ ≃ ↑(Set.Iio (Cardinal.mk ConNF.μ).ord)

Equations

• ConNF.μEquiv = Equiv.ulift.symm.trans ⋯.some

instance ConNF.instLtWellOrderκ [ConNF.Params] : LtWellOrder ConNF.κ

Equations

• ConNF.instLtWellOrderκ = ConNF.κEquiv.ltWellOrder

instance ConNF.instOfNatκ [ConNF.Params] (n : ℕ) : OfNat ConNF.κ n

Equations

• ConNF.instOfNatκ n = ConNF.κEquiv.ofNat n

theorem ConNF.instNoMaxOrderκ [ConNF.Params] : NoMaxOrder ConNF.κ

instance ConNF.instLtWellOrderμ [ConNF.Params] : LtWellOrder ConNF.μ

Equations

• ConNF.instLtWellOrderμ = ConNF.μEquiv.ltWellOrder

theorem ConNF.instNoMaxOrderμ [ConNF.Params] : NoMaxOrder ConNF.μ

theorem ConNF.instInfiniteΛ [ConNF.Params] : Infinite ConNF.Λ

theorem ConNF.instInfiniteκ [ConNF.Params] : Infinite ConNF.κ

theorem ConNF.instInfiniteμ [ConNF.Params] : Infinite ConNF.μ

theorem ConNF.Λ_type_isLimit [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2).IsLimit

@[simp]

theorem ConNF.κ_type [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.κ) => x1 < x2) = (Cardinal.mk ConNF.κ).ord

@[simp]

theorem ConNF.μ_type [ConNF.Params] : (Ordinal.type fun (x1 x2 : ConNF.μ) => x1 < x2) = (Cardinal.mk ConNF.μ).ord

instance ConNF.instAddMonoidκ [ConNF.Params] : AddMonoid ConNF.κ

Equations

• ConNF.instAddMonoidκ = ConNF.κEquiv.addMonoid

instance ConNF.instSubκ [ConNF.Params] : Sub ConNF.κ

Equations

• ConNF.instSubκ = ConNF.κEquiv.sub

theorem ConNF.κ_ofNat_def [ConNF.Params] (n : ℕ) : OfNat.ofNat n = ConNF.κEquiv.symm (OfNat.ofNat n)

theorem ConNF.κ_add_def [ConNF.Params] (x y : ConNF.κ) : x + y = ConNF.κEquiv.symm (ConNF.κEquiv x + ConNF.κEquiv y)

theorem ConNF.κ_sub_def [ConNF.Params] (x y : ConNF.κ) : x - y = ConNF.κEquiv.symm (ConNF.κEquiv x - ConNF.κEquiv y)

theorem ConNF.κEquiv_ofNat [ConNF.Params] (n : ℕ) : ↑(ConNF.κEquiv (OfNat.ofNat n)) = ↑n

theorem ConNF.κEquiv_add [ConNF.Params] (x y : ConNF.κ) : ↑(ConNF.κEquiv (x + y)) = ↑(ConNF.κEquiv x) + ↑(ConNF.κEquiv y)

theorem ConNF.κEquiv_sub [ConNF.Params] (x y : ConNF.κ) : ↑(ConNF.κEquiv (x - y)) = ↑(ConNF.κEquiv x) - ↑(ConNF.κEquiv y)

theorem ConNF.κEquiv_lt [ConNF.Params] (x y : ConNF.κ) : x < y ↔ ConNF.κEquiv x < ConNF.κEquiv y

theorem ConNF.κEquiv_le [ConNF.Params] (x y : ConNF.κ) : x ≤ y ↔ ConNF.κEquiv x ≤ ConNF.κEquiv y

theorem ConNF.κ_zero_le [ConNF.Params] (x : ConNF.κ) : 0 ≤ x

theorem ConNF.instCovariantClassκHAddLe [ConNF.Params] : CovariantClass ConNF.κ ConNF.κ (fun (x1 x2 : ConNF.κ) => x1 + x2) fun (x1 x2 : ConNF.κ) => x1 ≤ x2

theorem ConNF.instCovariantClassκHAddLt [ConNF.Params] : CovariantClass ConNF.κ ConNF.κ (fun (x1 x2 : ConNF.κ) => x1 + x2) fun (x1 x2 : ConNF.κ) => x1 < x2

theorem ConNF.instCovariantClassκSwapHAddLe [ConNF.Params] : CovariantClass ConNF.κ ConNF.κ (Function.swap fun (x1 x2 : ConNF.κ) => x1 + x2) fun (x1 x2 : ConNF.κ) => x1 ≤ x2

theorem ConNF.κ_le_add [ConNF.Params] (x y : ConNF.κ) : x ≤ x + y

theorem ConNF.instIsLeftCancelAddκ [ConNF.Params] : IsLeftCancelAdd ConNF.κ

theorem ConNF.κ_typein [ConNF.Params] (x : ConNF.κ) : (Ordinal.typein fun (x1 x2 : ConNF.κ) => x1 < x2).toRelEmbedding x = ↑(ConNF.κEquiv x)

theorem ConNF.κ_card_Iio_eq [ConNF.Params] (x : ConNF.κ) : Cardinal.mk ↑{y : ConNF.κ | y < x} = (↑(ConNF.κEquiv x)).card

theorem ConNF.μ_card_Iio_lt [ConNF.Params] (ν : ConNF.μ) : Cardinal.mk ↑{ξ : ConNF.μ | ξ < ν} < Cardinal.mk ConNF.μ

theorem ConNF.μ_card_Iic_lt [ConNF.Params] (ν : ConNF.μ) : Cardinal.mk ↑{ξ : ConNF.μ | ξ ≤ ν} < Cardinal.mk ConNF.μ

theorem ConNF.μ_bounded_lt_of_lt_μ_ord_cof [ConNF.Params] (s : Set ConNF.μ) (h : Cardinal.mk ↑s < (Cardinal.mk ConNF.μ).ord.cof) : Set.Bounded (fun (x1 x2 : ConNF.μ) => x1 < x2) s

theorem ConNF.card_lt_of_μ_bounded [ConNF.Params] (s : Set ConNF.μ) (h : Set.Bounded (fun (x1 x2 : ConNF.μ) => x1 < x2) s) : Cardinal.mk ↑s < Cardinal.mk ConNF.μ