Merge branch 'master' into uniqueness-split-essential-surjectivity

src/order-theory.lagda.md

@@ -120,11 +120,11 @@ open import order-theory.top-elements-posets public
 open import order-theory.top-elements-preorders public
 open import order-theory.total-orders public
 open import order-theory.total-preorders public
+open import order-theory.transitive-well-founded-relations public
 open import order-theory.upper-bounds-chains-posets public
 open import order-theory.upper-bounds-large-posets public
 open import order-theory.upper-bounds-posets public
 open import order-theory.upper-sets-large-posets public
-open import order-theory.well-founded-orders public
 open import order-theory.well-founded-relations public
 open import order-theory.zorns-lemma public
 ```

src/order-theory/accessible-elements-relations.lagda.md

@@ -22,10 +22,11 @@ open import foundation-core.propositions
 ## Idea
 
 Given a type `X` with a [binary relation](foundation.binary-relations.md)
-`_<_ : X → X → Type` we say that `x : X` is **accessible** if `y` is accessible
-for all `y < x`. Note that the predicate of being an accessible element is a
-recursive condition. The accessibility predicate is therefore implemented as an
-inductive type with one constructor:
+`_<_ : X → X → Type` we say that `x : X` is
+{{#concept "accessible" Disambiguation="element with respect to a binary relation" Agda=is-accessible-element-Relation}}
+if, recursively, `y` is accessible for all `y < x`. Since the accessibility
+predicate is defined recursively, it is implemented as an inductive type with
+one constructor:
 
 ```text
   access : ((y : X) → y < x → is-accessible y) → is-accessible x
@@ -37,7 +38,7 @@ inductive type with one constructor:
 
 ```agda
 module _
-  {l1 l2} {X : UU l1} (_<_ : Relation l2 X)
+  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
   where
 
   data is-accessible-element-Relation (x : X) : UU (l1 ⊔ l2)
@@ -70,8 +71,7 @@ module _
   is-accessible-element-is-related-to-accessible-element-Relation :
     {x : X} → is-accessible-element-Relation _<_ x →
     {y : X} → y < x → is-accessible-element-Relation _<_ y
-  is-accessible-element-is-related-to-accessible-element-Relation (access f) =
-    f
+  is-accessible-element-is-related-to-accessible-element-Relation (access f) = f
 ```
 
 ### An induction principle for accessible elements
@@ -112,7 +112,9 @@ are equal. Therefore it follows that `f ＝ f'`, and we conclude that
 `access f ＝ access f'`.
 
 ```agda
-module _ {l1 l2} {X : UU l1} (_<_ : Relation l2 X) where
+module _
+  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
+  where
 
   all-elements-equal-is-accessible-element-Relation :
     (x : X) → all-elements-equal (is-accessible-element-Relation _<_ x)

src/order-theory/ordinals.lagda.md

@@ -10,28 +10,49 @@ module order-theory.ordinals where
 open import foundation.binary-relations
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.sets
 open import foundation.universe-levels
 
-open import order-theory.well-founded-orders
+open import order-theory.posets
+open import order-theory.preorders
+open import order-theory.transitive-well-founded-relations
 open import order-theory.well-founded-relations
 ```
 
 </details>
 
 ## Idea
 
-An ordinal is a propositional relation that is
+An
+{{#concept "ordinal" WDID=Q191780 WD="ordinal number" Agda=is-ordinal Agda=Ordinal}}
+is a type `X` [equipped](foundation.structure.md) with a
+[propositional](foundation-core.propositions.md)
+[relation](foundation.binary-relations.md) `_<_` 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.
+- **Well-founded:** a structure on which it is well-defined to do induction.
+- **Transitive:** if `x < y` and `y < z` then `x < z`.
+- **Extensional:** `x ＝ y` precisely if they are greater than the same
+  elements.
 
 In other words, it is a
-[well-founded order](order-theory.well-founded-orders.md) that is `Prop`-valued
-and antisymmetric.
+[transitive well-founded relation](order-theory.transitive-well-founded-relations.md)
+that is `Prop`-valued and extensional.
 
 ## Definitions
 
+### The extensionality principle of ordinals
+
+```agda
+extensionality-principle-Ordinal :
+  {l1 l2 : Level} {X : UU l1} → Relation-Prop l2 X → UU (l1 ⊔ l2)
+extensionality-principle-Ordinal {X = X} R =
+  (x y : X) →
+  ((u : X) → type-Relation-Prop R u x ↔ type-Relation-Prop R u y) → x ＝ y
+```
+
 ### The predicate of being an ordinal
 
 ```agda
@@ -41,61 +62,113 @@ module _
 
   is-ordinal : UU (l1 ⊔ l2)
   is-ordinal =
-    is-well-founded-order-Relation (type-Relation-Prop R) ×
-    is-antisymmetric (type-Relation-Prop R)
+    ( is-transitive-well-founded-relation-Relation (type-Relation-Prop R)) ×
+    ( extensionality-principle-Ordinal R)
 ```
 
-### Ordinals
+### The type of ordinals
 
 ```agda
-Ordinal : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
-Ordinal l2 X = Σ (Relation-Prop l2 X) is-ordinal
+Ordinal : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Ordinal l1 l2 = Σ (UU l1) (λ X → Σ (Relation-Prop l2 X) is-ordinal)
 
 module _
-  {l1 l2 : Level} {X : UU l1} (S : Ordinal l2 X)
+  {l1 l2 : Level} (O : Ordinal l1 l2)
   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)
+  type-Ordinal : UU l1
+  type-Ordinal = pr1 O
+
+  le-prop-Ordinal : Relation-Prop l2 type-Ordinal
+  le-prop-Ordinal = pr1 (pr2 O)
+
+  le-Ordinal : Relation l2 type-Ordinal
+  le-Ordinal = type-Relation-Prop le-prop-Ordinal
+
+  is-ordinal-Ordinal : is-ordinal le-prop-Ordinal
+  is-ordinal-Ordinal = pr2 (pr2 O)
+
+  is-transitive-well-founded-relation-le-Ordinal :
+    is-transitive-well-founded-relation-Relation le-Ordinal
+  is-transitive-well-founded-relation-le-Ordinal = pr1 is-ordinal-Ordinal
+
+  transitive-well-founded-relation-Ordinal :
+    Transitive-Well-Founded-Relation l2 type-Ordinal
+  transitive-well-founded-relation-Ordinal =
+    ( le-Ordinal , is-transitive-well-founded-relation-le-Ordinal)
+
+  is-extensional-Ordinal : extensionality-principle-Ordinal le-prop-Ordinal
+  is-extensional-Ordinal = pr2 is-ordinal-Ordinal
+
+  is-transitive-le-Ordinal : is-transitive le-Ordinal
+  is-transitive-le-Ordinal =
+    is-transitive-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-well-founded-relation-le-Ordinal : is-well-founded-Relation le-Ordinal
+  is-well-founded-relation-le-Ordinal =
+    is-well-founded-relation-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  well-founded-relation-Ordinal : Well-Founded-Relation l2 type-Ordinal
+  well-founded-relation-Ordinal =
+    well-founded-relation-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-asymmetric-le-Ordinal : is-asymmetric le-Ordinal
+  is-asymmetric-le-Ordinal =
+    is-asymmetric-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-irreflexive-le-Ordinal : is-irreflexive le-Ordinal
+  is-irreflexive-le-Ordinal =
+    is-irreflexive-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+```
+
+The associated reflexive relation on an ordinal.
+
+```agda
+  leq-Ordinal : Relation (l1 ⊔ l2) type-Ordinal
+  leq-Ordinal =
+    leq-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-prop-leq-Ordinal : {x y : type-Ordinal} → is-prop (leq-Ordinal x y)
+  is-prop-leq-Ordinal {y = y} =
+    is-prop-Π
+      ( λ u →
+        is-prop-function-type (is-prop-type-Relation-Prop le-prop-Ordinal u y))
+
+  leq-prop-Ordinal : Relation-Prop (l1 ⊔ l2) type-Ordinal
+  leq-prop-Ordinal x y = (leq-Ordinal x y , is-prop-leq-Ordinal)
+
+  refl-leq-Ordinal : is-reflexive leq-Ordinal
+  refl-leq-Ordinal =
+    refl-leq-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  transitive-leq-Ordinal : is-transitive leq-Ordinal
+  transitive-leq-Ordinal =
+    transitive-leq-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  antisymmetric-leq-Ordinal : is-antisymmetric leq-Ordinal
+  antisymmetric-leq-Ordinal x y p q =
+    is-extensional-Ordinal x y (λ u → p u , q u)
+
+  is-preorder-leq-Ordinal : is-preorder-Relation-Prop leq-prop-Ordinal
+  is-preorder-leq-Ordinal = (refl-leq-Ordinal , transitive-leq-Ordinal)
+
+  preorder-Ordinal : Preorder l1 (l1 ⊔ l2)
+  preorder-Ordinal = (type-Ordinal , leq-prop-Ordinal , is-preorder-leq-Ordinal)
+
+  poset-Ordinal : Poset l1 (l1 ⊔ l2)
+  poset-Ordinal = (preorder-Ordinal , antisymmetric-leq-Ordinal)
+
+  is-set-type-Ordinal : is-set type-Ordinal
+  is-set-type-Ordinal = is-set-type-Poset poset-Ordinal
+
+  set-Ordinal : Set l1
+  set-Ordinal = (type-Ordinal , is-set-type-Ordinal)
 ```

src/order-theory/preorders.lagda.md

@@ -30,17 +30,23 @@ open import foundation.universe-levels
 A **preorder** is a type equipped with a reflexive, transitive relation that is
 valued in propositions.
 
-## Definition
+## Definitions
+
+### The predicate on a propositional relation of being a preorder
+
+```agda
+is-preorder-Relation-Prop :
+  {l1 l2 : Level} {X : UU l1} → Relation-Prop l2 X → UU (l1 ⊔ l2)
+is-preorder-Relation-Prop R =
+  is-reflexive-Relation-Prop R × is-transitive-Relation-Prop R
+```
+
+### The type of preorders
 
 ```agda
 Preorder : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
 Preorder l1 l2 =
-  Σ ( UU l1)
-    ( λ X →
-      Σ ( Relation-Prop l2 X)
-        ( λ R →
-          ( is-reflexive (type-Relation-Prop R)) ×
-          ( is-transitive (type-Relation-Prop R))))
+  Σ (UU l1) (λ X → Σ (Relation-Prop l2 X) (is-preorder-Relation-Prop))
 
 module _
   {l1 l2 : Level} (X : Preorder l1 l2)