Prove properties about ordinal arithmetic

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/Base.agda

@@ -29,6 +29,9 @@ private
   variable
     ℓ : Level
 
+infix 7 _·_
+infix 6 _+_
+
 -- Ordinals are simply well-ordered sets
 Ord : ∀ {ℓ} → Type _
 Ord {ℓ} = Woset ℓ ℓ

Cubical/Data/Ordinal/Properties.agda

@@ -9,8 +9,291 @@ This file contains:
 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)

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