Well-orderings and Ordinals (#1072)

* Removed redundant and unused Rel definition

Also added the statement that WellFounded is a prop

* Defined well-orderings

* Better converting from HoTT's extensionality

* Moved Woset into its own folder

* Details on simulations and that WFs are irrefl

* Proof that well-ordered sets form a poset

* Constructed well-orderings of an initial segment

* Changed operator for initial segment

* Proved the type of well-orders is well-founded

* Proof that well-orderings are well-ordered

* Removed unused import

* Basic properties of well-ordered sets

* Renamed cardinality to cardinals; defined ordinals

Defined operations on ordinals;
exponentation remains to be defined.

* Renamed properties of simulations

* Changed symbols for ordinal order, started sup

* Substantial overhaul; better level polymorphism

* Fix URL

* Prove properties about ordinal arithmetic

* Fix missed definition name change

* Fix whitespace

* Improved comments as per code review

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

Cubical/Data/Cardinality/Base.agda → 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)

Cubical/Data/Cardinality/Properties.agda → 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 , _)

Cubical/Data/Empty/Base.agda

@@ -20,3 +20,6 @@ rec* ()
 
 elim : {A : ⊥ → Type ℓ} → (x : ⊥) → A x
 elim ()
+
+elim* : {A : ⊥* {ℓ'} → Type ℓ} → (x : ⊥* {ℓ'}) → A x
+elim* ()

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