Type indices

Signed-off-by: zeramorphic <[email protected]>

.vscode/con-nf.code-snippets

@@ -0,0 +1,49 @@
+{
+	// Place your con-nf workspace snippets here. Each snippet is defined under a snippet name and has a scope, prefix, body and
+	// description. Add comma separated ids of the languages where the snippet is applicable in the scope field. If scope
+	// is left empty or omitted, the snippet gets applied to all languages. The prefix is what is
+	// used to trigger the snippet and the body will be expanded and inserted. Possible variables are:
+	// $1, $2 for tab stops, $0 for the final cursor position, and ${1:label}, ${2:another} for placeholders.
+	// Placeholders with the same ids are connected.
+	// Example:
+	// "Print to console": {
+	// 	"scope": "javascript,typescript",
+	// 	"prefix": "log",
+	// 	"body": [
+	// 		"console.log('$1');",
+	// 		"$2"
+	// 	],
+	// 	"description": "Log output to console"
+	// }
+	"New file template": {
+		"scope": "lean4",
+		"prefix": "newfile",
+		"body": [
+			"import ConNF.Setup.Params",
+			"",
+			"/-!",
+			"# New file",
+			"",
+			"In this file...",
+			"",
+			"## Main declarations",
+			"",
+			"* `ConNF.foo`: Something new.",
+			"-/",
+			"",
+			"noncomputable section",
+			"universe u",
+			"",
+			"open Cardinal Ordinal",
+			"",
+			"namespace ConNF",
+			"",
+			"variable [Params.{u}]",
+			"",
+			"",
+			"",
+			"end ConNF",
+		],
+		"description": "New file template"
+	}
+}

ConNF/Aux/Ordinal.lean

@@ -14,14 +14,58 @@ theorem card_Iio (o : Ordinal.{u}) : #(Set.Iio o) = Cardinal.lift.{u + 1} o.card
 
 instance {o : Ordinal.{u}} : LtWellOrder (Set.Iio o) where
 
-theorem type_iio (o : Ordinal.{u}) :
+theorem type_Iio (o : Ordinal.{u}) :
     type ((· < ·) : Set.Iio o → Set.Iio o → Prop) = lift.{u + 1} o := by
   have := Ordinal.lift_type_eq.{u + 1, u, u + 1}
     (r := ((· < ·) : Set.Iio o → Set.Iio o → Prop)) (s := o.out.r)
   rw [lift_id, type_out] at this
   rw [this]
   exact ⟨o.enumIsoOut.toRelIsoLT⟩
 
+def withBot_orderIso {α : Type u} [Preorder α] [IsWellOrder α (· < ·)] :
+    ((· < ·) : WithBot α → WithBot α → Prop) ≃r
+      Sum.Lex (EmptyRelation (α := PUnit)) ((· < ·) : α → α → Prop) where
+  toFun := WithBot.recBotCoe (Sum.inl PUnit.unit) Sum.inr
+  invFun := Sum.elim (λ _ ↦ ⊥) (λ x ↦ x)
+  left_inv x := by cases x <;> rfl
+  right_inv x := by cases x <;> rfl
+  map_rel_iff' {x y} := by cases x <;> cases y <;>
+    simp only [Equiv.coe_fn_mk, WithBot.recBotCoe_bot, WithBot.recBotCoe_coe,
+    WithBot.coe_lt_coe, WithBot.bot_lt_coe, empty_relation_apply, lt_self_iff_false, not_lt_bot,
+    Sum.lex_inl_inl, Sum.lex_inr_inl, Sum.lex_inr_inr, Sum.Lex.sep]
+
+@[simp]
+theorem type_withBot {α : Type u} [Preorder α] [IsWellOrder α (· < ·)] :
+    type ((· < ·) : WithBot α → WithBot α → Prop) = 1 + type ((· < ·) : α → α → Prop) := by
+  change _ = type EmptyRelation + _
+  rw [← type_sum_lex, type_eq]
+  exact ⟨withBot_orderIso⟩
+
+theorem noMaxOrder_of_isLimit {α : Type u} [Preorder α] [IsWellOrder α (· < ·)]
+    (h : (type ((· < ·) : α → α → Prop)).IsLimit) : NoMaxOrder α := by
+  constructor
+  intro a
+  have := (succ_lt_of_isLimit h).mpr (typein_lt_type (· < ·) a)
+  obtain ⟨b, hb⟩ := typein_surj (· < ·) this
+  use b
+  have := Order.lt_succ (typein ((· < ·) : α → α → Prop) a)
+  rw [← hb, typein_lt_typein] at this
+  exact this
+
+theorem isLimit_of_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWellOrder α (· < ·)]
+    (h : NoMaxOrder α) : (type ((· < ·) : α → α → Prop)).IsLimit := by
+  constructor
+  · simp only [ne_eq, type_eq_zero_iff_isEmpty, not_isEmpty_of_nonempty, not_false_eq_true]
+  · intro o ho
+    obtain ⟨x, hx⟩ := h.exists_gt (enum ((· < ·) : α → α → Prop) o ho)
+    refine lt_of_le_of_lt ?_ (typein_lt_type ((· < ·) : α → α → Prop) x)
+    rw [← typein_lt_typein ((· < ·) : α → α → Prop), typein_enum] at hx
+    rwa [Order.succ_le_iff]
+
+theorem isLimit_iff_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWellOrder α (· < ·)] :
+    (type ((· < ·) : α → α → Prop)).IsLimit ↔ NoMaxOrder α :=
+  ⟨noMaxOrder_of_isLimit, isLimit_of_noMaxOrder⟩
+
 variable {c : Cardinal.{u}} (h : ℵ₀ ≤ c)
 
 theorem add_lt_ord (h : ℵ₀ ≤ c) {x y : Ordinal.{u}}

ConNF/Aux/WellOrder.lean

@@ -7,14 +7,3 @@ variable {α β : Type _}
 instance [LinearOrder α] [IsWellOrder α (· < ·)] : LtWellOrder α := ⟨⟩
 
 open Ordinal
-
-theorem noMaxOrder_of_ordinal_type_eq [LtWellOrder α]
-    (h : (type ((· < ·) : α → α → Prop)).IsLimit) : NoMaxOrder α := by
-  constructor
-  intro a
-  have := (Ordinal.succ_lt_of_isLimit h).mpr (Ordinal.typein_lt_type (· < ·) a)
-  obtain ⟨b, hb⟩ := Ordinal.typein_surj (· < ·) this
-  use b
-  have := Order.lt_succ (Ordinal.typein ((· < ·) : α → α → Prop) a)
-  rw [← hb, Ordinal.typein_lt_typein] at this
-  exact this

ConNF/Setup/Params.lean

@@ -1,8 +1,19 @@
+import Mathlib.Order.Interval.Set.Infinite
 import ConNF.Aux.Cardinal
 import ConNF.Aux.Ordinal
 import ConNF.Aux.Transfer
 import ConNF.Aux.WellOrder
 
+/-!
+# 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.
+-/
+
 noncomputable section
 universe u
 
@@ -14,6 +25,7 @@ class Params where
   Λ : Type u
   κ : Type u
   μ : Type u
+  [Λ_nonempty : Nonempty Λ]
   [ΛWellOrder : LtWellOrder Λ]
   [Λ_noMaxOrder : NoMaxOrder Λ]
   aleph0_lt_κ : ℵ₀ < #κ
@@ -55,8 +67,11 @@ def inaccessibleParams.{v} : Params where
   Λ := (Cardinal.univ.{v, v + 1}).ord.out.α
   κ := ULift.{v + 1, v} (aleph 1).out
   μ := Cardinal.univ.{v, v + 1}.out
+  Λ_nonempty := by
+    rw [ord_univ, out_nonempty_iff_ne_zero, Ordinal.univ_id]
+    simp only [ne_eq, type_eq_zero_iff_isEmpty, not_isEmpty_of_nonempty, not_false_eq_true]
   Λ_noMaxOrder := by
-    apply noMaxOrder_of_ordinal_type_eq
+    apply noMaxOrder_of_isLimit
     change (type (Cardinal.univ.{v, v + 1}).ord.out.r).IsLimit
     rw [type_out]
     apply ord_isLimit
@@ -85,6 +100,7 @@ export Params (Λ κ μ aleph0_lt_κ κ_isRegular μ_isStrongLimit κ_lt_μ κ_l
 
 variable [Params.{u}]
 
+instance : Nonempty Λ := Params.Λ_nonempty
 instance : LtWellOrder Λ := Params.ΛWellOrder
 instance : NoMaxOrder Λ := Params.Λ_noMaxOrder
 
@@ -94,28 +110,38 @@ theorem aleph0_lt_μ : ℵ₀ < #μ :=
 theorem type_Λ_le_μ_ord : type ((· < ·) : Λ → Λ → Prop) ≤ (#μ).ord :=
   Λ_le_cof_μ.trans <| ord_cof_le (#μ).ord
 
-opaque κEquiv : κ ≃ Set.Iio (#κ).ord := by
+@[irreducible]
+def κEquiv : κ ≃ Set.Iio (#κ).ord := by
   apply Equiv.ulift.{u + 1, u}.symm.trans
   apply Nonempty.some
   rw [← Cardinal.eq, mk_uLift, card_Iio, card_ord]
 
-opaque μEquiv : μ ≃ Set.Iio (#μ).ord := by
+@[irreducible]
+def μEquiv : μ ≃ Set.Iio (#μ).ord := by
   apply Equiv.ulift.{u + 1, u}.symm.trans
   apply Nonempty.some
   rw [← Cardinal.eq, mk_uLift, card_Iio, card_ord]
 
 instance : LtWellOrder κ := Equiv.ltWellOrder κEquiv
 instance : LtWellOrder μ := Equiv.ltWellOrder μEquiv
 
+instance : Infinite Λ := NoMaxOrder.infinite
+instance : Infinite κ := by rw [infinite_iff]; exact aleph0_lt_κ.le
+instance : Infinite μ := by rw [infinite_iff]; exact aleph0_lt_μ.le
+
+theorem Λ_type_isLimit : (type ((· < ·) : Λ → Λ → Prop)).IsLimit := by
+  rw [isLimit_iff_noMaxOrder]
+  infer_instance
+
 @[simp]
-theorem κ.type : type ((· < ·) : κ → κ → Prop) = (#κ).ord := by
+theorem κ_type : type ((· < ·) : κ → κ → Prop) = (#κ).ord := by
   have := κEquiv.ltWellOrder_type
-  rwa [Ordinal.lift_id, type_iio, Ordinal.lift_inj] at this
+  rwa [Ordinal.lift_id, type_Iio, Ordinal.lift_inj] at this
 
 @[simp]
-theorem μ.type : type ((· < ·) : μ → μ → Prop) = (#μ).ord := by
+theorem μ_type : type ((· < ·) : μ → μ → Prop) = (#μ).ord := by
   have := μEquiv.ltWellOrder_type
-  rwa [Ordinal.lift_id, type_iio, Ordinal.lift_inj] at this
+  rwa [Ordinal.lift_id, type_Iio, Ordinal.lift_inj] at this
 
 instance : AddMonoid κ :=
   letI := iioAddMonoid aleph0_lt_κ.le
@@ -125,24 +151,24 @@ instance : Sub κ :=
   letI := iioSub (#κ).ord
   Equiv.sub κEquiv
 
-theorem κ.add_def (x y : κ) :
+theorem κ_add_def (x y : κ) :
     letI := iioAddMonoid aleph0_lt_κ.le
     x + y = κEquiv.symm (κEquiv x + κEquiv y) :=
   rfl
 
-theorem κ.sub_def (x y : κ) :
+theorem κ_sub_def (x y : κ) :
     letI := iioSub (#κ).ord
     x - y = κEquiv.symm (κEquiv x - κEquiv y) :=
   rfl
 
-theorem κ.κEquiv_add (x y : κ) :
+theorem κEquiv_add (x y : κ) :
     (κEquiv (x + y) : Ordinal) = (κEquiv x : Ordinal) + κEquiv y := by
-  rw [κ.add_def, Equiv.apply_symm_apply]
+  rw [κ_add_def, Equiv.apply_symm_apply]
   rfl
 
-theorem κ.κEquiv_sub (x y : κ) :
+theorem κEquiv_sub (x y : κ) :
     (κEquiv (x - y) : Ordinal) = (κEquiv x : Ordinal) - κEquiv y := by
-  rw [κ.sub_def, Equiv.apply_symm_apply]
+  rw [κ_sub_def, Equiv.apply_symm_apply]
   rfl
 
 end ConNF

ConNF/Setup/TypeIndex.lean

@@ -0,0 +1,40 @@
+import ConNF.Setup.Params
+
+/-!
+# Type indices
+
+In this file, we declare the notion of a type index, and prove some of its basic properties.
+
+## Main declarations
+
+* `ConNF.TypeIndex`: The type of type indices.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal
+
+namespace ConNF
+
+variable [Params.{u}]
+
+/-- Either the base type or a proper type index (an inhabitant of `Λ`).
+The base type is written `⊥`. -/
+@[reducible]
+def TypeIndex :=
+  WithBot Λ
+
+@[simp]
+protected theorem TypeIndex.type :
+    type ((· < ·) : TypeIndex → TypeIndex → Prop) = type ((· < ·) : Λ → Λ → Prop) := by
+  rw [type_withBot]
+  exact one_add_of_omega_le <| omega_le_of_isLimit Λ_type_isLimit
+
+@[simp]
+protected theorem TypeIndex.card :
+    #TypeIndex = #Λ := by
+  have := congr_arg Ordinal.card TypeIndex.type
+  rwa [card_type, card_type] at this
+
+end ConNF

blueprint/src/chapters/environment.tex

@@ -45,6 +45,7 @@ \section{Model parameters}
 \begin{definition}[type index]
   \label{def:TypeIndex}
   \uses{def:Params}
+  \lean{ConNF.TypeIndex}
   The type of \emph{type indices} is \( \lambda^\bot \coloneq \texttt{WithBot}(\lambda) \): the collection of \emph{proper type indices} \( \lambda \) together with a designated symbol \( \bot \) which is smaller than all proper type indices.
   Note that \( \ot(\lambda^\bot) = \ot(\lambda) \), and hence that for each \( \alpha : \lambda^\bot \),
   \[ \#\{ \beta : \lambda^\bot \mid \beta < \alpha \} \leq \#\{ \beta : \lambda^\bot \mid \beta \leq \alpha \} < \cof(\ord(\#\mu)) \]

blueprint/src/web.tex

@@ -23,7 +23,7 @@
 \input{macro/web}
 
 \github{https://github.com/leanprover-community/con-nf/}
-\dochome{https://leanprover-community.github.io/con-nf/docs}
+\dochome{https://leanprover-community.github.io/con-nf/doc}
 
 \title{New Foundations is consistent}
 \author{Sky Wilshaw}