Definition of ordinals (UniMath#1159)

Defining the ordinals and coslice precats. I noticed that for relations
you usually have two definitions of properties, one for type-valued
relations, and one for prop-valued ones. Maybe I should add a
prop-valued `is-well-founded-order-Relation`?

src/category-theory.lagda.md

@@ -33,6 +33,7 @@ open import category-theory.copresheaf-categories public
 open import category-theory.coproducts-in-precategories public
 open import category-theory.cores-categories public
 open import category-theory.cores-precategories public
+open import category-theory.coslice-precategories public
 open import category-theory.dependent-products-of-categories public
 open import category-theory.dependent-products-of-large-categories public
 open import category-theory.dependent-products-of-large-precategories public

src/category-theory/coslice-precategories.lagda.md

@@ -0,0 +1,35 @@
+# Coslice precategories
+
+```agda
+module category-theory.coslice-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.opposite-precategories
+open import category-theory.precategories
+open import category-theory.slice-precategories
+
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The {{#concept "coslice precategory" Agda=Coslice-Precategory}} of a
+[precategory](category-theory.precategories.md) `C` under an object `X` of `C`
+is the category of objects of `C` equipped with a morphism from `X`.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2) (X : obj-Precategory C)
+  where
+
+  Coslice-Precategory : Precategory (l1 ⊔ l2) l2
+  Coslice-Precategory =
+    Slice-Precategory (opposite-Precategory C) X
+```

src/elementary-number-theory/inequality-natural-numbers.lagda.md

@@ -7,6 +7,8 @@ module elementary-number-theory.inequality-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.precategories
+
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -147,6 +149,13 @@ pr1 ℕ-Poset = ℕ-Preorder
 pr2 ℕ-Poset = antisymmetric-leq-ℕ
 ```
 
+### The precategory of natural numbers ordered by inequality
+
+```agda
+ℕ-Precategory : Precategory lzero lzero
+ℕ-Precategory = precategory-Preorder ℕ-Preorder
+```
+
 ### For any two natural numbers we can decide which one is less than the other
 
 ```agda

src/order-theory.lagda.md

@@ -82,6 +82,7 @@ open import order-theory.order-preserving-maps-large-posets public
 open import order-theory.order-preserving-maps-large-preorders public
 open import order-theory.order-preserving-maps-posets public
 open import order-theory.order-preserving-maps-preorders public
+open import order-theory.ordinals public
 open import order-theory.posets public
 open import order-theory.powers-of-large-locales public
 open import order-theory.precategory-of-decidable-total-orders public

src/order-theory/ordinals.lagda.md

@@ -0,0 +1,101 @@
+# Ordinals
+
+```agda
+module order-theory.ordinals where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import order-theory.well-founded-orders
+open import order-theory.well-founded-relations
+```
+
+</details>
+
+## Idea
+
+An ordinal is a propositional relation that is
+
+- Transitive: `R x y` and `R y z` imply `R x y`.
+- Extensional: `R x y` and `R y x` imply `x ＝ y`.
+- Well-founded: a structure on which it is well-defined to do induction.
+
+In other words, it is a
+[well-founded order](order-theory.well-founded-orders.md) that is `Prop`-valued
+and antisymmetric.
+
+## Definitions
+
+### The predicate of being an ordinal
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} (R : Relation-Prop l2 X)
+  where
+
+  is-ordinal : UU (l1 ⊔ l2)
+  is-ordinal =
+    is-well-founded-order-Relation (type-Relation-Prop R) ×
+    is-antisymmetric (type-Relation-Prop R)
+```
+
+### Ordinals
+
+```agda
+Ordinal : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
+Ordinal l2 X = Σ (Relation-Prop l2 X) is-ordinal
+
+module _
+  {l1 l2 : Level} {X : UU l1} (S : Ordinal l2 X)
+  where
+
+  lt-prop-Ordinal : Relation-Prop l2 X
+  lt-prop-Ordinal = pr1 S
+
+  lt-Ordinal : Relation l2 X
+  lt-Ordinal = type-Relation-Prop lt-prop-Ordinal
+
+  is-ordinal-Ordinal :
+    is-ordinal lt-prop-Ordinal
+  is-ordinal-Ordinal = pr2 S
+
+  is-well-founded-order-Ordinal :
+    is-well-founded-order-Relation lt-Ordinal
+  is-well-founded-order-Ordinal = pr1 is-ordinal-Ordinal
+
+  is-antisymmetric-Ordinal :
+    is-antisymmetric lt-Ordinal
+  is-antisymmetric-Ordinal = pr2 is-ordinal-Ordinal
+
+  is-transitive-Ordinal : is-transitive lt-Ordinal
+  is-transitive-Ordinal =
+    pr1 is-well-founded-order-Ordinal
+
+  is-well-founded-relation-Ordinal :
+    is-well-founded-Relation lt-Ordinal
+  is-well-founded-relation-Ordinal =
+    pr2 is-well-founded-order-Ordinal
+
+  well-founded-relation-Ordinal : Well-Founded-Relation l2 X
+  pr1 well-founded-relation-Ordinal =
+    lt-Ordinal
+  pr2 well-founded-relation-Ordinal =
+    is-well-founded-relation-Ordinal
+
+  is-asymmetric-Ordinal :
+    is-asymmetric lt-Ordinal
+  is-asymmetric-Ordinal =
+    is-asymmetric-Well-Founded-Relation well-founded-relation-Ordinal
+
+  is-irreflexive-Ordinal :
+    is-irreflexive lt-Ordinal
+  is-irreflexive-Ordinal =
+    is-irreflexive-Well-Founded-Relation
+      ( well-founded-relation-Ordinal)
+```

src/set-theory/cumulative-hierarchy.lagda.md

@@ -38,8 +38,8 @@ open import foundation.universe-levels
 ## Idea
 
 The cumulative hierarchy is a model of set theory. Instead of introducing it as
-a HIT, as in the HoTT Book Section 10.4, we introduce its induction principle,
-following Reference 2 below.
+a HIT, as in Section 10.4 of {{#cite UF13}}, we introduce its induction
+principle, following {{#cite dJKFX23}}.
 
 ## Definitions