diff --git a/Cubical/Data/Cardinal.agda b/Cubical/Data/Cardinal.agda
new file mode 100644
index 0000000000..380e953f10
--- /dev/null
+++ b/Cubical/Data/Cardinal.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Cardinal where
+
+open import Cubical.Data.Cardinal.Base public
+open import Cubical.Data.Cardinal.Properties public
diff --git a/Cubical/Data/Cardinality/Base.agda b/Cubical/Data/Cardinal/Base.agda
similarity index 83%
rename from Cubical/Data/Cardinality/Base.agda
rename to Cubical/Data/Cardinal/Base.agda
index 56f161145f..72b8ebd6db 100644
--- a/Cubical/Data/Cardinality/Base.agda
+++ b/Cubical/Data/Cardinal/Base.agda
@@ -7,7 +7,7 @@ This file contains:
 
 -}
 {-# OPTIONS --safe #-}
-module Cubical.Data.Cardinality.Base where
+module Cubical.Data.Cardinal.Base where
 
 open import Cubical.HITs.SetTruncation as ∥₂
 open import Cubical.Foundations.Prelude
@@ -19,7 +19,7 @@ open import Cubical.Data.Unit
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
 
 -- First, we define a cardinal as the set truncation of Set
 Card : Type (ℓ-suc ℓ)
@@ -41,14 +41,14 @@ card = ∣_∣₂
 𝟙 = card (Unit* , isSetUnit*)
 
 -- Now we define some arithmetic
-_+_ : Card {ℓ} → Card {ℓ} → Card {ℓ}
+_+_ : Card {ℓ} → Card {ℓ'} → Card {ℓ-max ℓ ℓ'}
 _+_ = ∥₂.rec2 isSetCard λ (A , isSetA) (B , isSetB)
                         → card ((A ⊎ B) , isSet⊎ isSetA isSetB)
 
-_·_ : Card {ℓ} → Card {ℓ} → Card {ℓ}
+_·_ : Card {ℓ} → Card {ℓ'} → Card {ℓ-max ℓ ℓ'}
 _·_ = ∥₂.rec2 isSetCard λ (A , isSetA) (B , isSetB)
                         → card ((A × B) , isSet× isSetA isSetB)
 
-_^_ : Card {ℓ} → Card {ℓ} → Card {ℓ}
+_^_ : Card {ℓ} → Card {ℓ'} → Card {ℓ-max ℓ ℓ'}
 _^_ = ∥₂.rec2 isSetCard λ (A , isSetA) (B , _)
                         → card ((B → A) , isSet→ isSetA)
diff --git a/Cubical/Data/Cardinality/Properties.agda b/Cubical/Data/Cardinal/Properties.agda
similarity index 72%
rename from Cubical/Data/Cardinality/Properties.agda
rename to Cubical/Data/Cardinal/Properties.agda
index 77a6dba379..1c7371cf0c 100644
--- a/Cubical/Data/Cardinality/Properties.agda
+++ b/Cubical/Data/Cardinal/Properties.agda
@@ -7,10 +7,10 @@ This file contains:
 
 -}
 {-# OPTIONS --safe #-}
-module Cubical.Data.Cardinality.Properties where
+module Cubical.Data.Cardinal.Properties where
 
 open import Cubical.HITs.SetTruncation as ∥₂
-open import Cubical.Data.Cardinality.Base
+open import Cubical.Data.Cardinal.Base
 
 open import Cubical.Algebra.CommSemiring
 
@@ -30,55 +30,60 @@ open import Cubical.Relation.Binary.Order.Properties
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' ℓ'' ℓa ℓb ℓc ℓd : Level
 
 -- Cardinality is a commutative semiring
 module _ where
   private
-    +Assoc : (A B C : Card {ℓ}) → A + (B + C) ≡ (A + B) + C
+    +Assoc : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc})
+           → A + (B + C) ≡ (A + B) + C
     +Assoc = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _))
                       λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                   (sym (isoToPath ⊎-assoc-Iso)))
 
-    ·Assoc : (A B C : Card {ℓ}) → A · (B · C) ≡ (A · B) · C
+    ·Assoc : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc})
+           → A · (B · C) ≡ (A · B) · C
     ·Assoc = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _))
                       λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                   (sym (isoToPath Σ-assoc-Iso)))
 
-    +IdR𝟘 : (A : Card {ℓ}) → A + 𝟘 ≡ A
+    +IdR𝟘 : (A : Card {ℓ}) → A + 𝟘 {ℓ} ≡ A
     +IdR𝟘 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
                     λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                             (isoToPath ⊎-IdR-⊥*-Iso))
 
-    +IdL𝟘 : (A : Card {ℓ}) → 𝟘 + A ≡ A
+    +IdL𝟘 : (A : Card {ℓ}) → 𝟘 {ℓ} + A ≡ A
     +IdL𝟘 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
                     λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                             (isoToPath ⊎-IdL-⊥*-Iso))
 
-    ·IdR𝟙 : (A : Card {ℓ}) → A · 𝟙 ≡ A
+    ·IdR𝟙 : (A : Card {ℓ}) → A · 𝟙 {ℓ} ≡ A
     ·IdR𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
                     λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                             (isoToPath rUnit*×Iso))
 
-    ·IdL𝟙 : (A : Card {ℓ}) → 𝟙 · A ≡ A
+    ·IdL𝟙 : (A : Card {ℓ}) → 𝟙 {ℓ} · A ≡ A
     ·IdL𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
                     λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                             (isoToPath lUnit*×Iso))
 
-    +Comm : (A B : Card {ℓ}) → (A + B) ≡ (B + A)
+    +Comm : (A : Card {ℓa}) (B : Card {ℓb})
+          → (A + B) ≡ (B + A)
     +Comm = ∥₂.elim2 (λ _ _ → isProp→isSet (isSetCard _ _))
                      λ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                (isoToPath ⊎-swap-Iso))
 
-    ·Comm : (A B : Card {ℓ}) → (A · B) ≡ (B · A)
+    ·Comm : (A : Card {ℓa}) (B : Card {ℓb})
+          → (A · B) ≡ (B · A)
     ·Comm = ∥₂.elim2 (λ _ _ → isProp→isSet (isSetCard _ _))
                      λ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                (isoToPath Σ-swap-Iso))
 
-    ·LDist+ : (A B C : Card {ℓ}) → A · (B + C) ≡ (A · B) + (A · C)
+    ·LDist+ : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc})
+            → A · (B + C) ≡ (A · B) + (A · C)
     ·LDist+ = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _))
                        λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
-                                                   (isoToPath ×DistL⊎Iso))
+                                                   (isoToPath ×DistR⊎Iso))
 
     AnnihilL : (A : Card {ℓ}) → 𝟘 · A ≡ 𝟘
     AnnihilL = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
@@ -90,7 +95,7 @@ module _ where
 
 -- Exponentiation is also well-behaved
 
-^AnnihilR𝟘 : (A : Card {ℓ}) → A ^ 𝟘 ≡ 𝟙
+^AnnihilR𝟘 : (A : Card {ℓ}) → A ^ 𝟘 {ℓ} ≡ 𝟙 {ℓ}
 ^AnnihilR𝟘 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
              λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                             (isoToPath (iso⊥ _)))
@@ -100,7 +105,7 @@ module _ where
                  Iso.rightInv (iso⊥ A) _   = refl
                  Iso.leftInv  (iso⊥ A) _ i ()
 
-^IdR𝟙 : (A : Card {ℓ}) → A ^ 𝟙 ≡ A
+^IdR𝟙 : (A : Card {ℓ}) → A ^ 𝟙 {ℓ} ≡ A
 ^IdR𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
                 λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                (isoToPath (iso⊤ _)))
@@ -110,7 +115,7 @@ module _ where
               Iso.rightInv (iso⊤ _) _ = refl
               Iso.leftInv  (iso⊤ _) _ = refl
 
-^AnnihilL𝟙 : (A : Card {ℓ}) → 𝟙 ^ A ≡ 𝟙
+^AnnihilL𝟙 : (A : Card {ℓ}) → 𝟙 {ℓ} ^ A ≡ 𝟙 {ℓ}
 ^AnnihilL𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))
                      λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                              (isoToPath (iso⊤ _)))
@@ -120,12 +125,14 @@ module _ where
                    Iso.rightInv (iso⊤ _) _ = refl
                    Iso.leftInv  (iso⊤ _) _ = refl
 
-^LDist+ : (A B C : Card {ℓ}) → A ^ (B + C) ≡ (A ^ B) · (A ^ C)
+^LDist+ : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc})
+        → A ^ (B + C) ≡ (A ^ B) · (A ^ C)
 ^LDist+ = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _))
                    λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                (isoToPath Π⊎Iso))
 
-^Assoc· : (A B C : Card {ℓ}) → A ^ (B · C) ≡ (A ^ B) ^ C
+^Assoc· : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc})
+        → A ^ (B · C) ≡ (A ^ B) ^ C
 ^Assoc· = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _))
                    λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                (isoToPath (is _ _ _)))
@@ -134,7 +141,8 @@ module _ where
                            (C × B → A) Iso⟨ curryIso ⟩
                            (C → B → A) ∎Iso
 
-^RDist· : (A B C : Card {ℓ}) → (A · B) ^ C ≡ (A ^ C) · (B ^ C)
+^RDist· : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc})
+        → (A · B) ^ C ≡ (A ^ C) · (B ^ C)
 ^RDist· = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _))
                    λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
                                                (isoToPath Σ-Π-Iso))
@@ -143,51 +151,48 @@ module _ where
 -- With basic arithmetic done, we can now define an ordering over cardinals
 module _ where
   private
-    _≲'_ : Card {ℓ} → Card {ℓ} → hProp ℓ
+    _≲'_ : Card {ℓ} → Card {ℓ'} → hProp (ℓ-max ℓ ℓ')
     _≲'_ = ∥₂.rec2 isSetHProp λ (A , _) (B , _) → ∥ A ↪ B ∥₁ , isPropPropTrunc
 
-  _≲_ : Rel (Card {ℓ}) (Card {ℓ}) ℓ
+  _≲_ : Rel (Card {ℓ}) (Card {ℓ'}) (ℓ-max ℓ ℓ')
   A ≲ B = ⟨ A ≲' B ⟩
 
+  isPropValued≲ : (A : Card {ℓ}) (B : Card {ℓ'}) → isProp (A ≲ B)
+  isPropValued≲ a b = str (a ≲' b)
+
+  isRefl≲ : BinaryRelation.isRefl {A = Card {ℓ}} _≲_
+  isRefl≲ = ∥₂.elim (λ A → isProp→isSet (isPropValued≲ A A))
+                     λ (A , _) → ∣ id↪ A ∣₁
+
+  isTrans≲ : (A : Card {ℓ}) (B : Card {ℓ'}) (C : Card {ℓ''})
+           → A ≲ B → B ≲ C → A ≲ C
+  isTrans≲ = ∥₂.elim3
+             (λ x _ z → isSetΠ2 λ _ _ → isProp→isSet (isPropValued≲ x z))
+             λ (A , _) (B , _) (C , _)
+               → ∥₁.map2 λ A↪B B↪C → compEmbedding B↪C A↪B
+
   isPreorder≲ : IsPreorder {ℓ-suc ℓ} _≲_
   isPreorder≲
-    = ispreorder isSetCard prop reflexive transitive
-                 where prop : BinaryRelation.isPropValued _≲_
-                       prop a b = str (a ≲' b)
-
-                       reflexive : BinaryRelation.isRefl _≲_
-                       reflexive = ∥₂.elim (λ A → isProp→isSet (prop A A))
-                                           (λ (A , _) → ∣ id↪ A ∣₁)
-
-                       transitive : BinaryRelation.isTrans _≲_
-                       transitive = ∥₂.elim3 (λ x _ z → isSetΠ2
-                                                      λ _ _ → isProp→isSet
-                                                              (prop x z))
-                                             (λ (A , _) (B , _) (C , _)
-                                              → ∥₁.map2 λ A↪B B↪C
-                                                        → compEmbedding
-                                                          B↪C
-                                                          A↪B)
+    = ispreorder isSetCard isPropValued≲ isRefl≲ isTrans≲
 
 isLeast𝟘 : ∀{ℓ} → isLeast isPreorder≲ (Card {ℓ} , id↪ (Card {ℓ})) (𝟘 {ℓ})
-isLeast𝟘 = ∥₂.elim (λ x → isProp→isSet (IsPreorder.is-prop-valued
-                                       isPreorder≲ 𝟘 x))
+isLeast𝟘 = ∥₂.elim (λ x → isProp→isSet (isPropValued≲ 𝟘 x))
                    (λ _ → ∣ ⊥.rec* , (λ ()) ∣₁)
 
 -- Our arithmetic behaves as expected over our preordering
-+Monotone≲ : (A B C D : Card {ℓ}) → A ≲ C → B ≲ D → (A + B) ≲ (C + D)
++Monotone≲ : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc}) (D : Card {ℓd})
+           → A ≲ C → B ≲ D → (A + B) ≲ (C + D)
 +Monotone≲
-  = ∥₂.elim4 (λ w x y z → isSetΠ2 λ _ _ → isProp→isSet (IsPreorder.is-prop-valued
-                                                       isPreorder≲
+  = ∥₂.elim4 (λ w x y z → isSetΠ2 λ _ _ → isProp→isSet (isPropValued≲
                                                        (w + x)
                                                        (y + z)))
               λ (A , _) (B , _) (C , _) (D , _)
               → ∥₁.map2 λ A↪C B↪D → ⊎Monotone↪ A↪C B↪D
 
-·Monotone≲ : (A B C D : Card {ℓ}) → A ≲ C → B ≲ D → (A · B) ≲ (C · D)
+·Monotone≲ : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc}) (D : Card {ℓd})
+           → A ≲ C → B ≲ D → (A · B) ≲ (C · D)
 ·Monotone≲
-  = ∥₂.elim4 (λ w x y z → isSetΠ2 λ _ _ → isProp→isSet (IsPreorder.is-prop-valued
-                                                       isPreorder≲
+  = ∥₂.elim4 (λ w x y z → isSetΠ2 λ _ _ → isProp→isSet (isPropValued≲
                                                        (w · x)
                                                        (y · z)))
               λ (A , _) (B , _) (C , _) (D , _)
diff --git a/Cubical/Data/Cardinality.agda b/Cubical/Data/Cardinality.agda
deleted file mode 100644
index 2c992fe9c8..0000000000
--- a/Cubical/Data/Cardinality.agda
+++ /dev/null
@@ -1,5 +0,0 @@
-{-# OPTIONS --safe #-}
-module Cubical.Data.Cardinality where
-
-open import Cubical.Data.Cardinality.Base public
-open import Cubical.Data.Cardinality.Properties public
diff --git a/Cubical/Data/Empty/Base.agda b/Cubical/Data/Empty/Base.agda
index b126a028f1..2ed93831b5 100644
--- a/Cubical/Data/Empty/Base.agda
+++ b/Cubical/Data/Empty/Base.agda
@@ -20,3 +20,6 @@ rec* ()
 
 elim : {A : ⊥ → Type ℓ} → (x : ⊥) → A x
 elim ()
+
+elim* : {A : ⊥* {ℓ'} → Type ℓ} → (x : ⊥* {ℓ'}) → A x
+elim* ()
diff --git a/Cubical/Data/Ordinal.agda b/Cubical/Data/Ordinal.agda
new file mode 100644
index 0000000000..54a05cdc3f
--- /dev/null
+++ b/Cubical/Data/Ordinal.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Ordinal where
+
+open import Cubical.Data.Ordinal.Base public
+open import Cubical.Data.Ordinal.Properties public
diff --git a/Cubical/Data/Ordinal/Base.agda b/Cubical/Data/Ordinal/Base.agda
new file mode 100644
index 0000000000..116fb8c4f9
--- /dev/null
+++ b/Cubical/Data/Ordinal/Base.agda
@@ -0,0 +1,257 @@
+{-
+
+This file contains:
+
+- Ordinals as well-ordered sets
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Data.Ordinal.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Unit
+
+open import Cubical.Induction.WellFounded
+
+open import Cubical.Relation.Binary.Base
+open import Cubical.Relation.Binary.Extensionality
+open import Cubical.Relation.Binary.Order.Woset
+
+private
+  variable
+    ℓ : Level
+
+infix 7 _·_
+infix 6 _+_
+
+-- Ordinals are simply well-ordered sets
+Ord : ∀ {ℓ} → Type _
+Ord {ℓ} = Woset ℓ ℓ
+
+isSetOrd : isSet (Ord {ℓ})
+isSetOrd = isSetWoset
+
+-- The successor ordinal is simply the union with unit
+suc : Ord {ℓ} → Ord {ℓ}
+suc {ℓ} (A , ordStr) = (A ⊎ Unit* {ℓ}) , wosetstr _≺_ iswos
+  where _≺ₐ_ = WosetStr._≺_ ordStr
+        wosA = WosetStr.isWoset ordStr
+        setA = IsWoset.is-set wosA
+        propA = IsWoset.is-prop-valued wosA
+        wellA = IsWoset.is-well-founded wosA
+        weakA = IsWoset.is-weakly-extensional wosA
+        transA = IsWoset.is-trans wosA
+
+
+        _≺_ : Rel (A ⊎ Unit* {ℓ}) (A ⊎ Unit* {ℓ}) ℓ
+        inl a ≺ inl b = a ≺ₐ b
+        inl _ ≺ inr * = Unit* {ℓ}
+        inr * ≺ _ = ⊥* {ℓ}
+
+        open BinaryRelation
+
+        set : isSet (A ⊎ Unit*)
+        set = isSet⊎ setA isSetUnit*
+
+        prop : isPropValued _≺_
+        prop (inl a) (inl b) = propA a b
+        prop (inl _) (inr *) = isPropUnit*
+        prop (inr *) _ = isProp⊥*
+
+        well : WellFounded _≺_
+        well (inl x) = WFI.induction wellA {P = λ x → Acc _≺_ (inl x)}
+                     (λ _ ind → acc (λ { (inl y) → ind y
+                                       ; (inr *) () })) x
+        well (inr *) = acc (λ { (inl y) _ → well (inl y)
+                              ; (inr *) () })
+
+        weak : isWeaklyExtensional _≺_
+        weak = ≺×→≡→isWeaklyExtensional _≺_ set prop
+             λ { (inl x) (inl y) ex → cong inl
+                 (isWeaklyExtensional→≺Equiv→≡ _≺ₐ_ weakA x y λ z
+                 → propBiimpl→Equiv (propA z x) (propA z y)
+                   (ex (inl z) .fst)
+                   (ex (inl z) .snd))
+               ; (inl x) (inr *) ex → ⊥.rec
+                   (WellFounded→isIrrefl _≺ₐ_ wellA x (ex (inl x) .snd tt*))
+               ; (inr *) (inl x) ex → ⊥.rec
+                   (WellFounded→isIrrefl _≺ₐ_ wellA x (ex (inl x) .fst tt*))
+               ; (inr *) (inr _) _ → refl
+               }
+
+        trans : isTrans _≺_
+        trans (inl a) (inl b) (inl c) = transA a b c
+        trans (inl _) (inl _) (inr *) _ _ = tt*
+        trans (inl a) (inr *) _ _ ()
+        trans (inr *) _ _ ()
+
+        iswos : IsWoset _≺_
+        iswos = iswoset set prop well weak trans
+
+-- Ordinal addition is handled similarly
+_+_ : Ord {ℓ} → Ord {ℓ} → Ord {ℓ}
+A + B = (⟨ A ⟩ ⊎ ⟨ B ⟩) , wosetstr _≺_ wos
+  where _≺ᵣ_ = WosetStr._≺_ (str A)
+        _≺ₛ_ = WosetStr._≺_ (str B)
+
+        wosA = WosetStr.isWoset (str A)
+        setA = IsWoset.is-set wosA
+        propA = IsWoset.is-prop-valued wosA
+        wellA = IsWoset.is-well-founded wosA
+        weakA = IsWoset.is-weakly-extensional wosA
+        transA = IsWoset.is-trans wosA
+
+        wosB = WosetStr.isWoset (str B)
+        setB = IsWoset.is-set wosB
+        propB = IsWoset.is-prop-valued wosB
+        wellB = IsWoset.is-well-founded wosB
+        weakB = IsWoset.is-weakly-extensional wosB
+        transB = IsWoset.is-trans wosB
+
+        _≺_ : Rel (⟨ A ⟩ ⊎ ⟨ B ⟩) (⟨ A ⟩ ⊎ ⟨ B ⟩) _
+        inl a₀ ≺ inl a₁ = a₀ ≺ᵣ a₁
+        inl a₀ ≺ inr b₁ = Unit*
+        inr b₀ ≺ inl a₁ = ⊥*
+        inr b₀ ≺ inr b₁ = b₀ ≺ₛ b₁
+
+        open BinaryRelation
+
+        set : isSet (⟨ A ⟩ ⊎ ⟨ B ⟩)
+        set = isSet⊎ setA setB
+
+        prop : isPropValued _≺_
+        prop (inl a₀) (inl a₁) = propA a₀ a₁
+        prop (inl a₀) (inr b₁) = isPropUnit*
+        prop (inr b₀) (inl a₁) = isProp⊥*
+        prop (inr b₀) (inr b₁) = propB b₀ b₁
+
+        well : WellFounded _≺_
+        well (inl a₀) = WFI.induction wellA {P = λ a → Acc _≺_ (inl a)}
+          (λ _ ind → acc λ { (inl a₁) → ind a₁
+                           ; (inr b₁) () }) a₀
+        well (inr b₀) = WFI.induction wellB {P = λ b → Acc _≺_ (inr b)}
+          (λ _ ind → acc λ { (inl a₁) _ → well (inl a₁)
+                           ; (inr b₁) → ind b₁ }) b₀
+
+        weak : isWeaklyExtensional _≺_
+        weak = ≺×→≡→isWeaklyExtensional _≺_ set prop
+          λ { (inl a₀) (inl a₁) ex → cong inl
+              (isWeaklyExtensional→≺Equiv→≡ _≺ᵣ_ weakA a₀ a₁ λ c →
+                propBiimpl→Equiv (propA c a₀) (propA c a₁)
+                (ex (inl c) .fst)
+                (ex (inl c) .snd))
+            ; (inl a₀) (inr _) ex →
+              ⊥.rec (WellFounded→isIrrefl _≺ᵣ_ wellA a₀ (ex (inl a₀) .snd tt*))
+            ; (inr _) (inl a₁) ex →
+              ⊥.rec (WellFounded→isIrrefl _≺ᵣ_ wellA a₁ (ex (inl a₁) .fst tt*))
+            ; (inr b₀) (inr b₁) ex → cong inr
+              (isWeaklyExtensional→≺Equiv→≡ _≺ₛ_ weakB b₀ b₁ λ c →
+                propBiimpl→Equiv (propB c b₀) (propB c b₁)
+                (ex (inr c) .fst)
+                (ex (inr c) .snd))
+            }
+
+        trans : isTrans _≺_
+        trans (inl a) (inl b) (inl c) = transA a b c
+        trans (inl _) _ (inr _) _ _ = tt*
+        trans _ (inr _) (inl _) _ ()
+        trans (inr _) (inl _) _ ()
+        trans (inr a) (inr b) (inr c) = transB a b c
+
+        wos : IsWoset _≺_
+        wos = iswoset set prop well weak trans
+
+-- Ordinal multiplication is handled lexicographically
+_·_ : Ord {ℓ} → Ord {ℓ} → Ord {ℓ}
+A · B = ⟨ A ⟩ × ⟨ B ⟩ , wosetstr _≺_ wos
+  where _≺ᵣ_ = WosetStr._≺_ (str A)
+        _≺ₛ_ = WosetStr._≺_ (str B)
+
+        wosA = WosetStr.isWoset (str A)
+        setA = IsWoset.is-set wosA
+        propA = IsWoset.is-prop-valued wosA
+        wellA = IsWoset.is-well-founded wosA
+        weakA = IsWoset.is-weakly-extensional wosA
+        transA = IsWoset.is-trans wosA
+
+        wosB = WosetStr.isWoset (str B)
+        setB = IsWoset.is-set wosB
+        propB = IsWoset.is-prop-valued wosB
+        wellB = IsWoset.is-well-founded wosB
+        weakB = IsWoset.is-weakly-extensional wosB
+        transB = IsWoset.is-trans wosB
+
+        _≺_ : Rel (⟨ A ⟩ × ⟨ B ⟩) (⟨ A ⟩ × ⟨ B ⟩) _
+        (a₀ , b₀) ≺ (a₁ , b₁) = (b₀ ≺ₛ b₁) ⊎ ((b₀ ≡ b₁) × (a₀ ≺ᵣ a₁))
+
+        open BinaryRelation
+
+        set : isSet (⟨ A ⟩ × ⟨ B ⟩)
+        set = isSet× setA setB
+
+        prop : isPropValued _≺_
+        prop (a₀ , b₀) (a₁ , b₁)
+          = isProp⊎ (propB _ _) (isProp× (setB _ _) (propA _ _))
+            λ b₀≺b₁ (b₀≡b₁ , _)
+          → WellFounded→isIrrefl _≺ₛ_ wellB b₁ (subst (_≺ₛ b₁) b₀≡b₁ b₀≺b₁)
+
+        well : WellFounded _≺_
+        well (a₀ , b₀) = WFI.induction wellB {P = λ b → ∀ a → Acc _≺_ (a , b)}
+          (λ b₁ indB → WFI.induction wellA {P = λ a → Acc _≺_ (a , b₁)}
+           λ a₂ indA → acc λ { (a , b) (inl b≺b₁) → indB b b≺b₁ a
+                             ; (a , b) (inr (b≡b₁ , a≺a₁))
+                             → subst (λ x → Acc _≺_ (a , x))
+                                     (sym b≡b₁)
+                                     (indA a a≺a₁) }) b₀ a₀
+
+        weak : isWeaklyExtensional _≺_
+        weak = ≺×→≡→isWeaklyExtensional _≺_ set prop λ (a₀ , b₀) (a₁ , b₁) ex →
+             ΣPathP ((isWeaklyExtensional→≺Equiv→≡ _≺ᵣ_ weakA a₀ a₁
+               (λ a₂ → propBiimpl→Equiv (propA a₂ a₀) (propA a₂ a₁)
+               (λ a₂≺a₀ → ⊎.rec (λ b₀≺b₁ → ⊥.rec
+                          (WellFounded→isIrrefl _≺ₛ_ wellB b₁
+                          (subst (_≺ₛ b₁) (lemma a₀ a₁ b₀ b₁ ex) b₀≺b₁))) snd
+                          (ex (a₂ , b₀) .fst (inr (refl , a₂≺a₀))))
+               λ a₂≺a₁ → ⊎.rec (λ b₁≺b₀ → ⊥.rec
+                         (WellFounded→isIrrefl _≺ₛ_ wellB b₁
+                         (subst (b₁ ≺ₛ_) (lemma a₀ a₁ b₀ b₁ ex) b₁≺b₀))) snd
+                         (ex (a₂ , b₁) .snd (inr (refl , a₂≺a₁)))))
+               , lemma a₀ a₁ b₀ b₁ ex)
+             where lemma : ∀ a₀ a₁ b₀ b₁
+                         → (∀ c → (c ≺ (a₀ , b₀) → c ≺ (a₁ , b₁))
+                                × (c ≺ (a₁ , b₁) → c ≺ (a₀ , b₀)))
+                         → b₀ ≡ b₁
+                   lemma a₀ a₁ b₀ b₁ ex
+                     = isWeaklyExtensional→≺Equiv→≡ _≺ₛ_ weakB b₀ b₁
+                       λ b₂ → propBiimpl→Equiv (propB b₂ b₀) (propB b₂ b₁)
+                         (λ b₂≺b₀ → ⊎.rec (λ b₂≺b₁ → b₂≺b₁)
+                            (λ (_ , a₁≺a₁)
+                            → ⊥.rec (WellFounded→isIrrefl _≺ᵣ_ wellA a₁ a₁≺a₁))
+                              (ex (a₁ , b₂) .fst (inl b₂≺b₀)))
+                         λ b₂≺b₁ → ⊎.rec (λ b₂≺b₀ → b₂≺b₀)
+                           (λ (_ , a₀≺a₀)
+                           → ⊥.rec (WellFounded→isIrrefl _≺ᵣ_ wellA a₀ a₀≺a₀))
+                             (ex (a₀ , b₂) .snd (inl b₂≺b₁))
+
+        trans : isTrans _≺_
+        trans (_ , b₀) (_ , b₁) (_ , b₂) (inl b₀≺b₁) (inl b₁≺b₂)
+          = inl (transB b₀ b₁ b₂ b₀≺b₁ b₁≺b₂)
+        trans (_ , b₀) _ _ (inl b₀≺b₁) (inr (b₁≡b₂ , _))
+          = inl (subst (b₀ ≺ₛ_) b₁≡b₂ b₀≺b₁)
+        trans _ _ (_ , b₂) (inr (b₀≡b₁ , _)) (inl b₁≺b₂)
+          = inl (subst (_≺ₛ b₂) (sym b₀≡b₁) b₁≺b₂)
+        trans (a₀ , _) (a₁ , _) (a₂ , _)
+              (inr (b₀≡b₁ , a₀≺a₁))
+              (inr (b₁≡b₂ , a₁≺a₂))
+          = inr ((b₀≡b₁ ∙ b₁≡b₂) , (transA a₀ a₁ a₂ a₀≺a₁ a₁≺a₂))
+
+        wos : IsWoset _≺_
+        wos = iswoset set prop well weak trans
diff --git a/Cubical/Data/Ordinal/Properties.agda b/Cubical/Data/Ordinal/Properties.agda
new file mode 100644
index 0000000000..0cfbd9d98c
--- /dev/null
+++ b/Cubical/Data/Ordinal/Properties.agda
@@ -0,0 +1,299 @@
+{-
+
+This file contains:
+
+- Properties of ordinals
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Data.Ordinal.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Functions.Embedding
+
+open import Cubical.Data.Ordinal.Base
+open import Cubical.Data.Empty as ⊥ using (⊥ ; ⊥* ; isProp⊥*)
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum as ⊎ hiding (rec ; elim ; map)
+open import Cubical.Data.Unit
+
+open import Cubical.Induction.WellFounded
+
+open import Cubical.Relation.Binary.Base
+open import Cubical.Relation.Binary.Extensionality
+open import Cubical.Relation.Binary.Order.Woset
+open import Cubical.Relation.Binary.Order.Woset.Simulation
+open import Cubical.Relation.Binary.Order
+
+private
+  variable
+    ℓ : Level
+
+propOrd : (P : Type ℓ) → isProp P → Ord {ℓ}
+propOrd {ℓ} P prop = P , (wosetstr _<_ (iswoset set prp well weak trans))
+  where
+    open BinaryRelation
+    _<_ : P → P → Type ℓ
+    a < b = ⊥*{ℓ}
+
+    set : isSet P
+    set = isProp→isSet prop
+
+    prp : isPropValued _<_
+    prp _ _ = isProp⊥*
+
+    well : WellFounded _<_
+    well _ = acc (λ _ → ⊥.elim*)
+
+    weak : isWeaklyExtensional _<_
+    weak = ≺×→≡→isWeaklyExtensional _<_ set prp λ x y _ → prop x y
+
+    trans : isTrans _<_
+    trans _ _ _ = ⊥.elim*
+
+𝟘 𝟙 : Ord {ℓ}
+𝟘 {ℓ} = propOrd (⊥* {ℓ}) (isProp⊥*)
+𝟙 {ℓ} = propOrd (Unit* {ℓ}) (isPropUnit*)
+
+isLeast𝟘 : ∀{ℓ} → isLeast (isPoset→isPreorder isPoset≼) ((Ord {ℓ}) , (id↪ (Ord {ℓ}))) (𝟘 {ℓ})
+isLeast𝟘 _ = ⊥.elim* , (⊥.elim* , ⊥.elim*)
+
+-- The successor of 𝟘 is 𝟙
+suc𝟘 : suc (𝟘 {ℓ}) ≡ 𝟙 {ℓ}
+suc𝟘 = equivFun (WosetPath _ _) (eq , makeIsWosetEquiv eq eqsuc λ _ _ → ⊥.elim*)
+  where
+    eq : ⟨ 𝟘 ⟩ ⊎ Unit* ≃ ⟨ 𝟙 ⟩
+    eq = ⊎-IdL-⊥*-≃
+
+    eqsuc : _
+    eqsuc (inr x) (inr y) = ⊥.elim*
+
++IdR : (α : Ord {ℓ}) → α + 𝟘 {ℓ} ≡ α
++IdR α = equivFun (WosetPath _ _) (eq , (makeIsWosetEquiv eq eqα λ _ _ x≺y → x≺y))
+  where
+    eq : ⟨ α ⟩ ⊎ ⟨ 𝟘 ⟩ ≃ ⟨ α ⟩
+    eq = ⊎-IdR-⊥*-≃
+
+    eqα : _
+    eqα (inl x) (inl y) x≺y = x≺y
+
++IdL : (α : Ord {ℓ}) → 𝟘 {ℓ} + α ≡ α
++IdL α = equivFun (WosetPath _ _) (eq , (makeIsWosetEquiv eq eqα λ _ _ x≺y → x≺y))
+  where
+    eq : ⟨ 𝟘 ⟩ ⊎ ⟨ α ⟩ ≃ ⟨ α ⟩
+    eq = ⊎-IdL-⊥*-≃
+
+    eqα : (x y : ⟨ 𝟘 ⟩ ⊎ ⟨ α ⟩)
+        → ((𝟘 + α) .snd WosetStr.≺ x) y
+        → (α .snd WosetStr.≺ equivFun eq x) (equivFun eq y)
+    eqα (inr x) (inr y) x≺y = x≺y
+
+-- The successor is just addition by 𝟙
+suc≡+𝟙 : (α : Ord {ℓ}) → suc α ≡ α + 𝟙 {ℓ}
+suc≡+𝟙 α = equivFun (WosetPath _ _) (eq , (makeIsWosetEquiv eq eqsucα eqα+𝟙))
+  where
+    eq : ⟨ suc α ⟩ ≃ ⟨ α ⟩ ⊎ ⟨ 𝟙 ⟩
+    eq = idEquiv ⟨ suc α ⟩
+
+    eqsucα : _
+    eqsucα (inl x) (inl y) x≺y = x≺y
+    eqsucα (inl x) (inr y) _ = tt*
+    eqsucα (inr x) (inl y) = ⊥.elim*
+    eqsucα (inr x) (inr y) = ⊥.elim*
+
+    eqα+𝟙 : _
+    eqα+𝟙 (inl x) (inl y) x≺y = x≺y
+    eqα+𝟙 (inl x) (inr y) _ = tt*
+    eqα+𝟙 (inr x) (inl y) = ⊥.elim*
+    eqα+𝟙 (inr x) (inr y) = ⊥.elim*
+
+-- Successor is strictly increasing, though we can't prove it's the smallest ordinal greater than its predecessor
+suc≺ : (α : Ord {ℓ}) → α ≺ suc α
+suc≺ α = (inr tt*) , (eq , makeIsWosetEquiv eq eqsucα eqαsuc)
+  where
+    fun : ⟨ suc α ↓ inr tt* ⟩ → ⟨ α ⟩
+    fun (inl a , _) = a
+
+    iseq : isEquiv fun
+    fst (fst (equiv-proof iseq a)) = (inl a) , tt*
+    snd (fst (equiv-proof iseq a)) = refl
+    snd (equiv-proof iseq a) ((inl x , _) , x≡a)
+      = Σ≡Prop (λ _ → IsWoset.is-set (WosetStr.isWoset (str α)) _ _)
+                (Σ≡Prop lem (cong inl (sym x≡a)))
+      where lem : (y : ⟨ suc α ⟩) → isProp _
+            lem (inl y) = isPropUnit*
+            lem (inr _) = ⊥.elim*
+    eq : ⟨ suc α ↓ inr tt* ⟩ ≃ ⟨ α ⟩
+    eq = fun , iseq
+
+    eqsucα : _
+    eqsucα (inl x , _) (inl y , _) x<y = x<y
+
+    eqαsuc : _
+    eqαsuc x y x≺y = x≺y
+
+·IdR : (α : Ord {ℓ}) → α · 𝟙 {ℓ} ≡ α
+·IdR α = equivFun (WosetPath _ _) (eq , makeIsWosetEquiv eq eqα𝟙 eqα)
+  where
+    eq : ⟨ α ⟩ × ⟨ 𝟙 ⟩ ≃ ⟨ α ⟩
+    eq = isoToEquiv rUnit*×Iso
+
+    eqα𝟙 : _
+    eqα𝟙 (x , _) (y , _) (inl tt≺tt) = ⊥.rec (IsStrictPoset.is-irrefl
+                                                (isWoset→isStrictPoset
+                                                   (WosetStr.isWoset (str 𝟙)))
+                                               tt* tt≺tt)
+    eqα𝟙 (x , _) (y , _) (inr (_ , x≺y)) = x≺y
+
+    eqα : _
+    eqα x y x≺y = inr ((isPropUnit* _ _) , x≺y)
+
+·IdL : (α : Ord {ℓ}) → 𝟙 {ℓ} · α ≡ α
+·IdL α = equivFun (WosetPath _ _) (eq , makeIsWosetEquiv eq eq𝟙α eqα)
+  where
+    eq : ⟨ 𝟙 ⟩ × ⟨ α ⟩ ≃ ⟨ α ⟩
+    eq = isoToEquiv lUnit*×Iso
+
+    eq𝟙α : _
+    eq𝟙α (_ , x) (_ , y) (inr (_ , tt≺tt)) = ⊥.rec
+                                               (IsStrictPoset.is-irrefl
+                                                (isWoset→isStrictPoset
+                                                  (WosetStr.isWoset (str 𝟙)))
+                                                tt* tt≺tt)
+    eq𝟙α (_ , x) (_ , y) (inl x≺y) = x≺y
+
+    eqα : _
+    eqα x y x≺y = inl x≺y
+
+·AnnihilR : (α : Ord {ℓ}) → α · 𝟘 {ℓ} ≡ 𝟘 {ℓ}
+·AnnihilR α = equivFun (WosetPath _ _)
+                       (eq , makeIsWosetEquiv eq (λ b _ _ → ⊥.elim* (b .snd)) ⊥.elim*)
+  where
+    eq : ⟨ α ⟩ × ⟨ 𝟘 ⟩ ≃ ⟨ 𝟘 ⟩
+    eq = (⊥.elim* ∘ snd) , (record { equiv-proof = ⊥.elim* })
+
+·AnnihilL : (α : Ord {ℓ}) → 𝟘 {ℓ} · α ≡ 𝟘 {ℓ}
+·AnnihilL α = equivFun (WosetPath _ _)
+                       (eq , makeIsWosetEquiv eq (λ b _ _ → ⊥.elim* (b .fst)) ⊥.elim*)
+  where
+    eq : ⟨ 𝟘 ⟩ × ⟨ α ⟩ ≃ ⟨ 𝟘 ⟩
+    eq = (⊥.elim* ∘ fst) , (record { equiv-proof = ⊥.elim*  })
+
++Assoc : (α β γ : Ord {ℓ}) → (α + β) + γ ≡ α + (β + γ)
++Assoc α β γ = equivFun (WosetPath _ _) (eq , makeIsWosetEquiv eq eq→ eq←)
+  where
+    eq : (⟨ α ⟩ ⊎ ⟨ β ⟩) ⊎ ⟨ γ ⟩ ≃ ⟨ α ⟩ ⊎ (⟨ β ⟩ ⊎ ⟨ γ ⟩)
+    eq = ⊎-assoc-≃
+
+    eq→ : _
+    eq→ (inl (inl x)) (inl (inl y)) x≺y = x≺y
+    eq→ (inl (inl x)) (inl (inr y)) x≺y = tt*
+    eq→ (inl (inr x)) (inl (inl y)) = ⊥.elim*
+    eq→ (inl (inr x)) (inl (inr y)) x≺y = x≺y
+    eq→ (inl (inl x)) (inr y) x≺y = tt*
+    eq→ (inl (inr x)) (inr y) x≺y = tt*
+    eq→ (inr x) (inl (inl y)) = ⊥.elim*
+    eq→ (inr x) (inl (inr y)) = ⊥.elim*
+    eq→ (inr x) (inr y) x≺y = x≺y
+
+    eq← : _
+    eq← (inl x) (inl y) x≺y = x≺y
+    eq← (inl x) (inr (inl y)) x≺y = tt*
+    eq← (inl x) (inr (inr y)) x≺y = tt*
+    eq← (inr (inl x)) (inl y) = ⊥.elim*
+    eq← (inr (inr x)) (inl y) = ⊥.elim*
+    eq← (inr (inl x)) (inr (inl y)) x≺y = x≺y
+    eq← (inr (inl x)) (inr (inr y)) x≺y = tt*
+    eq← (inr (inr x)) (inr (inl y)) = ⊥.elim*
+    eq← (inr (inr x)) (inr (inr y)) x≺y = x≺y
+
+·Assoc : (α β γ : Ord {ℓ}) → (α · β) · γ ≡ α · (β · γ)
+·Assoc α β γ = equivFun (WosetPath _ _) (eq , makeIsWosetEquiv eq eq→ eq←)
+  where
+    eq : (⟨ α ⟩ × ⟨ β ⟩) × ⟨ γ ⟩ ≃ ⟨ α ⟩ × (⟨ β ⟩ × ⟨ γ ⟩)
+    eq = Σ-assoc-≃
+
+    eq→ : _
+    eq→ ((xa , xb) , xc) ((ya , yb) , yc) (inl xc≺yc)
+      = inl (inl xc≺yc)
+    eq→ ((xa , xb) , xc) ((ya , yb) , yc) (inr (xc≡yc , inl xb≺yb))
+      = inl (inr (xc≡yc , xb≺yb))
+    eq→ ((xa , xb) , xc) ((ya , yb) , yc) (inr (xc≡yc , inr (xb≡yb , xa≺ya)))
+      = inr ((≡-× xb≡yb xc≡yc) , xa≺ya)
+
+    eq← : _
+    eq← (xa , xb , xc) (ya , yb , yc) (inl (inl xc≺yc))
+      = inl xc≺yc
+    eq← (xa , xb , xc) (ya , yb , yc) (inl (inr (xc≡yc , xb≺yb)))
+      = inr (xc≡yc , (inl xb≺yb))
+    eq← (xa , xb , xc) (ya , yb , yc) (inr (xbxc≡ybyc , xa≺ya))
+      = inr ((PathPΣ xbxc≡ybyc .snd) , (inr ((PathPΣ xbxc≡ybyc .fst) , xa≺ya)))
+
+≺-o+ : {β γ : Ord {ℓ}} → (α : Ord {ℓ}) → β ≺ γ → (α + β) ≺ (α + γ)
+≺-o+ {ℓ} {β} {γ} α (g , γ↓g≃β , wEq) = inr g , eq , makeIsWosetEquiv eq eq→ eq←
+  where
+    fun : ⟨ (α + γ) ↓ inr g ⟩ → ⟨ α + β ⟩
+    fun (inl x , _) = inl x
+    fun (inr x , p) = inr (equivFun γ↓g≃β (x , p))
+
+    inv : ⟨ α + β ⟩ → ⟨ (α + γ) ↓ inr g ⟩
+    inv (inl x) = inl x , tt*
+    inv (inr x) = inr (invEq γ↓g≃β x .fst) , invEq γ↓g≃β x .snd
+
+    is : Iso ⟨ (α + γ) ↓ inr g ⟩ ⟨ α + β ⟩
+    Iso.fun is = fun
+    Iso.inv is = inv
+    Iso.rightInv is (inl x) = refl
+    Iso.rightInv is (inr x) = cong inr (secEq γ↓g≃β x)
+    Iso.leftInv  is (inl x , _) = ΣPathP (refl , (isPropUnit* _ _))
+    Iso.leftInv  is (inr x , x≺g)
+      = ΣPathP (cong inr (PathPΣ (retEq γ↓g≃β (x , x≺g)) .fst)
+                        , PathPΣ (retEq γ↓g≃β (x , x≺g)) .snd)
+
+    eq : _
+    eq = isoToEquiv is
+
+    eq→ : _
+    eq→ (inl x , _) (inl y , _) x≺y = x≺y
+    eq→ (inl x , _) (inr y , _) _ = tt*
+    eq→ (inr x , x≺g) (inl y , y≺g) = ⊥.elim*
+    eq→ (inr x , x≺g) (inr y , y≺g) x≺y
+      = equivFun (IsWosetEquiv.pres≺ wEq (x , x≺g) (y , y≺g)) x≺y
+
+    eq← : _
+    eq← (inl x) (inl y) x≺y = x≺y
+    eq← (inl x) (inr y) _ = tt*
+    eq← (inr x) (inl y) = ⊥.elim*
+    eq← (inr x) (inr y) x≺y = equivFun (IsWosetEquiv.pres≺⁻ wEq x y) x≺y
+
+·DistR+ : (α β γ : Ord {ℓ}) → α · (β + γ) ≡ (α · β) + (α · γ)
+·DistR+ α β γ = equivFun (WosetPath _ _) (eq , makeIsWosetEquiv eq eq→ eq←)
+  where
+    eq : ⟨ α ⟩ × (⟨ β ⟩ ⊎ ⟨ γ ⟩) ≃ (⟨ α ⟩ × ⟨ β ⟩) ⊎ (⟨ α ⟩ × ⟨ γ ⟩)
+    eq = isoToEquiv ×DistR⊎Iso
+
+    eq→ : _
+    eq→ (xa , inl xb) (ya , inl yb) (inl xg≺yg) = inl xg≺yg
+    eq→ (xa , inl xb) (ya , inl yb) (inr (xb≡yb , xa≺ya))
+      = inr (isEmbedding→Inj isEmbedding-inl xb yb xb≡yb , xa≺ya)
+    eq→ (xa , inl xb) (ya , inr yg) (inl x≺y) = x≺y
+    eq→ (xa , inl xb) (ya , inr yg) (inr (xb≡yg , _)) = ⊥.rec* (⊎Path.encode _ _ xb≡yg)
+    eq→ (xa , inr xg) (ya , inl yb) (inr (xg≡yb , _)) = ⊥.rec* (⊎Path.encode _ _ xg≡yb)
+    eq→ (xa , inr xg) (ya , inr yg) (inl xg≺yg) = inl xg≺yg
+    eq→ (xa , inr xg) (ya , inr yg) (inr (xg≡yg , xa≺ya))
+      = inr (isEmbedding→Inj isEmbedding-inr xg yg xg≡yg , xa≺ya)
+
+    eq← : _
+    eq← (inl (xa , xb)) (inl (ya , yb)) (inl xb≺yb) = inl xb≺yb
+    eq← (inl (xa , xb)) (inl (ya , yb)) (inr (xb≡yb , xa≺ya))
+      = inr (cong inl xb≡yb , xa≺ya)
+    eq← (inl (xa , xb)) (inr (ya , yg)) _ = inl tt*
+    eq← (inr x) (inl (ya , yb)) = ⊥.elim*
+    eq← (inr xg) (inr yg) (inl xg≺yg) = inl xg≺yg
+    eq← (inr (xa , xg)) (inr (ya , yg)) (inr (xg≡yg , xa≺ya))
+      = inr (cong inr xg≡yg , xa≺ya)
diff --git a/Cubical/Data/Sum/Properties.agda b/Cubical/Data/Sum/Properties.agda
index b469b59ccf..2be7be3c1f 100644
--- a/Cubical/Data/Sum/Properties.agda
+++ b/Cubical/Data/Sum/Properties.agda
@@ -222,15 +222,15 @@ rightInv Σ⊎Iso (inr (b , eb)) = refl
 leftInv Σ⊎Iso (inl a , ea) = refl
 leftInv Σ⊎Iso (inr b , eb) = refl
 
-×DistL⊎Iso : Iso (A × (B ⊎ C)) ((A × B) ⊎ (A × C))
-fun ×DistL⊎Iso (a , inl b) = inl (a , b)
-fun ×DistL⊎Iso (a , inr c) = inr (a , c)
-inv ×DistL⊎Iso (inl (a , b)) = a , inl b
-inv ×DistL⊎Iso (inr (a , c)) = a , inr c
-rightInv ×DistL⊎Iso (inl (a , b)) = refl
-rightInv ×DistL⊎Iso (inr (a , c)) = refl
-leftInv ×DistL⊎Iso (a , inl b) = refl
-leftInv ×DistL⊎Iso (a , inr c) = refl
+×DistR⊎Iso : Iso (A × (B ⊎ C)) ((A × B) ⊎ (A × C))
+fun ×DistR⊎Iso (a , inl b) = inl (a , b)
+fun ×DistR⊎Iso (a , inr c) = inr (a , c)
+inv ×DistR⊎Iso (inl (a , b)) = a , inl b
+inv ×DistR⊎Iso (inr (a , c)) = a , inr c
+rightInv ×DistR⊎Iso (inl (a , b)) = refl
+rightInv ×DistR⊎Iso (inr (a , c)) = refl
+leftInv ×DistR⊎Iso (a , inl b) = refl
+leftInv ×DistR⊎Iso (a , inr c) = refl
 
 Π⊎≃ : ((x : A ⊎ B) → E x) ≃ ((a : A) → E (inl a)) × ((b : B) → E (inr b))
 Π⊎≃ = isoToEquiv Π⊎Iso
diff --git a/Cubical/HITs/SetTruncation/Properties.agda b/Cubical/HITs/SetTruncation/Properties.agda
index 56bd3914ff..33d3deefa0 100644
--- a/Cubical/HITs/SetTruncation/Properties.agda
+++ b/Cubical/HITs/SetTruncation/Properties.agda
@@ -24,8 +24,11 @@ open import Cubical.HITs.PropositionalTruncation
 
 private
   variable
-    ℓ ℓ' ℓ'' : Level
-    A B C D : Type ℓ
+    ℓ ℓ' ℓ'' ℓa ℓb ℓc ℓd : Level
+    A : Type ℓa
+    B : Type ℓb
+    C : Type ℓc
+    D : Type ℓd
 
 isSetPathImplicit : {x y : ∥ A ∥₂} → isSet (x ≡ y)
 isSetPathImplicit = isOfHLevelPath 2 squash₂ _ _
@@ -72,19 +75,20 @@ elim2 Cset f (squash₂ x y p q i j) z =
 --                     (λ a → elim (λ _ → Cset _ _) (f a))
 
 -- TODO: generalize
-elim3 : {B : (x y z : ∥ A ∥₂) → Type ℓ}
-        (Bset : ((x y z : ∥ A ∥₂) → isSet (B x y z)))
-        (g : (a b c : A) → B ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂)
-        (x y z : ∥ A ∥₂) → B x y z
-elim3 Bset g = elim2 (λ _ _ → isSetΠ (λ _ → Bset _ _ _))
-                     (λ a b → elim (λ _ → Bset _ _ _) (g a b))
-
-elim4 : {B : (w x y z : ∥ A ∥₂) → Type ℓ}
-        (Bset : ((w x y z : ∥ A ∥₂) → isSet (B w x y z)))
-        (g : (a b c d : A) → B ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂ ∣ d ∣₂)
-        (w x y z : ∥ A ∥₂) → B w x y z
-elim4 Bset g = elim3 (λ _ _ _ → isSetΠ λ _ → Bset _ _ _ _)
-                     λ a b c → elim (λ _ → Bset _ _ _ _) (g a b c)
+elim3 : {D : ∥ A ∥₂ → ∥ B ∥₂ → ∥ C ∥₂ → Type ℓ}
+        (Dset : ((x : ∥ A ∥₂) (y : ∥ B ∥₂) (z : ∥ C ∥₂) → isSet (D x y z)))
+        (g : (a : A) (b : B) (c : C) → D ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂)
+        (x : ∥ A ∥₂) (y : ∥ B ∥₂) (z : ∥ C ∥₂) → D x y z
+elim3 Dset g = elim2 (λ _ _ → isSetΠ (λ _ → Dset _ _ _))
+                     (λ a b → elim (λ _ → Dset _ _ _) (g a b))
+
+elim4 : {E : ∥ A ∥₂ → ∥ B ∥₂ → ∥ C ∥₂ → ∥ D ∥₂ → Type ℓ}
+        (Eset : ((w : ∥ A ∥₂) (x : ∥ B ∥₂) (y : ∥ C ∥₂) (z : ∥ D ∥₂)
+              → isSet (E w x y z)))
+        (g : (a : A) (b : B) (c : C) (d : D) → E ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂ ∣ d ∣₂)
+        (w : ∥ A ∥₂) (x : ∥ B ∥₂) (y : ∥ C ∥₂) (z : ∥ D ∥₂) → E w x y z
+elim4 Eset g = elim3 (λ _ _ _ → isSetΠ λ _ → Eset _ _ _ _)
+                     λ a b c → elim (λ _ → Eset _ _ _ _) (g a b c)
 
 
 -- the recursor for maps into groupoids following the "HIT proof" in:
diff --git a/Cubical/Induction/WellFounded.agda b/Cubical/Induction/WellFounded.agda
index d82de49855..885d17892d 100644
--- a/Cubical/Induction/WellFounded.agda
+++ b/Cubical/Induction/WellFounded.agda
@@ -4,9 +4,6 @@ module Cubical.Induction.WellFounded where
 
 open import Cubical.Foundations.Prelude
 
-Rel : ∀{ℓ} → Type ℓ → ∀ ℓ' → Type _
-Rel A ℓ = A → A → Type ℓ
-
 module _ {ℓ ℓ'} {A : Type ℓ} (_<_ : A → A → Type ℓ') where
   WFRec : ∀{ℓ''} → (A → Type ℓ'') → A → Type _
   WFRec P x = ∀ y → y < x → P y
@@ -23,6 +20,9 @@ module _ {ℓ ℓ'} {A : Type ℓ} {_<_ : A → A → Type ℓ'} where
   isPropAcc x (acc p) (acc q)
     = λ i → acc (λ y y<x → isPropAcc y (p y y<x) (q y y<x) i)
 
+  isPropWellFounded : isProp (WellFounded _<_)
+  isPropWellFounded p q i a = isPropAcc a (p a) (q a) i
+
   access : ∀{x} → Acc _<_ x → WFRec _<_ (Acc _<_) x
   access (acc r) = r
 
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index 13339c4933..d583115a76 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -19,11 +19,13 @@ open import Cubical.HITs.PropositionalTruncation as ∥₁
 
 open import Cubical.Relation.Nullary.Base
 
+open import Cubical.Induction.WellFounded
+
 private
   variable
     ℓA ℓ≅A ℓA' ℓ≅A' : Level
 
-Rel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
+Rel : ∀ {ℓa ℓb} (A : Type ℓa) (B : Type ℓb) (ℓ' : Level) → Type (ℓ-max (ℓ-max ℓa ℓb) (ℓ-suc ℓ'))
 Rel A B ℓ' = A → B → Type ℓ'
 
 PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
@@ -95,6 +97,9 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
   isIrrefl×isTrans→isAsym (irrefl , trans) a₀ a₁ Ra₀a₁ Ra₁a₀
     = irrefl a₀ (trans a₀ a₁ a₀ Ra₀a₁ Ra₁a₀)
 
+  WellFounded→isIrrefl : WellFounded R → isIrrefl
+  WellFounded→isIrrefl well = WFI.induction well λ a f Raa → f a Raa Raa
+
   IrreflKernel : Rel A A (ℓ-max ℓ ℓ')
   IrreflKernel a b = R a b × (¬ a ≡ b)
 
diff --git a/Cubical/Relation/Binary/Extensionality.agda b/Cubical/Relation/Binary/Extensionality.agda
index 41b789887f..f67edd57bb 100644
--- a/Cubical/Relation/Binary/Extensionality.agda
+++ b/Cubical/Relation/Binary/Extensionality.agda
@@ -6,16 +6,50 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Transport
-open import Cubical.Data.Sigma
 open import Cubical.Relation.Binary.Base
 
+open import Cubical.Data.Sigma
+
 module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where
 
   ≡→≺Equiv : (x y : A) → x ≡ y → ∀ z → (z ≺ x) ≃ (z ≺ y)
   ≡→≺Equiv _ _ p z = substEquiv (z ≺_) p
 
   isWeaklyExtensional : Type _
-  isWeaklyExtensional = ∀ {x y} → isEquiv (≡→≺Equiv x y)
+  isWeaklyExtensional = ∀ x y → isEquiv (≡→≺Equiv x y)
 
   isPropIsWeaklyExtensional : isProp isWeaklyExtensional
-  isPropIsWeaklyExtensional = isPropImplicitΠ2 λ _ _ → isPropIsEquiv _
+  isPropIsWeaklyExtensional = isPropΠ2 λ _ _ → isPropIsEquiv _
+
+  {- HoTT Definition 10.3.9 has extensionality defined under these terms.
+     We prove that under those conditions, it implies our more hlevel-friendly
+     definition.
+  -}
+
+  ≺Equiv→≡→isWeaklyExtensional : isSet A → BinaryRelation.isPropValued _≺_
+                             → ((x y : A) → (∀ z → ((z ≺ x) ≃ (z ≺ y))) → x ≡ y)
+                             → isWeaklyExtensional
+  ≺Equiv→≡→isWeaklyExtensional setA prop f a b
+    = propBiimpl→Equiv (setA a b)
+                       (isPropΠ (λ z → isOfHLevel≃ 1
+                                                   (prop z a)
+                                                   (prop z b)))
+                       (≡→≺Equiv a b)
+                       (λ g → f a b λ z → g z) .snd
+
+  ≺×→≡→isWeaklyExtensional : isSet A → BinaryRelation.isPropValued _≺_
+                            → ((x y : A) → (∀ z → ((z ≺ x) → (z ≺ y))
+                                                × ((z ≺ y) → (z ≺ x))) → x ≡ y)
+                            → isWeaklyExtensional
+  ≺×→≡→isWeaklyExtensional setA prop f a b
+    = propBiimpl→Equiv (setA a b)
+                       (isPropΠ (λ z → isOfHLevel≃ 1
+                                                   (prop z a)
+                                                   (prop z b)))
+                       (≡→≺Equiv a b)
+                       (λ g → f a b λ z → (g z .fst) , invEq (g z)) .snd
+
+  isWeaklyExtensional→≺Equiv→≡ : isWeaklyExtensional
+                                → (x y : A) → (∀ z → (z ≺ x) ≃ (z ≺ y)) → x ≡ y
+  isWeaklyExtensional→≺Equiv→≡ weak x y
+    = invIsEq (weak x y)
diff --git a/Cubical/Relation/Binary/Order/Woset.agda b/Cubical/Relation/Binary/Order/Woset.agda
new file mode 100644
index 0000000000..1961de1b2d
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Woset.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+module Cubical.Relation.Binary.Order.Woset where
+
+open import Cubical.Relation.Binary.Order.Woset.Base public
+open import Cubical.Relation.Binary.Order.Woset.Properties public
diff --git a/Cubical/Relation/Binary/Order/Woset/Base.agda b/Cubical/Relation/Binary/Order/Woset/Base.agda
new file mode 100644
index 0000000000..730c2fe618
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Woset/Base.agda
@@ -0,0 +1,206 @@
+{-# OPTIONS --safe #-}
+module Cubical.Relation.Binary.Order.Woset.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.HalfAdjoint
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.SIP
+
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Reflection.StrictEquiv
+
+open import Cubical.Displayed.Base
+open import Cubical.Displayed.Auto
+open import Cubical.Displayed.Record
+open import Cubical.Displayed.Universe
+
+open import Cubical.Relation.Binary.Base
+open import Cubical.Relation.Binary.Extensionality
+
+open import Cubical.Induction.WellFounded
+
+open Iso
+open BinaryRelation
+
+
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ₀ ℓ₀' ℓ₁ ℓ₁' ℓ₂ ℓ₂' : Level
+
+record IsWoset {A : Type ℓ} (_≺_ : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
+  no-eta-equality
+  constructor iswoset
+
+  field
+    is-set : isSet A
+    is-prop-valued : isPropValued _≺_
+    is-well-founded : WellFounded _≺_
+    is-weakly-extensional : isWeaklyExtensional _≺_
+    is-trans : isTrans _≺_
+
+unquoteDecl IsWosetIsoΣ = declareRecordIsoΣ IsWosetIsoΣ (quote IsWoset)
+
+
+record WosetStr (ℓ' : Level) (A : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
+
+  constructor wosetstr
+
+  field
+    _≺_     : A → A → Type ℓ'
+    isWoset : IsWoset _≺_
+
+  infixl 7 _≺_
+
+  open IsWoset isWoset public
+
+Woset : ∀ ℓ ℓ' → Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ'))
+Woset ℓ ℓ' = TypeWithStr ℓ (WosetStr ℓ')
+
+woset : (A : Type ℓ) (_≺_ : A → A → Type ℓ') (h : IsWoset _≺_) → Woset ℓ ℓ'
+woset A _≺_ h = A , wosetstr _≺_ h
+
+record IsWosetEquiv {A : Type ℓ₀} {B : Type ℓ₁}
+  (M : WosetStr ℓ₀' A) (e : A ≃ B) (N : WosetStr ℓ₁' B)
+  : Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁')
+  where
+  constructor
+   iswosetequiv
+  -- Shorter qualified names
+  private
+    module M = WosetStr M
+    module N = WosetStr N
+
+  field
+    pres≺ : (x y : A) → x M.≺ y ≃ equivFun e x N.≺ equivFun e y
+
+  pres≺⁻ : (x y : B) → x N.≺ y ≃ invEq e x M.≺ invEq e y
+  pres≺⁻ x y = invEquiv
+                 (pres≺ (invEq e x) (invEq e y) ∙ₑ
+                  substEquiv (N._≺ equivFun e (invEq e y)) (secEq e x) ∙ₑ
+                  substEquiv (x N.≺_) (secEq e y))
+
+
+WosetEquiv : (M : Woset ℓ₀ ℓ₀') (M : Woset ℓ₁ ℓ₁') → Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁'))
+WosetEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsWosetEquiv (M .snd) e (N .snd)
+
+invWosetEquiv : {M : Woset ℓ₀ ℓ₀'} {N : Woset ℓ₁ ℓ₁'} → WosetEquiv M N → WosetEquiv N M
+invWosetEquiv (M≃N , iswq) = invEquiv M≃N , iswosetequiv (IsWosetEquiv.pres≺⁻ iswq)
+
+compWosetEquiv : {M : Woset ℓ₀ ℓ₀'} {N : Woset ℓ₁ ℓ₁'} {O : Woset ℓ₂ ℓ₂'}
+               → WosetEquiv M N → WosetEquiv N O → WosetEquiv M O
+compWosetEquiv (M≃N , wqMN) (N≃O , wqNO) = (compEquiv M≃N N≃O)
+               , (iswosetequiv (λ x y
+               → compEquiv (IsWosetEquiv.pres≺ wqMN x y)
+                           (IsWosetEquiv.pres≺ wqNO (equivFun M≃N x) (equivFun M≃N y))))
+
+reflWosetEquiv : {M : Woset ℓ₀ ℓ₀'} → WosetEquiv M M
+reflWosetEquiv {M = M} = (idEquiv ⟨ M ⟩) , (iswosetequiv (λ _ _ → idEquiv _))
+
+isPropIsWoset : {A : Type ℓ} (_≺_ : A → A → Type ℓ') → isProp (IsWoset _≺_)
+isPropIsWoset _≺_ = isOfHLevelRetractFromIso 1 IsWosetIsoΣ
+  (isPropΣ isPropIsSet
+    λ isSetA → isPropΣ (isPropΠ2 (λ _ _ → isPropIsProp))
+      λ isPropValued≺ → isProp×2
+                         isPropWellFounded
+                         (isPropIsWeaklyExtensional _≺_)
+                         (isPropΠ5 λ x _ z _ _ → isPropValued≺ x z))
+
+private
+  unquoteDecl IsWosetEquivIsoΣ = declareRecordIsoΣ IsWosetEquivIsoΣ (quote IsWosetEquiv)
+
+isPropIsWosetEquiv : {A : Type ℓ₀} {B : Type ℓ₁}
+                   → (M : WosetStr ℓ₀' A) (e : A ≃ B) (N : WosetStr ℓ₁' B)
+                   → isProp (IsWosetEquiv M e N)
+isPropIsWosetEquiv M e N = isOfHLevelRetractFromIso 1 IsWosetEquivIsoΣ
+  (isPropΠ2 λ x y → isOfHLevel≃ 1
+    (IsWoset.is-prop-valued (WosetStr.isWoset M) x y)
+    (IsWoset.is-prop-valued (WosetStr.isWoset N) (e .fst x) (e .fst y)))
+
+𝒮ᴰ-Woset : DUARel (𝒮-Univ ℓ) (WosetStr ℓ') (ℓ-max ℓ ℓ')
+𝒮ᴰ-Woset =
+  𝒮ᴰ-Record (𝒮-Univ _) IsWosetEquiv
+    (fields:
+      data[ _≺_ ∣ autoDUARel _ _ ∣ pres≺ ]
+      prop[ isWoset ∣ (λ _ _ → isPropIsWoset _) ])
+    where
+    open WosetStr
+    open IsWoset
+    open IsWosetEquiv
+
+WosetPath : (M N : Woset ℓ ℓ') → WosetEquiv M N ≃ (M ≡ N)
+WosetPath = ∫ 𝒮ᴰ-Woset .UARel.ua
+
+isSetWoset : isSet (Woset ℓ ℓ')
+isSetWoset M N = isOfHLevelRespectEquiv 1 (WosetPath M N)
+  λ ((f , eqf) , wqf) ((g , eqg) , wqg)
+    → Σ≡Prop (λ e → isPropIsWosetEquiv (str M) e (str N))
+      (Σ≡Prop (λ _ → isPropIsEquiv _)
+        (funExt (WFI.induction wellM λ a ind
+          → isWeaklyExtensional→≺Equiv→≡ _≺ₙ_ weakN (f a) (g a) λ c
+            → propBiimpl→Equiv (propN c (f a)) (propN c (g a))
+  (λ c≺ₙfa → subst (_≺ₙ g a) (secEq (g , eqg) c)
+               (equivFun (IsWosetEquiv.pres≺ wqg (invEq (g , eqg) c) a)
+                (subst (_≺ₘ a)
+                 (sym
+                  (cong (invEq (g , eqg))
+                   (sym (secEq (f , eqf) c)
+                   ∙ ind (invEq (f , eqf) c)
+                    (subst (invEq (f , eqf) c ≺ₘ_) (retEq (f , eqf) a)
+                     (equivFun (IsWosetEquiv.pres≺⁻ wqf c (f a)) c≺ₙfa)))
+                   ∙ retEq (g , eqg) (invEq (f , eqf) c)))
+                 (subst (invEq (f , eqf) c ≺ₘ_)
+                   (retEq (f , eqf) a)
+                     (equivFun
+                       (IsWosetEquiv.pres≺⁻ wqf c (f a)) c≺ₙfa)))))
+   λ c≺ₙga → subst (_≺ₙ f a) (secEq (f , eqf) c)
+               (equivFun (IsWosetEquiv.pres≺ wqf (invEq (f , eqf) c) a)
+                 (subst (_≺ₘ a)
+                   (sym
+                     (retEq (f , eqf) (invEq (g , eqg) c))
+                     ∙ cong (invEq (f , eqf))
+                      (ind (invEq (g , eqg) c)
+                       (subst (invEq (g , eqg) c ≺ₘ_) (retEq (g , eqg) a)
+                        (equivFun (IsWosetEquiv.pres≺⁻ wqg c (g a)) c≺ₙga))
+                       ∙ secEq (g , eqg) c))
+                   (subst (invEq (g , eqg) c ≺ₘ_)
+                     (retEq (g , eqg) a)
+                       (equivFun
+                         (IsWosetEquiv.pres≺⁻ wqg c (g a)) c≺ₙga)))))))
+  where _≺ₘ_ = WosetStr._≺_ (str M)
+        _≺ₙ_ = WosetStr._≺_ (str N)
+
+        wosM = WosetStr.isWoset (str M)
+        wosN = WosetStr.isWoset (str N)
+
+        wellM = IsWoset.is-well-founded (wosM)
+
+        weakN = IsWoset.is-weakly-extensional (wosN)
+
+        propN = IsWoset.is-prop-valued (wosN)
+
+-- an easier way of establishing an equivalence of wosets
+module _ {P : Woset ℓ₀ ℓ₀'} {S : Woset ℓ₁ ℓ₁'} (e : ⟨ P ⟩ ≃ ⟨ S ⟩) where
+  private
+    module P = WosetStr (P .snd)
+    module S = WosetStr (S .snd)
+
+  module _ (isMon : ∀ x y → x P.≺ y → equivFun e x S.≺ equivFun e y)
+           (isMonInv : ∀ x y → x S.≺ y → invEq e x P.≺ invEq e y) where
+    open IsWosetEquiv
+    open IsWoset
+
+    makeIsWosetEquiv : IsWosetEquiv (P .snd) e (S .snd)
+    pres≺ makeIsWosetEquiv x y = propBiimpl→Equiv (P.isWoset .is-prop-valued _ _)
+                                                  (S.isWoset .is-prop-valued _ _)
+                                                  (isMon _ _) (isMonInv' _ _)
+      where
+      isMonInv' : ∀ x y → equivFun e x S.≺ equivFun e y → x P.≺ y
+      isMonInv' x y ex≺ey = transport (λ i → retEq e x i P.≺ retEq e y i) (isMonInv _ _ ex≺ey)
diff --git a/Cubical/Relation/Binary/Order/Woset/Properties.agda b/Cubical/Relation/Binary/Order/Woset/Properties.agda
new file mode 100644
index 0000000000..9a2e0a52e3
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Woset/Properties.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --safe #-}
+module Cubical.Relation.Binary.Order.Woset.Properties where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Binary.Base
+open import Cubical.Relation.Binary.Order.Woset.Base
+open import Cubical.Relation.Binary.Order.StrictPoset.Base
+
+open import Cubical.Induction.WellFounded
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _
+  {A : Type ℓ}
+  {R : Rel A A ℓ'}
+  where
+
+  open BinaryRelation
+
+  isWoset→isStrictPoset : IsWoset R → IsStrictPoset R
+  isWoset→isStrictPoset wos = isstrictposet
+                              (IsWoset.is-set wos)
+                              (IsWoset.is-prop-valued wos)
+                              irrefl
+                              (IsWoset.is-trans wos)
+                              (isIrrefl×isTrans→isAsym R
+                                (irrefl , (IsWoset.is-trans wos)))
+                        where irrefl : isIrrefl R
+                              irrefl = WellFounded→isIrrefl R
+                                       (IsWoset.is-well-founded wos)
+
+Woset→StrictPoset : Woset ℓ ℓ' → StrictPoset ℓ ℓ'
+Woset→StrictPoset (_ , wos) = _ , strictposetstr (WosetStr._≺_ wos)
+                                  (isWoset→isStrictPoset (WosetStr.isWoset wos))
diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda
new file mode 100644
index 0000000000..51b789b6e8
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda
@@ -0,0 +1,931 @@
+{-# OPTIONS --safe #-}
+{-
+  This treatment of well-orderings follows chapter 10.3 of the HoTT book
+-}
+module Cubical.Relation.Binary.Order.Woset.Simulation where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
+
+open import Cubical.HITs.PropositionalTruncation as ∥₁
+open import Cubical.HITs.SetQuotients as /₂
+
+open import Cubical.Induction.WellFounded
+
+open import Cubical.Functions.Embedding
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Relation.Binary.Order.Woset.Base
+open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Base
+open import Cubical.Relation.Binary.Extensionality
+open import Cubical.Relation.Binary.Order.Properties
+
+private
+  variable
+    ℓ ℓ' ℓa ℓa' ℓb ℓb' ℓc ℓc' ℓd ℓd' : Level
+
+-- We start with the presumption that the lifting property for a simulation
+-- must be truncated, but will prove subsequently that simulations are embeddings
+-- and that no truncation is needed
+isSimulation∃ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') (f : ⟨ A ⟩ → ⟨ B ⟩)
+              → Type (ℓ-max (ℓ-max (ℓ-max ℓa ℓa') ℓb) ℓb')
+isSimulation∃ A B f = monotone × ∃lifting
+  where _≺ᵣ_ = WosetStr._≺_ (str A)
+        _≺ₛ_ = WosetStr._≺_ (str B)
+
+        monotone = ∀ a a' → a ≺ᵣ a' → (f a) ≺ₛ (f a')
+
+        less : ∀ a → Type _
+        less a = Σ[ a' ∈ ⟨ A ⟩ ] a' ≺ᵣ a
+
+        ∃lifting = ∀ a b → b ≺ₛ (f a) → ∃[ (a' , _) ∈ less a ] f a' ≡ b
+
+isSimulation∃→isEmbedding : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') → ∀ f
+                          → isSimulation∃ A B f → isEmbedding f
+isSimulation∃→isEmbedding A B f (rrel , efib)
+  = injEmbedding setB
+    λ {a b} → WFI.induction wellR {P = λ a' → ∀ b' → f a' ≡ f b' → a' ≡ b'}
+              (λ a' ind b' fa'≡fb'
+                 → isWeaklyExtensional→≺Equiv→≡ _≺ᵣ_ weakR a' b'
+                   λ c → propBiimpl→Equiv (propR c a') (propR c b')
+                     (λ c≺ᵣa' → ∥₁.rec (propR c b')
+                                       (λ ((a'' , fa''≺ᵣb') , fc≡fa'')
+                                       → subst (_≺ᵣ b') (sym
+                                               (ind c c≺ᵣa' a'' (sym fc≡fa'')))
+                                         fa''≺ᵣb')
+                                  (efib b' (f c) (subst (f c ≺ₛ_) fa'≡fb'
+                                                        (rrel c a' c≺ᵣa'))))
+                     λ c≺ᵣb' → ∥₁.rec (propR c a')
+                                      (λ ((b'' , fb''≺ᵣa') , fc≡fb'')
+                                      → subst (_≺ᵣ a')
+                                              (ind b'' fb''≺ᵣa' c
+                                                fc≡fb'') fb''≺ᵣa')
+                                 (efib a' (f c) (subst (f c ≺ₛ_)
+                                       (sym fa'≡fb') (rrel c b' c≺ᵣb')))) a b
+    where _≺ᵣ_ = WosetStr._≺_ (str A)
+          _≺ₛ_ = WosetStr._≺_ (str B)
+
+          wosR = WosetStr.isWoset (str A)
+          wosS = WosetStr.isWoset (str B)
+
+          setB = IsWoset.is-set wosS
+
+          wellR = IsWoset.is-well-founded wosR
+          weakR = IsWoset.is-weakly-extensional wosR
+          propR = IsWoset.is-prop-valued wosR
+
+-- With the fact that it's an embedding, we can do away with the truncation
+isSimulation : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') (f : ⟨ A ⟩ → ⟨ B ⟩)
+             → Type (ℓ-max (ℓ-max (ℓ-max ℓa ℓa') ℓb) ℓb')
+isSimulation A B f = monotone × lifting
+  where _≺ᵣ_ = WosetStr._≺_ (str A)
+        _≺ₛ_ = WosetStr._≺_ (str B)
+
+        monotone = ∀ a a' → a ≺ᵣ a' → (f a) ≺ₛ (f a')
+
+        less : ∀ a → Type _
+        less a = Σ[ a' ∈ ⟨ A ⟩ ] a' ≺ᵣ a
+
+        lifting = ∀ a b → b ≺ₛ (f a) → fiber {A = less a} (f ∘ fst) b
+
+isSimulation∃→isSimulation : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') → ∀ f
+                           → isSimulation∃ A B f → isSimulation A B f
+isSimulation∃→isSimulation A B f (mono , lifting) = mono
+                           , (λ a b b≺fa → ∥₁.rec
+                           (isEmbedding→hasPropFibers (isEmbedding-∘
+                             (isSimulation∃→isEmbedding A B f (mono , lifting))
+                             (λ _ _ → isEmbeddingFstΣProp λ _ → propR _ _)) b)
+                             (λ x → x) (lifting a b b≺fa))
+                           where propR = IsWoset.is-prop-valued (WosetStr.isWoset (str A))
+
+isSimulation→isEmbedding : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') → ∀ f
+                         → isSimulation A B f → isEmbedding f
+isSimulation→isEmbedding A B f (rrel , efib)
+  = injEmbedding setB
+    λ {a b} → WFI.induction wellR {P = λ a' → ∀ b' → f a' ≡ f b' → a' ≡ b'}
+            (λ a' ind b' fa'≡fb' → isWeaklyExtensional→≺Equiv→≡
+               _≺ᵣ_ weakR a' b' λ c → propBiimpl→Equiv
+                 (propR c a') (propR c b')
+                 (λ c≺ᵣa' → subst (_≺ᵣ b')
+                            (sym (ind c c≺ᵣa'
+                                 (efib b' (f c)
+                                   (subst (f c ≺ₛ_) fa'≡fb'
+                                          (rrel c a' c≺ᵣa')) .fst .fst)
+                                 (sym (efib b' (f c) (subst (f c ≺ₛ_)
+                                      fa'≡fb' (rrel c a' c≺ᵣa')) .snd))))
+                            (efib b' (f c) (subst (f c ≺ₛ_) fa'≡fb'
+                                             (rrel c a' c≺ᵣa')) .fst .snd))
+                  λ c≺ᵣb' → subst (_≺ᵣ a')
+                            (ind (efib a' (f c) (subst (f c ≺ₛ_)
+                              (sym fa'≡fb') (rrel c b' c≺ᵣb')) .fst .fst)
+                                (efib a' (f c) (subst (f c ≺ₛ_)
+                                  (sym fa'≡fb') (rrel c b' c≺ᵣb')) .fst .snd)
+                                c (efib a' (f c) (subst (f c ≺ₛ_)
+                                  (sym fa'≡fb') (rrel c b' c≺ᵣb')) .snd))
+                              (efib a' (f c) (subst (f c ≺ₛ_)
+                                (sym fa'≡fb') (rrel c b' c≺ᵣb')) .fst .snd)) a b
+    where _≺ᵣ_ = WosetStr._≺_ (str A)
+          _≺ₛ_ = WosetStr._≺_ (str B)
+
+          wosR = WosetStr.isWoset (str A)
+          wosS = WosetStr.isWoset (str B)
+
+          setB = IsWoset.is-set wosS
+
+          wellR = IsWoset.is-well-founded wosR
+          weakR = IsWoset.is-weakly-extensional wosR
+          propR = IsWoset.is-prop-valued wosR
+
+isSimulationUnique : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb')
+                   → ∀ f g → isSimulation A B f → isSimulation A B g
+                   → f ≡ g
+isSimulationUnique A B f g (rreff , fibf) (rrefg , fibg) =
+           (funExt (WFI.induction wellR λ a ind
+                   → isWeaklyExtensional→≺Equiv→≡ _≺ₛ_ weakS (f a) (g a) λ b
+                     → propBiimpl→Equiv (propS b (f a)) (propS b (g a))
+                       (λ b≺ₛfa → subst (_≺ₛ g a)
+                          (sym (sym (fibf a b b≺ₛfa .snd)
+                            ∙ ind (fibf a b b≺ₛfa .fst .fst)
+                                  (fibf a b b≺ₛfa .fst .snd)))
+                          (rrefg (fibf a b b≺ₛfa .fst .fst) a
+                                 (fibf a b b≺ₛfa .fst .snd)))
+                          λ b≺ₛga → subst (_≺ₛ f a)
+                          (ind (fibg a b b≺ₛga .fst .fst)
+                               (fibg a b b≺ₛga .fst .snd)
+                               ∙ fibg a b b≺ₛga .snd)
+                          (rreff (fibg a b b≺ₛga .fst .fst) a
+                                 (fibg a b b≺ₛga .fst .snd))))
+  where _≺ₛ_ = WosetStr._≺_ (str B)
+
+        wosR = WosetStr.isWoset (str A)
+        wosS = WosetStr.isWoset (str B)
+
+        wellR = IsWoset.is-well-founded wosR
+
+        weakS = IsWoset.is-weakly-extensional wosS
+
+        propS = IsWoset.is-prop-valued wosS
+
+isPropIsSimulation : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb')
+                   → ∀ f → isProp (isSimulation A B f)
+isPropIsSimulation A B f sim₀
+  = isProp× (isPropΠ3 λ _ _ _ → propS _ _)
+            (isPropΠ3 (λ _ b _ → isEmbedding→hasPropFibers
+                                 (isEmbedding-∘
+                                 (isSimulation→isEmbedding A B f sim₀)
+                                 λ _ _ → isEmbeddingFstΣProp
+                                         λ _ → propR _ _) b)) sim₀
+  where propR = IsWoset.is-prop-valued (WosetStr.isWoset (str A))
+        propS = IsWoset.is-prop-valued (WosetStr.isWoset (str B))
+
+_≼_ : Rel (Woset ℓa ℓa') (Woset ℓb ℓb') (ℓ-max (ℓ-max (ℓ-max ℓa ℓa') ℓb) ℓb')
+A ≼ B = Σ[ f ∈ (⟨ A ⟩ → ⟨ B ⟩) ] isSimulation A B f
+
+-- Necessary intermediary steps to prove that simulations form a poset
+isRefl≼ : BinaryRelation.isRefl {A = Woset ℓ ℓ'} _≼_
+isRefl≼ A = (idfun ⟨ A ⟩) , ((λ _ _ a≺ᵣa' → a≺ᵣa')
+                          , λ _ b b≺ₛfa → (b , b≺ₛfa) , refl)
+
+isSimulation-∘ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') (C : Woset ℓc ℓc')
+               → ∀ f g
+               → isSimulation A B f
+               → isSimulation B C g
+               → isSimulation A C (g ∘ f)
+isSimulation-∘ A B C f g (rreff , fibf) (rrefg , fibg)
+  = (λ a a' a≺ᵣa' → rrefg (f a) (f a') (rreff a a' a≺ᵣa'))
+  , λ a c c≺ₜgfa → ((fibf a (fibg (f a) c c≺ₜgfa .fst .fst)
+                            (fibg (f a) c c≺ₜgfa .fst .snd) .fst .fst)
+                   , fibf a (fibg (f a) c c≺ₜgfa .fst .fst)
+                            (fibg (f a) c c≺ₜgfa .fst .snd) .fst .snd)
+                   , cong g (fibf a (fibg (f a) c c≺ₜgfa .fst .fst)
+                            (fibg (f a) c c≺ₜgfa .fst .snd) .snd)
+                   ∙ fibg (f a) c c≺ₜgfa .snd
+
+isTrans≼ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') (C : Woset ℓc ℓc')
+         → A ≼ B → B ≼ C → A ≼ C
+isTrans≼ A B C (f , simf) (g , simg)
+  = (g ∘ f) , (isSimulation-∘ A B C f g simf simg)
+
+isPropValued≼ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') → isProp (A ≼ B)
+isPropValued≼ A B (f , simf) (g , simg)
+  = Σ≡Prop (λ _ → isPropIsSimulation A B _)
+           (isSimulationUnique A B f g simf simg)
+
+isAntisym≼Equiv : (A : Woset ℓa ℓa') (B  : Woset ℓb ℓb')
+                → A ≼ B → B ≼ A → WosetEquiv A B
+isAntisym≼Equiv A B (f , simf) (g , simg)
+  = (isoToEquiv is
+  , (makeIsWosetEquiv (isoToEquiv is)
+                      (fst simf)
+                      (fst simg)))
+  where is : Iso ⟨ A ⟩ ⟨ B ⟩
+        Iso.fun is = f
+        Iso.inv is = g
+        Iso.rightInv is b i
+          = cong (_$_ ∘ fst)
+            (isPropValued≼ B B (isTrans≼ B A B (g , simg) (f , simf))
+              (isRefl≼ B)) i b
+        Iso.leftInv is a i
+          = cong (_$_ ∘ fst)
+            (isPropValued≼ A A (isTrans≼ A B A (f , simf) (g , simg))
+              (isRefl≼ A)) i a
+
+isAntisym≼ : BinaryRelation.isAntisym {A = Woset ℓ ℓ'} _≼_
+isAntisym≼ A B A≼B B≼A = equivFun (WosetPath A B) (isAntisym≼Equiv A B A≼B B≼A)
+
+isPoset≼ : IsPoset {A = Woset ℓ ℓ'} _≼_
+isPoset≼ = isposet
+           isSetWoset
+           isPropValued≼
+           isRefl≼
+           isTrans≼
+           isAntisym≼
+
+isWosetEquiv→isSimulation : {A : Woset ℓa ℓa'} {B : Woset ℓb ℓb'}
+                          → ((eq , _) : WosetEquiv A B)
+                          → isSimulation A B (equivFun eq)
+isWosetEquiv→isSimulation {A = A} (A≃B , wqAB)
+                          = ((λ a a' → equivFun (IsWosetEquiv.pres≺ wqAB a a'))
+                          , λ a b b≺fa → ((invEq A≃B b)
+                          , subst (invEq A≃B b ≺ᵣ_) (retEq A≃B a)
+                            (equivFun (IsWosetEquiv.pres≺⁻ wqAB b
+                                      (equivFun A≃B a)) b≺fa))
+                          , secEq A≃B b)
+                          where _≺ᵣ_ = WosetStr._≺_ (str A)
+
+WosetEquiv→≼ : {A : Woset ℓa ℓa'} {B : Woset ℓb ℓb'}
+             → WosetEquiv A B
+             → A ≼ B
+WosetEquiv→≼ (A≃B , wqAB) = (equivFun A≃B) , isWosetEquiv→isSimulation (A≃B , wqAB)
+
+isPropValuedWosetEquiv : {A : Woset ℓa ℓa'} {B : Woset ℓb ℓb'}
+                       → (M : WosetEquiv A B)
+                       → (N : WosetEquiv A B)
+                       → M ≡ N
+isPropValuedWosetEquiv {A = A} {B = B} M N
+  = Σ≡Prop (λ _ → isPropIsWosetEquiv _ _ _)
+    (Σ≡Prop (λ _ → isPropIsEquiv _)
+    (isSimulationUnique A B (M .fst .fst) (N .fst .fst)
+      (isWosetEquiv→isSimulation M)
+      (isWosetEquiv→isSimulation N)))
+
+_↓_ : (A : Woset ℓ ℓ') → (a : ⟨ A ⟩ ) → Woset (ℓ-max ℓ ℓ') ℓ'
+A ↓ a = (Σ[ b ∈ ⟨ A ⟩ ] b ≺ a)
+      , wosetstr _≺ᵢ_ (iswoset
+        setᵢ
+        propᵢ
+        (λ (x , x≺a)
+        → WFI.induction well {P = λ x' → (x'≺a : x' ≺ a)
+                                       → Acc _≺ᵢ_ (x' , x'≺a)}
+            (λ _ ind _ → acc (λ (y , y≺a) y≺x'
+                       → ind y y≺x' y≺a)) x x≺a)
+        (≺×→≡→isWeaklyExtensional _≺ᵢ_ setᵢ propᵢ
+          (λ (x , x≺a) (y , y≺a) f
+           → Σ≡Prop (λ b → prop b a)
+             (isWeaklyExtensional→≺Equiv→≡ _≺_ weak x y
+              λ c → propBiimpl→Equiv (prop c x) (prop c y)
+               (λ c≺x → f (c , trans c x a c≺x x≺a) .fst c≺x)
+                λ c≺y → f (c , trans c y a c≺y y≺a) .snd c≺y)))
+         λ (x , _) (y , _) (z , _) x≺y y≺z → trans x y z x≺y y≺z)
+  where _≺_ = WosetStr._≺_ (str A)
+        wos = WosetStr.isWoset (str A)
+        set = IsWoset.is-set wos
+        prop = IsWoset.is-prop-valued wos
+        well = IsWoset.is-well-founded wos
+        weak = IsWoset.is-weakly-extensional wos
+        trans = IsWoset.is-trans wos
+
+        _≺ᵢ_ = BinaryRelation.InducedRelation _≺_
+               ((Σ[ b ∈ ⟨ A ⟩ ] b ≺ a)
+               , EmbeddingΣProp λ b → prop b a)
+        setᵢ = isSetΣ set (λ b → isProp→isSet (prop b a))
+        propᵢ = λ (x , _) (y , _) → prop x y
+
+isEmbedding↓ : (A : Woset ℓ ℓ') → isEmbedding (A ↓_)
+isEmbedding↓ A = injEmbedding isSetWoset (unique _ _)
+  where _≺_ = WosetStr._≺_ (str A)
+        wos = WosetStr.isWoset (str A)
+        prop = IsWoset.is-prop-valued wos
+        well = IsWoset.is-well-founded wos
+        weak = IsWoset.is-weakly-extensional wos
+        trans = IsWoset.is-trans wos
+
+        unique : ∀ a b → (A ↓ a) ≡ (A ↓ b) → a ≡ b
+        unique a b p = isWeaklyExtensional→≺Equiv→≡ _≺_ weak a b λ c
+          → propBiimpl→Equiv (prop c a) (prop c b)
+            (λ c≺a → subst (_≺ b) (sym (to≡ c c≺a)) (snd (to (c , c≺a))))
+            λ c≺b → subst (_≺ a) (sym (inv≡ c c≺b)) (snd (inv (c , c≺b)))
+          where weq = invEq (WosetPath (A ↓ a) (A ↓ b)) p
+                to = equivFun (fst weq)
+                inv = invEq (fst weq)
+
+                pres≺ = IsWosetEquiv.pres≺ (snd weq)
+                pres≺⁻ = IsWosetEquiv.pres≺⁻ (snd weq)
+
+                to≡ : ∀ c → (c≺a : c ≺ a) → c ≡ fst (to (c , c≺a))
+                to≡ = WFI.induction well λ a' ind a'≺a
+                  → isWeaklyExtensional→≺Equiv→≡ _≺_ weak
+                    a' _ λ c
+                    → propBiimpl→Equiv (prop c a') (prop c _)
+                    (λ c≺a' → subst (_≺ fst (to (a' , a'≺a)))
+                      (sym (ind c c≺a' (trans c a' a c≺a' a'≺a)))
+                      (equivFun (pres≺ (c , trans c a' a c≺a' a'≺a)
+                                        (a' , a'≺a)) c≺a'))
+                     λ c≺toa' → subst (_≺ a') (ind (fst (inv (c , c≺b c≺toa')))
+                       (subst (fst (inv (c , c≺b c≺toa')) ≺_) (invtoa'≡a' a'≺a)
+                       (equivFun (pres≺⁻ (c , c≺b c≺toa') (to (a' , a'≺a))) c≺toa'))
+                       (snd (inv (c , c≺b c≺toa'))) ∙ invc≡toinvc (c≺b c≺toa'))
+                       (subst (fst (inv (c , c≺b c≺toa')) ≺_) (invtoa'≡a' a'≺a)
+                       (equivFun (pres≺⁻ (c , (c≺b c≺toa')) (to (a' , a'≺a))) c≺toa'))
+                  where c≺b : ∀ {c a'}
+                               → {a'≺a : a' ≺ a}
+                               → c ≺ fst (to (a' , a'≺a))
+                               → c ≺ b
+                        c≺b {c} {a'} {a'≺a} c≺toa'
+                          = trans c _ b c≺toa' (snd (to (a' , a'≺a)))
+
+                        invtoa'≡a' : ∀ {a'}
+                                   → (a'≺a : a' ≺ a)
+                                   → fst (inv (to (a' , a'≺a))) ≡ a'
+                        invtoa'≡a' {a'} a'≺a
+                          = fst (PathPΣ (retEq (fst weq) (a' , a'≺a)))
+
+                        invc≡toinvc : ∀ {c}
+                                     → (c≺b : c ≺ b)
+                                     → fst (to (inv (c , c≺b))) ≡ c
+                        invc≡toinvc {c} c≺b
+                          = fst (PathPΣ (secEq (fst weq) (c , c≺b)))
+
+                inv≡ : ∀ c → (c≺b : c ≺ b) → c ≡ fst (inv (c , c≺b))
+                inv≡ = WFI.induction well λ b' ind b'≺b
+                  → isWeaklyExtensional→≺Equiv→≡ _≺_ weak
+                    b' _ λ c
+                    → propBiimpl→Equiv (prop c b') (prop c _)
+                    (λ c≺b' → subst (_≺ fst (inv (b' , b'≺b)))
+                      (sym (ind c c≺b' (trans c b' b c≺b' b'≺b)))
+                      (equivFun (pres≺⁻ (c , trans c b' b c≺b' b'≺b)
+                                         (b' , b'≺b)) c≺b'))
+                     λ c≺invb' → subst (_≺ b') (ind (fst (to (c , c≺a c≺invb')))
+                       (subst (fst (to (c , c≺a c≺invb')) ≺_) (toinvb'≡b' b'≺b)
+                       (equivFun (pres≺ (c , c≺a c≺invb') (inv (b' , b'≺b))) c≺invb'))
+                       (snd (to (c , c≺a c≺invb'))) ∙ toc≡invtoc (c≺a c≺invb'))
+                       (subst (fst (to (c , c≺a c≺invb')) ≺_) (toinvb'≡b' b'≺b)
+                       (equivFun (pres≺ (c , (c≺a c≺invb')) (inv (b' , b'≺b))) c≺invb'))
+                  where c≺a : ∀ {c b'}
+                               → {b'≺b : b' ≺ b}
+                               → c ≺ fst (inv (b' , b'≺b))
+                               → c ≺ a
+                        c≺a {c} {b'} {b'≺b} c≺invb'
+                          = trans c _ a c≺invb' (snd (inv (b' , b'≺b)))
+
+                        toinvb'≡b' : ∀ {b'}
+                                   → (b'≺b : b' ≺ b)
+                                   → fst (to (inv (b' , b'≺b))) ≡ b'
+                        toinvb'≡b' {b'} b'≺b
+                          = fst (PathPΣ (secEq (fst weq) (b' , b'≺b)))
+
+                        toc≡invtoc : ∀ {c}
+                                     → (c≺a : c ≺ a)
+                                     → fst (inv (to (c , c≺a))) ≡ c
+                        toc≡invtoc {c} c≺a
+                          = fst (PathPΣ (retEq (fst weq) (c , c≺a)))
+
+↓Absorb : (A : Woset ℓ ℓ') → ∀ a b
+        → (b≺a : WosetStr._≺_ (str A) b a)
+        → (A ↓ a) ↓ (b , b≺a) ≡ A ↓ b
+↓Absorb A a b b≺a = isAntisym≼ _ _ (f , simf) (g , simg)
+  where _≺_ = WosetStr._≺_ (str A)
+        wos = WosetStr.isWoset (str A)
+        prop = IsWoset.is-prop-valued wos
+        trans = IsWoset.is-trans wos
+
+        f : ⟨ (A ↓ a) ↓ (b , b≺a) ⟩ → ⟨ A ↓ b ⟩
+        f ((c , c≺a) , c≺b) = (c , c≺b)
+
+        simf : isSimulation ((A ↓ a) ↓ (b , b≺a)) (A ↓ b) f
+        simf = (λ _ _ p → p)
+          , λ ((a' , a'≺a) , a'≺b) (b' , b'≺b) b'≺fa
+          → (((b' , trans b' b a b'≺b b≺a) , b'≺b) , b'≺fa) , refl
+
+        g : ⟨ A ↓ b ⟩ → ⟨ (A ↓ a) ↓ (b , b≺a) ⟩
+        g (c , c≺b) = ((c , trans c b a c≺b b≺a) , c≺b)
+
+        simg : isSimulation (A ↓ b) ((A ↓ a) ↓ (b , b≺a)) g
+        simg = (λ _ _ p → p)
+          , λ (a' , a'≺b) ((b' , b'≺a) , b'≺b) b'≺ga
+          → ((b' , b'≺b) , b'≺ga)
+          , Σ≡Prop (λ _ → prop _ _)
+           (Σ≡Prop (λ _ → prop _ _) refl)
+
+↓AbsorbEquiv : (A : Woset ℓ ℓ') → ∀ a b
+             → (b≺a : WosetStr._≺_ (str A) b a)
+             → WosetEquiv ((A ↓ a) ↓ (b , b≺a)) (A ↓ b)
+↓AbsorbEquiv A a b b≺a = subst (λ x → WosetEquiv ((A ↓ a) ↓ (b , b≺a)) x)
+                               (↓Absorb A a b b≺a) reflWosetEquiv
+
+↓Monotone : (A : Woset ℓ ℓ') → ∀ a
+          → (A ↓ a) ≼ A
+↓Monotone A a = f , sim
+  where _≺ᵣ_ = WosetStr._≺_ (str (A ↓ a))
+        _≺ₛ_ = WosetStr._≺_ (str A)
+
+        trans = IsWoset.is-trans (WosetStr.isWoset (str A))
+
+        f : ⟨ A ↓ a ⟩ → ⟨ A ⟩
+        f (a' , _) = a'
+
+        sim : isSimulation (A ↓ a) A f
+        sim = mono , lifting
+          where mono : ∀ a' a'' → a' ≺ᵣ a'' → (f a') ≺ₛ (f a'')
+                mono _ _ a'≺ᵣa'' = a'≺ᵣa''
+
+                lifting : ∀ a' b → b ≺ₛ (f a')
+                        → fiber {A = Σ[ a'' ∈ ⟨ A ↓ a ⟩ ] a'' ≺ᵣ a'} (f ∘ fst) b
+                lifting (a' , a'≺ᵣa) b b≺ₛfa'
+                  = ((b , trans b a' a b≺ₛfa' a'≺ᵣa) , b≺ₛfa') , refl
+
+-- To avoid having this wind up in a higher universe, we define with an equivalence
+_≺_ : Rel (Woset ℓa ℓa') (Woset ℓb ℓb') (ℓ-max (ℓ-max (ℓ-max ℓa ℓa') ℓb) ℓb')
+A ≺ B = Σ[ b ∈ ⟨ B ⟩ ] WosetEquiv (B ↓ b) A
+
+↓Decreasing : (A : Woset ℓ ℓ') → ∀ a
+             → (A ↓ a) ≺ A
+↓Decreasing A a = a , (invEq (WosetPath (A ↓ a) (A ↓ a)) refl)
+
+↓Respects≺ : (A : Woset ℓ ℓ') → ∀ a b
+            → WosetStr._≺_ (str A) a b
+            → (A ↓ a) ≺ (A ↓ b)
+↓Respects≺ A a b a≺b = (a , a≺b) , (invEq (WosetPath _ (A ↓ a)) (↓Absorb A b a a≺b))
+
+↓Respects≺⁻ : (A : Woset ℓ ℓ') → ∀ a b
+              → (A ↓ a) ≺ (A ↓ b)
+              → WosetStr._≺_ (str A) a b
+↓Respects≺⁻ A a b ((c , c≺b) , A↓b↓c≃A↓a)
+  = subst (_≺ᵣ b)
+      (isEmbedding→Inj (isEmbedding↓ A) c a
+       (sym (↓Absorb A b c c≺b) ∙ A↓b↓c≡A↓a))
+      c≺b
+  where _≺ᵣ_ = WosetStr._≺_ (str A)
+        A↓b↓c≡A↓a = equivFun (WosetPath _ (A ↓ a)) A↓b↓c≃A↓a
+
+↓RespectsEquiv : {A : Woset ℓa ℓa'} {B : Woset ℓb ℓb'}
+               → (e : WosetEquiv A B)
+               → ∀ a → WosetEquiv (A ↓ a) (B ↓ equivFun (fst e) a)
+↓RespectsEquiv {A = A} {B = B} e a = eq
+               , makeIsWosetEquiv eq
+                 (λ (x , _) (y , _) x≺y
+                 → equivFun (IsWosetEquiv.pres≺ (snd e) x y) x≺y)
+                 λ (x , _) (y , _) x≺y
+                 → equivFun (IsWosetEquiv.pres≺⁻ (snd e) x y) x≺y
+  where wosA = WosetStr.isWoset (str A)
+        wosB = WosetStr.isWoset (str B)
+
+        propA = IsWoset.is-prop-valued wosA
+        propB = IsWoset.is-prop-valued wosB
+
+        eq : ⟨ A ↓ a ⟩ ≃ ⟨ B ↓ equivFun (fst e) a ⟩
+        eq = Σ-cong-equiv (fst e)
+             λ x → propBiimpl→Equiv (propA _ _) (propB _ _)
+                   (equivFun (IsWosetEquiv.pres≺ (snd e) x a))
+                   (invEq (IsWosetEquiv.pres≺ (snd e) x a))
+
+↓RespectsEquiv⁻ : {A : Woset ℓa ℓa'} {B : Woset ℓb ℓb'}
+                → (e : WosetEquiv A B)
+                → ∀ b → WosetEquiv (A ↓ invEq (fst e) b) (B ↓ b)
+↓RespectsEquiv⁻ {A = A} {B = B} e b = eq
+                , makeIsWosetEquiv eq
+                  (λ (x , _) (y , _) x≺y
+                  → equivFun (IsWosetEquiv.pres≺ (snd e) x y) x≺y)
+                  λ (x , _) (y , _) x≺y
+                  → equivFun (IsWosetEquiv.pres≺⁻ (snd e) x y) x≺y
+  where wosA = WosetStr.isWoset (str A)
+        wosB = WosetStr.isWoset (str B)
+
+        propA = IsWoset.is-prop-valued wosA
+        propB = IsWoset.is-prop-valued wosB
+
+        eq : ⟨ A ↓ invEq (fst e) b ⟩ ≃ ⟨ B ↓ b ⟩
+        eq = invEquiv (Σ-cong-equiv (invEquiv (fst e))
+             λ x → propBiimpl→Equiv (propB _ _) (propA _ _)
+                   (equivFun (IsWosetEquiv.pres≺⁻ (snd e) x b))
+                   (invEq (IsWosetEquiv.pres≺⁻ (snd e) x b)))
+
+≺Absorb↓ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb')
+           → Σ[ b ∈ ⟨ B ⟩ ] A ≺ (B ↓ b)
+           → A ≺ B
+≺Absorb↓ A B (b , (b' , b'≺b) , B↓b↓b'≃A) = b'
+          , subst (λ x → WosetEquiv x A) (↓Absorb B b b' b'≺b) B↓b↓b'≃A
+
+≺Weaken≼ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb')
+           → A ≺ B
+           → A ≼ B
+≺Weaken≼ A B (b , B↓b≃A) = isTrans≼ A (B ↓ b) B
+  (WosetEquiv→≼ (invWosetEquiv B↓b≃A)) (↓Monotone B b)
+
+≺Trans≼ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') (C : Woset ℓc ℓc')
+         → A ≺ B
+         → B ≼ C
+         → A ≺ C
+≺Trans≼ A B C (b , B↓b≃A) (f , (mono , lifting))
+  = (f b) , compWosetEquiv eq B↓b≃A
+    where _≺ᵣ_ = WosetStr._≺_ (str C)
+          _≺ₛ_ = WosetStr._≺_ (str B)
+
+          wosC = WosetStr.isWoset (str C)
+          wosB = WosetStr.isWoset (str B)
+
+          propC = IsWoset.is-prop-valued wosC
+          propB = IsWoset.is-prop-valued wosB
+
+          transB = IsWoset.is-trans wosB
+
+          eq : WosetEquiv (C ↓ f b) (B ↓ b)
+          eq = isAntisym≼Equiv (C ↓ f b) (B ↓ b)
+               (fun , simf)
+               (inv , simg)
+             where fun : ⟨ C ↓ f b ⟩ → ⟨ B ↓ b ⟩
+                   fun (c , c≺fb) = lifting b c c≺fb .fst
+
+                   funIdem : ∀ b' → (ineq : ((f b') ≺ᵣ (f b)))
+                           → fun (f b' , ineq) .fst ≡ b'
+                   funIdem b' fb'≺fb
+                     = isEmbedding→Inj (isSimulation→isEmbedding B C f
+                                       (mono , lifting)) _ b'
+                       (lifting b (f b') fb'≺fb .snd)
+
+                   simf : isSimulation (C ↓ f b) (B ↓ b) fun
+                   simf = m
+                        , λ (c , c≺fb) (b' , b'≺b) b'≺func
+                        → (((f b') , (mono b' b b'≺b))
+                        , (subst (f b' ≺ᵣ_) (lifting b c c≺fb .snd)
+                          (mono b' (fun (c , c≺fb) .fst) b'≺func)))
+                        , Σ≡Prop (λ _ → propB _ _)
+                          (funIdem b' (mono b' b b'≺b))
+                        where m : ∀ c c' → c .fst ≺ᵣ c' .fst
+                                → fun c .fst ≺ₛ fun c' .fst
+                              m (c , c≺fb) (c' , c'≺fb) c≺c'
+                                = subst (_≺ₛ fun (c' , c'≺fb) .fst)
+                                        b'''≡b'
+                                        b'''≺b'
+                                  where b' = fun (c , c≺fb) .fst
+                                        b'' = fun (c' , c'≺fb) .fst
+
+                                        fb'≡c = lifting b c c≺fb .snd
+                                        fb''≡c' = lifting b c' c'≺fb .snd
+
+                                        fb'≺fb'' = subst2 (_≺ᵣ_)
+                                                   (sym fb'≡c)
+                                                   (sym fb''≡c')
+                                                   c≺c'
+
+                                        b''' = lifting b'' (f b')
+                                                       fb'≺fb'' .fst .fst
+
+                                        b'''≺b' = lifting b'' (f b')
+                                                          fb'≺fb'' .fst .snd
+
+                                        fb'''≡fb' = lifting b'' (f b')
+                                                            fb'≺fb'' .snd
+
+                                        b'''≡b' = isEmbedding→Inj
+                                                  (isSimulation→isEmbedding B C
+                                                    f (mono , lifting))
+                                                  b''' b' fb'''≡fb'
+
+                   inv : ⟨ B ↓ b ⟩ → ⟨ C ↓ f b ⟩
+                   inv (b' , b'≺b) = (f b') , (mono b' b b'≺b)
+
+                   simg : isSimulation (B ↓ b) (C ↓ f b) inv
+                   simg = (λ (b' , _) (b'' , _) b'≺b'' → mono b' b'' b'≺b'')
+                           , λ (b' , b'≺b) (c , c≺fb) c≺fb'
+                           → (((lifting b' c c≺fb' .fst .fst)
+                           , transB _ b' b (lifting b' c c≺fb' .fst .snd) b'≺b)
+                           , lifting b' c c≺fb' .fst .snd)
+                           , Σ≡Prop (λ _ → propC _ _) (lifting b' c c≺fb' .snd)
+
+≺RespectsEquivL : {A : Woset ℓa ℓa'} {B : Woset ℓb ℓb'} (C : Woset ℓc ℓc')
+                 → WosetEquiv A B
+                 → A ≺ C
+                 → B ≺ C
+≺RespectsEquivL _ A≃B (c , C↓c≃A) = c , compWosetEquiv C↓c≃A A≃B
+
+≺RespectsEquivR : (A : Woset ℓa ℓa') {B : Woset ℓb ℓb'} {C : Woset ℓc ℓc'}
+                 → WosetEquiv B C
+                 → A ≺ B
+                 → A ≺ C
+≺RespectsEquivR _ B≃C (b , B↓b≃A)
+  = (equivFun (B≃C .fst) b)
+  , (compWosetEquiv (invWosetEquiv (↓RespectsEquiv B≃C b)) B↓b≃A)
+
+≺RespectsEquiv : {A : Woset ℓa ℓa'} {B : Woset ℓb ℓb'}
+                  {C : Woset ℓc ℓc'} {D : Woset ℓd ℓd'}
+                → WosetEquiv A C
+                → WosetEquiv B D
+                → A ≺ B
+                → C ≺ D
+≺RespectsEquiv {B = B} {C = C} A≃C B≃D A≺'B
+  = ≺RespectsEquivR C B≃D (≺RespectsEquivL B A≃C A≺'B)
+
+-- Necessary intermediates to show that _≺_ is well-ordered
+
+isPropValued≺ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb')
+               → isProp (A ≺ B)
+isPropValued≺ A B (b , p) (b' , q)
+  = Σ≡Prop (λ _ → isPropValuedWosetEquiv)
+    (isEmbedding→Inj (isEmbedding↓ B) b b'
+      (equivFun (WosetPath (B ↓ b) (B ↓ b'))
+        (compWosetEquiv p (invWosetEquiv q))))
+
+isWellFounded≺ : WellFounded (_≺_ {ℓa = ℓ} {ℓa' = ℓ})
+isWellFounded≺ A = acc (λ B (a , A↓a≃B)
+                    → subst (Acc _≺_)
+                            (equivFun (WosetPath (A ↓ a) B) A↓a≃B)
+                            (isAcc↓ A a))
+  where isAcc↓ : (A : Woset ℓ ℓ) → ∀ a → Acc _≺_ (A ↓ a)
+        isAcc↓ A = WFI.induction well λ a ind
+                 → acc (λ B ((a' , a'≺a) , A↓a↓a'≃B)
+                 → subst (Acc _≺_)
+                   (sym (↓Absorb A a a' a'≺a)
+                     ∙ equivFun (WosetPath _ B) A↓a↓a'≃B)
+                   (ind a' a'≺a))
+          where _≺ᵣ_ = WosetStr._≺_ (str A)
+                wos = WosetStr.isWoset (str A)
+                well = IsWoset.is-well-founded wos
+
+isTrans≺ : (A : Woset ℓa ℓa') (B : Woset ℓb ℓb') (C : Woset ℓc ℓc')
+          → A ≺ B → B ≺ C → A ≺ C
+isTrans≺ A B C (b , B↓b≃A) (c , C↓c≃B) = ≺Absorb↓ A C (c , (invEq (fst C↓c≃B) b
+                                 , compWosetEquiv (↓RespectsEquiv⁻ C↓c≃B b) B↓b≃A))
+
+isWeaklyExtensional≺ : isWeaklyExtensional (_≺_ {ℓa = ℓ} {ℓa' = ℓ})
+isWeaklyExtensional≺
+  = ≺Equiv→≡→isWeaklyExtensional _≺_ isSetWoset isPropValued≺
+      λ A B ex → path A B ex
+  where path : (A B : Woset ℓ ℓ)
+             → ((C : Woset ℓ ℓ) → (C ≺ A) ≃ (C ≺ B))
+             → A ≡ B
+        path A B ex = equivFun (WosetPath A B)
+                      (eq , (makeIsWosetEquiv eq
+                            (λ a a' a≺a'
+                              → ↓Respects≺⁻ B (equivFun eq a) (equivFun eq a')
+                                (≺RespectsEquiv
+                                  (invWosetEquiv (equivFun (ex (A ↓ a))
+                                                 (↓Decreasing A a) .snd))
+                                  (invWosetEquiv (equivFun (ex (A ↓ a'))
+                                                 (↓Decreasing A a') .snd))
+                                  (↓Respects≺ A a a' a≺a')))
+                            (λ b b' b≺b'
+                              → ↓Respects≺⁻ A (invEq eq b) (invEq eq b')
+                                (≺RespectsEquiv
+                                   (invWosetEquiv (invEq (ex (B ↓ b))
+                                                  (↓Decreasing B b) .snd))
+                                   (invWosetEquiv (invEq (ex (B ↓ b'))
+                                                  (↓Decreasing B b') .snd))
+                                   (↓Respects≺ B b b' b≺b')))))
+          where is : Iso ⟨ A ⟩ ⟨ B ⟩
+                Iso.fun is a = equivFun (ex (A ↓ a)) (↓Decreasing A a) .fst
+                Iso.inv is b = invEq (ex (B ↓ b)) (↓Decreasing B b) .fst
+                Iso.rightInv is p = isEmbedding→Inj (isEmbedding↓ B) q p
+                                    (equivFun (WosetPath (B ↓ q) (B ↓ p))
+                                      (compWosetEquiv
+                                        (equivFun (ex (A ↓ (Iso.inv is p)))
+                                                  (↓Decreasing A (Iso.inv is p)) .snd)
+                                        (invEq (ex (B ↓ p)) (↓Decreasing B p) .snd)))
+                                      where q = Iso.fun is (Iso.inv is p)
+                Iso.leftInv  is p = isEmbedding→Inj (isEmbedding↓ A) q p
+                                    (equivFun (WosetPath (A ↓ q) (A ↓ p))
+                                      (compWosetEquiv
+                                        (invEq (ex (B ↓ (Iso.fun is p)))
+                                               (↓Decreasing B (Iso.fun is p)) .snd)
+                                        (equivFun (ex (A ↓ p)) (↓Decreasing A p) .snd)))
+                                      where q = Iso.inv is (Iso.fun is p)
+
+                eq : ⟨ A ⟩ ≃ ⟨ B ⟩
+                eq = isoToEquiv is
+
+isWoset≺ : IsWoset (_≺_ {ℓa = ℓ} {ℓa' = ℓ})
+isWoset≺ = iswoset
+           isSetWoset
+           isPropValued≺
+           isWellFounded≺
+           isWeaklyExtensional≺
+           isTrans≺
+
+{- With all of the above handled, we now need the notion of suprema.
+   For that, though, we will expand upon the direction taken in
+   lemma 10.3.22 of the HoTT book by Tom de Jong in
+   https://www.cs.bham.ac.uk/~mhe/agda/Ordinals.OrdinalOfOrdinalsSuprema.html
+-}
+
+private
+  module _
+    { I : Type ℓ' }
+    ( F : I → Woset ℓ ℓ)
+    where
+
+    open BinaryRelation
+
+    ΣF : Type (ℓ-max ℓ ℓ')
+    ΣF = Σ[ i ∈ I ] ⟨ F i ⟩
+
+    _≈_ : ΣF → ΣF → Type ℓ
+    (i , x) ≈ (j , y) = WosetEquiv (F i ↓ x) (F j ↓ y)
+
+    _<_ : ΣF → ΣF → Type ℓ
+    (i , x) < (j , y) = (F i ↓ x) ≺ (F j ↓ y)
+
+    isPropValued< : isPropValued _<_
+    isPropValued< (i , x) (j , y) = isPropValued≺ (F i ↓ x) (F j ↓ y)
+
+    isTrans< : isTrans _<_
+    isTrans< (i , x) (j , y) (k , z)
+      = isTrans≺ (F i ↓ x) (F j ↓ y) (F k ↓ z)
+
+    isWellFounded< : WellFounded _<_
+    isWellFounded< (i , x) = WFI.induction isWellFounded≺
+      {P = λ a → ((i , x) : ΣF) → (WosetEquiv a (F i ↓ x)) → Acc _<_ (i , x)}
+      (λ a ind (i' , x') a≃Fi'↓x' → acc (λ (j , y) y'≺x'
+       → ind (F j ↓ y) (≺RespectsEquivR _ (invWosetEquiv a≃Fi'↓x') y'≺x')
+             (j , y) (reflWosetEquiv)))
+      (F i ↓ x) (i , x) (reflWosetEquiv)
+
+    -- We get weak extensionality up to ≈
+    isWeaklyExtensionalUpTo≈< : (α β : ΣF)
+                               → (∀ γ → (γ < α → γ < β) × (γ < β → γ < α))
+                               → α ≈ β
+    isWeaklyExtensionalUpTo≈< (i , x) (j , y) ex
+      = invEq (WosetPath _ _)
+        (isWeaklyExtensional→≺Equiv→≡ _≺_ isWeaklyExtensional≺
+        (F i ↓ x) (F j ↓ y) λ z
+        → propBiimpl→Equiv (isPropValued≺ z (F i ↓ x))
+                           (isPropValued≺ z (F j ↓ y))
+          (λ ((x' , x'≺x) , p) → ≺RespectsEquivL (F j ↓ y)
+            (subst (λ x → WosetEquiv x z) (↓Absorb (F i) x x' x'≺x) p)
+                   (ex (i , x') .fst ((x' , x'≺x)
+            , ↓AbsorbEquiv (F i) x x' x'≺x)))
+          λ ((y' , y'≺y) , q) → ≺RespectsEquivL (F i ↓ x)
+            (subst (λ x → WosetEquiv x z) (↓Absorb (F j) y y' y'≺y) q)
+                   (ex (j , y') .snd ((y' , y'≺y)
+            , ↓AbsorbEquiv (F j) y y' y'≺y)))
+
+  {- Given the above, it seems apparent that this will properly be an ordinal
+     under the set quotient. Before that, we want to show this will be
+     the supremum.
+  -}
+
+    ι : (i : I) → ⟨ F i ⟩ → ΣF
+    ι i x = (i , x)
+
+    ιPreservesOrder : (i : I) (x y : ⟨ F i ⟩)
+                    → WosetStr._≺_ (str (F i)) x y → ι i x < ι i y
+    ιPreservesOrder i x y x≺y = ↓Respects≺ (F i) x y x≺y
+
+    ι≈↓ : (i : I) (x : ⟨ F i ⟩) ((j , y) : ΣF)
+        → (j , y) < ι i x
+        → Σ[ x' ∈ ⟨ F i ⟩ ] WosetStr._≺_ (str (F i)) x' x × ι i x' ≈ (j , y)
+    ι≈↓ i x (j , y) ((x' , x'≺x) , e) = x' , x'≺x
+        , compWosetEquiv (invWosetEquiv (↓AbsorbEquiv (F (fst (ι i x))) x x' x'≺x)) e
+
+    module _
+      (β : Woset ℓ ℓ)
+      (upβ : (i : I) → F i ≼ β)
+      where
+
+      f : (i : I) → ⟨ F i ⟩ → ⟨ β ⟩
+      f i x = upβ i .fst x
+
+      fCommF : (i : I) (x : ⟨ F i ⟩) → F i ↓ x ≡ β ↓ (f i x)
+      fCommF i x = sym (equivFun (WosetPath (β ↓ (f i x)) (F i ↓ x))
+        (≺Trans≼ (F i ↓ x) (F i) β (↓Decreasing (F i) x) (upβ i) .snd))
+
+      f⃕ : ΣF → ⟨ β ⟩
+      f⃕ (i , x) = f i x
+
+      f⃕Respects≈ : {p q : ΣF} → p ≈ q → f⃕ p ≡ f⃕ q
+      f⃕Respects≈ {(i , x)} {(j , y)} e
+        = isEmbedding→Inj (isEmbedding↓ β) (f⃕ (i , x)) (f⃕ (j , y))
+          ((β ↓ f⃕ (i , x)) ≡⟨ sym (fCommF i x) ⟩
+           (F i ↓ x)        ≡⟨ equivFun (WosetPath (F i ↓ x) (F j ↓ y)) e ⟩
+           (F j ↓ y)        ≡⟨ fCommF j y ⟩
+           (β ↓ f⃕ (j , y)) ∎)
+
+      f⃕presβ≺ : (p q : ΣF) → p < q → WosetStr._≺_ (str β) (f⃕ p) (f⃕ q)
+      f⃕presβ≺ (i , x) (j , y) p<q = ↓Respects≺⁻ β (f⃕ (i , x)) (f⃕ (j , y))
+        (subst2 _≺_ (fCommF i x) (fCommF j y) p<q)
+
+      f⃕InitialSegment : (p : ΣF) (b : ⟨ β ⟩)
+                       → WosetStr._≺_ (str β) b (f⃕ p)
+                       → fiber {A = Σ[ q ∈ ΣF ] q < p} (f⃕ ∘ fst) b
+      f⃕InitialSegment (i , x) b b≺fp  = ((i , x') , u) , v
+        where lemma = upβ i .snd .snd
+
+              x' = lemma x b b≺fp .fst .fst
+              x'<x = lemma x b b≺fp .fst .snd
+
+              u = ↓Respects≺ (F i) x' x x'<x
+              v = lemma x b b≺fp .snd
+
+    -- A quick proof that ≈ is an equivalence relation
+    ≋ : isEquivRel _≈_
+    isEquivRel.reflexive ≋ = λ _ → reflWosetEquiv
+    isEquivRel.symmetric ≋ = λ _ _ → invWosetEquiv
+    isEquivRel.transitive ≋ = λ _ _ _ → compWosetEquiv
+
+    -- And now, we forge our quotient type
+
+    F/ : Type (ℓ-max ℓ ℓ')
+    F/ = ΣF / _≈_
+
+    _<'_ : ΣF → ΣF → hProp _
+    x <' y = (x < y , isPropValued< x y)
+
+    <Congruence : { p q p' q' : ΣF} → p ≈ p' → q ≈ q'
+                → p <' q ≡ p' <' q'
+    <Congruence {(i , x)} {(j , y)} {(i' , x')} {(j' , y')} eqp eqq
+      = Σ≡Prop (λ _ → isPropIsProp)
+        (isoToPath (isProp→Iso (isPropValued< _ _) (isPropValued< _ _)
+        (λ x<y → ≺RespectsEquiv eqp eqq x<y)
+        λ y<x → ≺RespectsEquiv (invWosetEquiv eqp) (invWosetEquiv eqq) y<x))
+
+    _</'_ : F/ → F/ → hProp _
+    x </' y = /₂.rec2 isSetHProp _<'_
+              (λ _ _ c a≈b → <Congruence a≈b (isEquivRel.reflexive ≋ c))
+              (λ a _ _ b≈c → <Congruence (isEquivRel.reflexive ≋ a) b≈c) x y
+
+    _</_ : F/ → F/ → Type ℓ
+    x </ y = ⟨ x </' y ⟩
+
+    isPropValued</ : isPropValued _</_
+    isPropValued</ x y = str (x </' y)
+
+    isTrans</ : isTrans _</_
+    isTrans</ = elimProp3 (λ x _ z → isPropΠ2 λ _ _ → isPropValued</ x z) isTrans<
+
+    isWeaklyExtensional</ : isWeaklyExtensional _</_
+    isWeaklyExtensional</ = ≺×→≡→isWeaklyExtensional _</_ squash/ isPropValued</
+      (elimProp2 (λ _ _ → isPropΠ λ _ → squash/ _ _)
+      λ a b z → eq/ a b (isWeaklyExtensionalUpTo≈< a b
+        λ c → z [ c ]))
+
+    isWellFounded</ : WellFounded _</_
+    isWellFounded</ = elimProp (λ _ → isPropAcc _)
+      (WFI.induction isWellFounded< λ a ind
+        → acc (elimProp (λ _ → isPropΠ λ _ → isPropAcc _)
+              λ b b<a → ind b b<a))
+
+    isWoset</ : IsWoset _</_
+    isWoset</ = iswoset squash/
+                        isPropValued</
+                        isWellFounded</
+                        isWeaklyExtensional</
+                        isTrans</
+
+    F/-Ord : Woset (ℓ-max ℓ' ℓ) ℓ
+    F/-Ord = F/ , wosetstr _</_ isWoset</
+
+    -- Now we verify that it's an upper bound
+    F/IsUpperBound : (i : I) → F i ≼ F/-Ord
+    F/IsUpperBound i = [_] ∘ ι i
+      , isSimulation∃→isSimulation (F i) F/-Ord ([_] ∘ ι i)
+       (ιPreservesOrder i
+      , λ x → elimProp (λ _ → isPropΠ λ _ → isPropPropTrunc)
+        λ (j , y) l → ∣ ((ι≈↓ i x (j , y) l .fst)
+                      , (ι≈↓ i x (j , y) l .snd .fst))
+                      , (eq/ (i , l .fst .fst) (j , y)
+                        (ι≈↓ i x (j , y) l .snd .snd)) ∣₁)
+
+    -- And that more specifically, it's the supremum
+    F/IsSupremum : (β : Woset ℓ ℓ)
+                 → ((i : I) → F i ≼ β)
+                 → F/-Ord ≼ β
+    F/IsSupremum β upβ = f/ , sim
+      where wosβ = WosetStr.isWoset (str β)
+            setβ = IsWoset.is-set wosβ
+            propβ = IsWoset.is-prop-valued wosβ
+
+            f/ : ⟨ F/-Ord ⟩ → ⟨ β ⟩
+            f/ = /₂.rec setβ
+                        (f⃕ β upβ)
+                        λ a b → f⃕Respects≈ β upβ {a} {b}
+
+            sim : isSimulation F/-Ord β f/
+            sim = isSimulation∃→isSimulation F/-Ord β f/
+                  ((elimProp2 (λ _ _ → isPropΠ λ _ → propβ _ _)
+                    (f⃕presβ≺ β upβ))
+                , elimProp (λ _ → isPropΠ2 λ _ _ → isPropPropTrunc)
+                  λ a b b≺fa → ∣ ([ f⃕InitialSegment β upβ a b b≺fa .fst .fst ]
+                                 , (f⃕InitialSegment β upβ a b b≺fa .fst .snd))
+                                 , (f⃕InitialSegment β upβ a b b≺fa .snd) ∣₁)
+
+-- With all of that done, we can now define supremum of small ordinal collections
+sup : {I : Type ℓ'} (F : I → Woset ℓ ℓ)
+    → Σ[ β ∈ Woset (ℓ-max ℓ' ℓ) ℓ ]
+         ((i : I) → F i ≼ β)
+       × ((γ : Woset ℓ ℓ) → ((i : I) → F i ≼ γ) → β ≼ γ)
+sup F = (F/-Ord F) , (F/IsUpperBound F) , (F/IsSupremum F)