Ordinals

src/1Lab/Path/IdentitySystem.lagda.md

@@ -176,6 +176,18 @@ identity-system-gives-path {R = R} {r = r} ids =
           ∙ transport-refl _ )
 ```
 
+In particular, swapping the arguments of the relation in an identity system
+yields another identity system.
+
+```agda
+flip-identity-system :
+  ∀ {ℓ ℓ'} {A : Type ℓ} {R : A → A → Type ℓ'} {r : ∀ a → R a a}
+  → is-identity-system R r
+  → is-identity-system (flip R) r
+flip-identity-system ids =
+  equiv-path→identity-system $ identity-system-gives-path ids ∙e sym-equiv
+```
+
 ## Based identity systems {defines="based-identity-system unary-identity-system"}
 
 It is sometimes useful to characterise the *based* identity type at

src/Data/Wellfounded/Properties.lagda.md

@@ -34,6 +34,14 @@ Wf-is-prop : is-prop (Wf R)
 Wf-is-prop = Π-is-hlevel 1 Acc-is-prop
 ```
 
+<!--
+```agda
+instance
+  H-Level-Acc : ∀ {x n} → H-Level (Acc R x) (suc n)
+  H-Level-Acc = prop-instance (Acc-is-prop _)
+```
+-->
+
 ## Instances
 
 The usual induction principle for the natural numbers is equivalent to

src/HoTT.lagda.md

@@ -43,7 +43,9 @@ open import Cat.Bi.Base
 open import Cat.Prelude
 open import Cat.Gaunt
 
+open import Data.Wellfounded.Properties
 open import Data.Set.Material.HIT
+open import Data.Wellfounded.Base
 open import Data.Set.Surjection
 open import Data.Wellfounded.W
 open import Data.Fin.Finite using (Listing→choice)
@@ -65,6 +67,7 @@ open import Homotopy.Pushout
 open import Homotopy.Wedge
 open import Homotopy.Base
 
+open import Order.Ordinal.Base
 open import Order.Base
 
 import Algebra.Monoid.Category as Monoid
@@ -1072,6 +1075,39 @@ _ = AC→LEM
 * Lemma 10.1.13: `Susp-prop-is-set`{.Agda}, `Susp-prop-path`{.Agda}
 * Theorem 10.1.14: `AC→LEM`{.Agda}
 
+### 10.3: Ordinal Numbers
+
+<!--
+```agda
+_ = Acc
+_ = Acc-is-prop
+_ = Wf
+_ = Wf-is-prop
+_ = <-wf
+_ = W-well-founded
+_ = is-simulation
+_ = is-simulation.has-injective
+_ = Ordinal-poset
+_ = simulation-unique
+_ = Ordinal
+_ = Ord
+```
+-->
+
+* Definition 10.3.1: `Acc`{.Agda}
+* Lemma 10.3.2: `Acc-is-prop`{.Agda}
+* Definition 10.3.3: `Wf`{.Agda}
+* Lemma 10.3.4: `Wf-is-prop`{.Agda}
+* Example 10.3.5: `<-wf`{.Agda}
+* Example 10.3.6: `W-well-founded`{.Agda}
+* Several theorems about extensional well-founded sets are stated only for ordinals.
+  * Definition 10.3.11: `is-simulation`{.Agda}
+  * Lemma 10.3.12: `is-simulation.has-injective`{.Agda}
+  * Corollary 10.3.15: `Ordinal-poset`{.Agda}
+  * Lemma 10.3.16: `simulation-unique`{.Agda}
+* Definition 10.3.17: `Ordinal`{.Agda}
+* Theorem 10.3.20: `Ord`{.Agda}
+
 ### 10.5: The cumulative hierarchy
 
 <!--