From 6e20d9eb978b0482c7343f6faaa5a0ad98a3cde6 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Wed, 1 Feb 2023 21:44:12 +0000 Subject: [PATCH 01/21] Removed redundant and unused Rel definition Also added the statement that WellFounded is a prop --- Cubical/Induction/WellFounded.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 Date: Thu, 2 Feb 2023 08:04:35 +0000 Subject: [PATCH 02/21] Defined well-orderings --- Cubical/Relation/Binary/Extensionality.agda | 20 ++- Cubical/Relation/Binary/Order/Woset.agda | 128 ++++++++++++++++++++ 2 files changed, 145 insertions(+), 3 deletions(-) create mode 100644 Cubical/Relation/Binary/Order/Woset.agda diff --git a/Cubical/Relation/Binary/Extensionality.agda b/Cubical/Relation/Binary/Extensionality.agda index 41b789887f..d8df4d22c8 100644 --- a/Cubical/Relation/Binary/Extensionality.agda +++ b/Cubical/Relation/Binary/Extensionality.agda @@ -6,7 +6,6 @@ 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 module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where @@ -15,7 +14,22 @@ module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where ≡→≺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) + (f a b) .snd diff --git a/Cubical/Relation/Binary/Order/Woset.agda b/Cubical/Relation/Binary/Order/Woset.agda new file mode 100644 index 0000000000..b5bf9820d1 --- /dev/null +++ b/Cubical/Relation/Binary/Order/Woset.agda @@ -0,0 +1,128 @@ +{-# OPTIONS --safe #-} +module Cubical.Relation.Binary.Order.Woset 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 + + +WosetEquiv : (M : Woset ℓ₀ ℓ₀') (M : Woset ℓ₁ ℓ₁') → Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁')) +WosetEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsWosetEquiv (M .snd) e (N .snd) + +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)) + +𝒮ᴰ-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 + +-- 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) From a3509b644e2335e5d34242d82749c2be700117f5 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Fri, 3 Feb 2023 04:04:01 +0000 Subject: [PATCH 03/21] Better converting from HoTT's extensionality --- Cubical/Relation/Binary/Extensionality.agda | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/Cubical/Relation/Binary/Extensionality.agda b/Cubical/Relation/Binary/Extensionality.agda index d8df4d22c8..7293645c44 100644 --- a/Cubical/Relation/Binary/Extensionality.agda +++ b/Cubical/Relation/Binary/Extensionality.agda @@ -8,6 +8,8 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Transport 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) @@ -25,11 +27,18 @@ module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where -} ≺Equiv→≡→IsWeaklyExtensional : isSet A → BinaryRelation.isPropValued _≺_ - → ((x y : A) → (∀ z → (z ≺ x) ≃ (z ≺ y)) → x ≡ y) + → ((x y : A) → (∀ z → ((z ≺ x) → (z ≺ y)) + × ((z ≺ y) → (z ≺ x))) → 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))) + (isPropΠ (λ z → isOfHLevel≃ 1 + (prop z a) + (prop z b))) (≡→≺Equiv a b) - (f a b) .snd + (λ g → f a b λ z → (g z .fst) , invEquiv (g z) .fst) .snd + + isWeaklyExtensional→≺Equiv→≡ : isWeaklyExtensional + → (x y : A) → (∀ z → (z ≺ x) ≃ (z ≺ y)) → x ≡ y + isWeaklyExtensional→≺Equiv→≡ weak x y + = invIsEq (weak x y) From 80b8b72cb46a018282f6c81d17be1ef955130181 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Fri, 3 Feb 2023 18:02:52 +0000 Subject: [PATCH 04/21] Moved Woset into its own folder --- Cubical/Relation/Binary/Order/{Woset.agda => Woset/Base.agda} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename Cubical/Relation/Binary/Order/{Woset.agda => Woset/Base.agda} (98%) diff --git a/Cubical/Relation/Binary/Order/Woset.agda b/Cubical/Relation/Binary/Order/Woset/Base.agda similarity index 98% rename from Cubical/Relation/Binary/Order/Woset.agda rename to Cubical/Relation/Binary/Order/Woset/Base.agda index b5bf9820d1..ae94325c10 100644 --- a/Cubical/Relation/Binary/Order/Woset.agda +++ b/Cubical/Relation/Binary/Order/Woset/Base.agda @@ -1,5 +1,5 @@ {-# OPTIONS --safe #-} -module Cubical.Relation.Binary.Order.Woset where +module Cubical.Relation.Binary.Order.Woset.Base where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv From 9a2d09209d5af794ce0f17055e9ecf935017e1f7 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sat, 4 Feb 2023 05:58:58 +0000 Subject: [PATCH 05/21] Details on simulations and that WFs are irrefl --- Cubical/Relation/Binary/Base.agda | 5 ++ .../Binary/Order/Woset/Simulation.agda | 87 +++++++++++++++++++ 2 files changed, 92 insertions(+) create mode 100644 Cubical/Relation/Binary/Order/Woset/Simulation.agda diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda index 68bb8f5d55..c548eb35d4 100644 --- a/Cubical/Relation/Binary/Base.agda +++ b/Cubical/Relation/Binary/Base.agda @@ -19,6 +19,8 @@ open import Cubical.HITs.PropositionalTruncation as ∥₁ open import Cubical.Relation.Nullary.Base +open import Cubical.Induction.WellFounded + private variable ℓA ℓ≅A ℓA' ℓ≅A' : Level @@ -89,6 +91,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/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda new file mode 100644 index 0000000000..b473aea409 --- /dev/null +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --safe #-} +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.Structure + +open import Cubical.Induction.WellFounded + +open import Cubical.Functions.Embedding + +open import Cubical.Data.Sigma + +open import Cubical.HITs.PropositionalTruncation + +open import Cubical.Relation.Binary.Order.Woset.Base +open import Cubical.Relation.Binary.Base +open import Cubical.Relation.Binary.Extensionality + +private + variable + ℓ ℓ' : Level + +isSimulation : (A B : Woset ℓ ℓ') (f : ⟨ A ⟩ → ⟨ B ⟩) → Type (ℓ-max ℓ ℓ') +isSimulation A B f = respectsRel × existsFib + where _≺ᵣ_ = WosetStr._≺_ (str A) + _≺ₛ_ = WosetStr._≺_ (str B) + + respectsRel = ∀ a a' → a ≺ᵣ a' → (f a) ≺ₛ (f a') + + less : ∀ a → Type _ + less a = Σ[ a' ∈ ⟨ A ⟩ ] a' ≺ᵣ a + + existsFib = ∀ a → ∀ b → b ≺ₛ (f a) → fiber {A = less a} (f ∘ fst) b + +isSimulation→isEmbedding : (A B : Woset ℓ ℓ') → ∀ 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' inda b' fa'≡fb' → isWeaklyExtensional→≺Equiv→≡ + _≺ᵣ_ weakR a' b' λ c → propBiimpl→Equiv + (propR c a') (propR c b') + (λ c≺ᵣa' → subst (_≺ᵣ b') + (sym (inda 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') + (inda (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) + + IsWosetR = WosetStr.isWoset (str A) + IsWosetS = WosetStr.isWoset (str B) + + setB = IsWoset.is-set IsWosetS + + wellR = IsWoset.is-well-founded IsWosetR + + weakR = IsWoset.is-weakly-extensional IsWosetR + + propR = IsWoset.is-prop-valued IsWosetR + +isPropIsSimulation : (A B : Woset ℓ ℓ') → ∀ 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₀) + λ w x → isEmbeddingFstΣProp + λ _ → propR _ _) b)) sim₀ + where propR = IsWoset.is-prop-valued (WosetStr.isWoset (str A)) + propS = IsWoset.is-prop-valued (WosetStr.isWoset (str B)) From 9d451cdac496cd671d9c09633616391a6cfb9b69 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sun, 5 Feb 2023 06:31:58 +0000 Subject: [PATCH 06/21] Proof that well-ordered sets form a poset --- Cubical/Relation/Binary/Order/Woset/Base.agda | 65 +++++++++++ .../Binary/Order/Woset/Simulation.agda | 102 +++++++++++++++++- 2 files changed, 165 insertions(+), 2 deletions(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Base.agda b/Cubical/Relation/Binary/Order/Woset/Base.agda index ae94325c10..e88368b0db 100644 --- a/Cubical/Relation/Binary/Order/Woset/Base.agda +++ b/Cubical/Relation/Binary/Order/Woset/Base.agda @@ -81,6 +81,12 @@ record IsWosetEquiv {A : Type ℓ₀} {B : Type ℓ₁} 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) @@ -94,6 +100,17 @@ isPropIsWoset _≺_ = isOfHLevelRetractFromIso 1 IsWosetIsoΣ (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 @@ -108,6 +125,54 @@ isPropIsWoset _≺_ = isOfHLevelRetractFromIso 1 IsWosetIsoΣ 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 diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index b473aea409..81b0b90d2c 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -5,6 +5,7 @@ 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.Induction.WellFounded @@ -13,9 +14,10 @@ open import Cubical.Functions.Embedding open import Cubical.Data.Sigma -open import Cubical.HITs.PropositionalTruncation +open import Cubical.HITs.PropositionalTruncation as ∥₁ open import Cubical.Relation.Binary.Order.Woset.Base +open import Cubical.Relation.Binary.Order.Poset.Base open import Cubical.Relation.Binary.Base open import Cubical.Relation.Binary.Extensionality @@ -33,7 +35,7 @@ isSimulation A B f = respectsRel × existsFib less : ∀ a → Type _ less a = Σ[ a' ∈ ⟨ A ⟩ ] a' ≺ᵣ a - existsFib = ∀ a → ∀ b → b ≺ₛ (f a) → fiber {A = less a} (f ∘ fst) b + existsFib = ∀ a b → b ≺ₛ (f a) → fiber {A = less a} (f ∘ fst) b isSimulation→isEmbedding : (A B : Woset ℓ ℓ') → ∀ f → isSimulation A B f → isEmbedding f @@ -85,3 +87,99 @@ isPropIsSimulation A B f sim₀ λ _ → propR _ _) b)) sim₀ where propR = IsWoset.is-prop-valued (WosetStr.isWoset (str A)) propS = IsWoset.is-prop-valued (WosetStr.isWoset (str B)) + +_≤_ : Rel (Woset ℓ ℓ') (Woset ℓ ℓ') (ℓ-max ℓ ℓ') +A ≤ B = Σ[ f ∈ (⟨ A ⟩ → ⟨ B ⟩) ] isSimulation A B f + +-- Necessary intermediary steps to prove that simulations form a poset +private + isRefl≤ : BinaryRelation.isRefl {A = Woset ℓ ℓ'} _≤_ + isRefl≤ A = (idfun ⟨ A ⟩) , ((λ _ _ a≺ᵣa' → a≺ᵣa') + , λ a b b≺ₛfa → (b , b≺ₛfa) , refl) + + isSimulation-∘ : (A B C : Woset ℓ ℓ') → ∀ 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≤ : BinaryRelation.isTrans {A = Woset ℓ ℓ'} _≤_ + isTrans≤ A B C (f , simf) (g , simg) + = (g ∘ f) , (isSimulation-∘ A B C f g simf simg) + + isSimulationRespectsId : (A : Type ℓ) (_<_ _≺_ : Rel A A ℓ') + → (wosR : IsWoset _<_) (wosS : IsWoset _≺_) + → isSimulation (woset A _<_ wosR) + (woset A _≺_ wosS) (idfun A) + → isSimulation (woset A _≺_ wosS) + (woset A _<_ wosR) (idfun A) + → _<_ ≡ _≺_ + isSimulationRespectsId A _<_ _≺_ wosR wosS (rrefl< , _) (rrefl≺ , _) + = funExt λ a → funExt λ b + → isoToPath (isProp→Iso (IsWoset.is-prop-valued wosR a b) + (IsWoset.is-prop-valued wosS a b) + (λ a Date: Sun, 5 Feb 2023 20:06:27 +0000 Subject: [PATCH 07/21] Constructed well-orderings of an initial segment --- Cubical/Relation/Binary/Extensionality.agda | 4 +- .../Binary/Order/Woset/Simulation.agda | 38 +++++++++++++++++++ 2 files changed, 40 insertions(+), 2 deletions(-) diff --git a/Cubical/Relation/Binary/Extensionality.agda b/Cubical/Relation/Binary/Extensionality.agda index 7293645c44..db1b24cb4f 100644 --- a/Cubical/Relation/Binary/Extensionality.agda +++ b/Cubical/Relation/Binary/Extensionality.agda @@ -26,11 +26,11 @@ module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where definition. -} - ≺Equiv→≡→IsWeaklyExtensional : isSet A → BinaryRelation.isPropValued _≺_ + ≺Equiv→≡→isWeaklyExtensional : isSet A → BinaryRelation.isPropValued _≺_ → ((x y : A) → (∀ z → ((z ≺ x) → (z ≺ y)) × ((z ≺ y) → (z ≺ x))) → x ≡ y) → isWeaklyExtensional - ≺Equiv→≡→IsWeaklyExtensional setA prop f a b + ≺Equiv→≡→isWeaklyExtensional setA prop f a b = propBiimpl→Equiv (setA a b) (isPropΠ (λ z → isOfHLevel≃ 1 (prop z a) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index 81b0b90d2c..9df66f5b90 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -183,3 +183,41 @@ isPoset≤ = isposet isRefl≤ isTrans≤ isAntisym≤ + +_/_ : (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) + (≺Equiv→≡→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 + +isBounded : (A B : Woset ℓ ℓ') → A ≤ B → Type (ℓ-max ℓ ℓ') +isBounded A B _ = Σ[ b ∈ ⟨ B ⟩ ] WosetEquiv A (B / b) + +_<_ : Rel (Woset ℓ ℓ') (Woset ℓ ℓ') (ℓ-max ℓ ℓ') +A < B = Σ[ f ∈ A ≤ B ] isBounded A B f From af6518baac6f192f40a8ef5f37b6abfb61a7feb2 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sun, 5 Feb 2023 23:48:25 +0000 Subject: [PATCH 08/21] Changed operator for initial segment --- Cubical/Relation/Binary/Order/Woset/Simulation.agda | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index 9df66f5b90..6ac8decaca 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -184,8 +184,8 @@ isPoset≤ = isposet isTrans≤ isAntisym≤ -_/_ : (A : Woset ℓ ℓ') → (a : ⟨ A ⟩ ) → Woset (ℓ-max ℓ ℓ') ℓ' -A / a = (Σ[ b ∈ ⟨ A ⟩ ] b ≺ a) +_↓_ : (A : Woset ℓ ℓ') → (a : ⟨ A ⟩ ) → Woset (ℓ-max ℓ ℓ') ℓ' +A ↓ a = (Σ[ b ∈ ⟨ A ⟩ ] b ≺ a) , wosetstr _≺ᵢ_ (iswoset setᵢ propᵢ @@ -215,9 +215,3 @@ A / a = (Σ[ 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 - -isBounded : (A B : Woset ℓ ℓ') → A ≤ B → Type (ℓ-max ℓ ℓ') -isBounded A B _ = Σ[ b ∈ ⟨ B ⟩ ] WosetEquiv A (B / b) - -_<_ : Rel (Woset ℓ ℓ') (Woset ℓ ℓ') (ℓ-max ℓ ℓ') -A < B = Σ[ f ∈ A ≤ B ] isBounded A B f From 105a345e0772166aa45286f7f92b8dc649fc6524 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Wed, 8 Feb 2023 04:39:46 +0000 Subject: [PATCH 09/21] Proved the type of well-orders is well-founded --- .../Binary/Order/Woset/Simulation.agda | 157 ++++++++++++++++-- 1 file changed, 142 insertions(+), 15 deletions(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index 6ac8decaca..e9404538ff 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -95,7 +95,7 @@ A ≤ B = Σ[ f ∈ (⟨ A ⟩ → ⟨ B ⟩) ] isSimulation A B f private isRefl≤ : BinaryRelation.isRefl {A = Woset ℓ ℓ'} _≤_ isRefl≤ A = (idfun ⟨ A ⟩) , ((λ _ _ a≺ᵣa' → a≺ᵣa') - , λ a b b≺ₛfa → (b , b≺ₛfa) , refl) + , λ _ b b≺ₛfa → (b , b≺ₛfa) , refl) isSimulation-∘ : (A B C : Woset ℓ ℓ') → ∀ f g → isSimulation A B f @@ -115,20 +115,6 @@ private isTrans≤ A B C (f , simf) (g , simg) = (g ∘ f) , (isSimulation-∘ A B C f g simf simg) - isSimulationRespectsId : (A : Type ℓ) (_<_ _≺_ : Rel A A ℓ') - → (wosR : IsWoset _<_) (wosS : IsWoset _≺_) - → isSimulation (woset A _<_ wosR) - (woset A _≺_ wosS) (idfun A) - → isSimulation (woset A _≺_ wosS) - (woset A _<_ wosR) (idfun A) - → _<_ ≡ _≺_ - isSimulationRespectsId A _<_ _≺_ wosR wosS (rrefl< , _) (rrefl≺ , _) - = funExt λ a → funExt λ b - → isoToPath (isProp→Iso (IsWoset.is-prop-valued wosR a b) - (IsWoset.is-prop-valued wosS a b) - (λ a Date: Thu, 9 Feb 2023 18:32:15 +0000 Subject: [PATCH 10/21] Proof that well-orderings are well-ordered --- Cubical/Relation/Binary/Extensionality.agda | 17 ++++- .../Binary/Order/Woset/Simulation.agda | 76 +++++++++++++++++-- 2 files changed, 84 insertions(+), 9 deletions(-) diff --git a/Cubical/Relation/Binary/Extensionality.agda b/Cubical/Relation/Binary/Extensionality.agda index db1b24cb4f..f67edd57bb 100644 --- a/Cubical/Relation/Binary/Extensionality.agda +++ b/Cubical/Relation/Binary/Extensionality.agda @@ -27,8 +27,7 @@ module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where -} ≺Equiv→≡→isWeaklyExtensional : isSet A → BinaryRelation.isPropValued _≺_ - → ((x y : A) → (∀ z → ((z ≺ x) → (z ≺ y)) - × ((z ≺ y) → (z ≺ x))) → x ≡ y) + → ((x y : A) → (∀ z → ((z ≺ x) ≃ (z ≺ y))) → x ≡ y) → isWeaklyExtensional ≺Equiv→≡→isWeaklyExtensional setA prop f a b = propBiimpl→Equiv (setA a b) @@ -36,7 +35,19 @@ module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where (prop z a) (prop z b))) (≡→≺Equiv a b) - (λ g → f a b λ z → (g z .fst) , invEquiv (g z) .fst) .snd + (λ 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 diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index e9404538ff..8a0248d8d1 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -180,7 +180,7 @@ A ↓ a = (Σ[ b ∈ ⟨ A ⟩ ] b ≺ a) → Acc _≺ᵢ_ (x' , x'≺a)} (λ _ ind _ → acc (λ (y , y≺a) y≺x' → ind y y≺x' y≺a)) x x≺a) - (≺Equiv→≡→isWeaklyExtensional _≺ᵢ_ setᵢ propᵢ + (≺×→≡→isWeaklyExtensional _≺ᵢ_ setᵢ propᵢ (λ (x , x≺a) (y , y≺a) f → Σ≡Prop (λ b → prop b a) (isWeaklyExtensional→≺Equiv→≡ _≺_ weak x y @@ -202,8 +202,8 @@ A ↓ a = (Σ[ b ∈ ⟨ A ⟩ ] b ≺ a) setᵢ = isSetΣ set (λ b → isProp→isSet (prop b a)) propᵢ = λ (x , _) (y , _) → prop x y -isEmbedding↓ : {A : Woset ℓ ℓ'} → isEmbedding (A ↓_) -isEmbedding↓ {A = A} = injEmbedding isSetWoset (unique _ _) +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 @@ -318,7 +318,6 @@ isEmbedding↓ {A = A} = injEmbedding isSetWoset (unique _ _) , Σ≡Prop (λ _ → prop _ _) (Σ≡Prop (λ _ → prop _ _) refl) - _<_ : Rel (Woset ℓ ℓ) (Woset ℓ ℓ) (ℓ-suc ℓ) A < B = fiber (B ↓_) A @@ -326,10 +325,29 @@ A < B = fiber (B ↓_) A → (A ↓ a) < A ↓Decreasing A a = a , refl --- Necessary intermediate to show the above is well-ordered +↓Respects< : (A : Woset ℓ ℓ) → ∀ a b + → WosetStr._≺_ (str A) a b + → (A ↓ a) < (A ↓ b) +↓Respects< A a b a≺b = (a , a≺b) , (↓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) + + Date: Thu, 9 Feb 2023 18:40:24 +0000 Subject: [PATCH 11/21] Removed unused import --- Cubical/Relation/Binary/Order/Woset/Simulation.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index 8a0248d8d1..fb0aa3c2a9 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -14,8 +14,6 @@ open import Cubical.Functions.Embedding open import Cubical.Data.Sigma -open import Cubical.HITs.PropositionalTruncation as ∥₁ - open import Cubical.Relation.Binary.Order.Woset.Base open import Cubical.Relation.Binary.Order.Poset.Base open import Cubical.Relation.Binary.Base @@ -365,7 +363,8 @@ private isTrans< A _ C A Date: Thu, 9 Feb 2023 19:43:47 +0000 Subject: [PATCH 12/21] Basic properties of well-ordered sets --- Cubical/Relation/Binary/Base.agda | 4 +- Cubical/Relation/Binary/Order/Woset.agda | 5 +++ .../Binary/Order/Woset/Properties.agda | 37 +++++++++++++++++++ 3 files changed, 44 insertions(+), 2 deletions(-) create mode 100644 Cubical/Relation/Binary/Order/Woset.agda create mode 100644 Cubical/Relation/Binary/Order/Woset/Properties.agda diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda index c548eb35d4..6e7e963539 100644 --- a/Cubical/Relation/Binary/Base.agda +++ b/Cubical/Relation/Binary/Base.agda @@ -91,8 +91,8 @@ 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 + 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/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/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)) From 8bac43d09f1da66ebbe02f4418565187067fd0e1 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Fri, 10 Feb 2023 07:08:41 +0000 Subject: [PATCH 13/21] Renamed cardinality to cardinals; defined ordinals Defined operations on ordinals; exponentation remains to be defined. --- Cubical/Data/Cardinal.agda | 5 + .../Data/{Cardinality => Cardinal}/Base.agda | 2 +- .../{Cardinality => Cardinal}/Properties.agda | 4 +- Cubical/Data/Cardinality.agda | 5 - Cubical/Data/Ordinal.agda | 5 + Cubical/Data/Ordinal/Base.agda | 254 ++++++++++++++++++ Cubical/Data/Ordinal/Properties.agda | 16 ++ 7 files changed, 283 insertions(+), 8 deletions(-) create mode 100644 Cubical/Data/Cardinal.agda rename Cubical/Data/{Cardinality => Cardinal}/Base.agda (97%) rename Cubical/Data/{Cardinality => Cardinal}/Properties.agda (99%) delete mode 100644 Cubical/Data/Cardinality.agda create mode 100644 Cubical/Data/Ordinal.agda create mode 100644 Cubical/Data/Ordinal/Base.agda create mode 100644 Cubical/Data/Ordinal/Properties.agda 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 97% rename from Cubical/Data/Cardinality/Base.agda rename to Cubical/Data/Cardinal/Base.agda index 56f161145f..b70750d21b 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 diff --git a/Cubical/Data/Cardinality/Properties.agda b/Cubical/Data/Cardinal/Properties.agda similarity index 99% rename from Cubical/Data/Cardinality/Properties.agda rename to Cubical/Data/Cardinal/Properties.agda index 77a6dba379..a84951b561 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 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/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..22d66253d5 --- /dev/null +++ b/Cubical/Data/Ordinal/Base.agda @@ -0,0 +1,254 @@ +{- + +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 + +-- 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..324199df52 --- /dev/null +++ b/Cubical/Data/Ordinal/Properties.agda @@ -0,0 +1,16 @@ +{- + +This file contains: + +- Properties of ordinals + +-} +{-# OPTIONS --safe #-} +module Cubical.Data.Ordinal.Properties where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Ordinal.Base + +private + variable + ℓ : Level From ca0d53cbb3206d0e98038521c1a863beb0cd8b39 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sat, 11 Feb 2023 20:41:02 +0000 Subject: [PATCH 14/21] Renamed properties of simulations --- Cubical/Relation/Binary/Order/Woset/Simulation.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index fb0aa3c2a9..2ec7ef00bf 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -24,16 +24,16 @@ private ℓ ℓ' : Level isSimulation : (A B : Woset ℓ ℓ') (f : ⟨ A ⟩ → ⟨ B ⟩) → Type (ℓ-max ℓ ℓ') -isSimulation A B f = respectsRel × existsFib +isSimulation A B f = monotone × lifting where _≺ᵣ_ = WosetStr._≺_ (str A) _≺ₛ_ = WosetStr._≺_ (str B) - respectsRel = ∀ a a' → a ≺ᵣ a' → (f a) ≺ₛ (f a') + monotone = ∀ a a' → a ≺ᵣ a' → (f a) ≺ₛ (f a') less : ∀ a → Type _ less a = Σ[ a' ∈ ⟨ A ⟩ ] a' ≺ᵣ a - existsFib = ∀ a b → b ≺ₛ (f a) → fiber {A = less a} (f ∘ fst) b + lifting = ∀ a b → b ≺ₛ (f a) → fiber {A = less a} (f ∘ fst) b isSimulation→isEmbedding : (A B : Woset ℓ ℓ') → ∀ f → isSimulation A B f → isEmbedding f From 27569f8da2b689d5cf9f461c97b7ad4db04cd205 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Mon, 13 Feb 2023 05:24:40 +0000 Subject: [PATCH 15/21] Changed symbols for ordinal order, started sup --- .../Binary/Order/Woset/Simulation.agda | 194 ++++++++++++------ 1 file changed, 132 insertions(+), 62 deletions(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index 2ec7ef00bf..a02411abe8 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -8,6 +8,8 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Structure +open import Cubical.HITs.SetQuotients + open import Cubical.Induction.WellFounded open import Cubical.Functions.Embedding @@ -86,13 +88,13 @@ isPropIsSimulation A B f sim₀ where propR = IsWoset.is-prop-valued (WosetStr.isWoset (str A)) propS = IsWoset.is-prop-valued (WosetStr.isWoset (str B)) -_≤_ : Rel (Woset ℓ ℓ') (Woset ℓ ℓ') (ℓ-max ℓ ℓ') -A ≤ B = Σ[ f ∈ (⟨ A ⟩ → ⟨ B ⟩) ] isSimulation A B f +_≼_ : Rel (Woset ℓ ℓ') (Woset ℓ ℓ') (ℓ-max ℓ ℓ') +A ≼ B = Σ[ f ∈ (⟨ A ⟩ → ⟨ B ⟩) ] isSimulation A B f -- Necessary intermediary steps to prove that simulations form a poset private - isRefl≤ : BinaryRelation.isRefl {A = Woset ℓ ℓ'} _≤_ - isRefl≤ A = (idfun ⟨ A ⟩) , ((λ _ _ a≺ᵣa' → a≺ᵣa') + isRefl≼ : BinaryRelation.isRefl {A = Woset ℓ ℓ'} _≼_ + isRefl≼ A = (idfun ⟨ A ⟩) , ((λ _ _ a≺ᵣa' → a≺ᵣa') , λ _ b b≺ₛfa → (b , b≺ₛfa) , refl) isSimulation-∘ : (A B C : Woset ℓ ℓ') → ∀ f g @@ -109,12 +111,12 @@ private (fibg (f a) c c≺ₜgfa .fst .snd) .snd) ∙ fibg (f a) c c≺ₜgfa .snd - isTrans≤ : BinaryRelation.isTrans {A = Woset ℓ ℓ'} _≤_ - isTrans≤ A B C (f , simf) (g , simg) + isTrans≼ : BinaryRelation.isTrans {A = Woset ℓ ℓ'} _≼_ + isTrans≼ A B C (f , simf) (g , simg) = (g ∘ f) , (isSimulation-∘ A B C f g simf simg) - isPropValued≤ : BinaryRelation.isPropValued {A = Woset ℓ ℓ'} _≤_ - isPropValued≤ A B (f , (rreff , fibf)) (g , (rrefg , fibg)) + isPropValued≼ : BinaryRelation.isPropValued {A = Woset ℓ ℓ'} _≼_ + isPropValued≼ A B (f , (rreff , fibf)) (g , (rrefg , fibg)) = Σ≡Prop (λ _ → isPropIsSimulation A B _) (funExt (WFI.induction wellR λ a ind → isWeaklyExtensional→≺Equiv→≡ _≺ₛ_ weakS (f a) (g a) λ b @@ -143,8 +145,8 @@ private propS = IsWoset.is-prop-valued wosS - isAntisym≤ : BinaryRelation.isAntisym {A = Woset ℓ ℓ'} _≤_ - isAntisym≤ A B (f , simf) (g , simg) = WosetPath A B .fst (isoToEquiv is + isAntisym≼ : BinaryRelation.isAntisym {A = Woset ℓ ℓ'} _≼_ + isAntisym≼ A B (f , simf) (g , simg) = WosetPath A B .fst (isoToEquiv is , (makeIsWosetEquiv (isoToEquiv is) (fst simf) (fst simg))) @@ -153,20 +155,20 @@ private 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 + (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 + (isPropValued≼ A A (isTrans≼ A B A (f , simf) (g , simg)) + (isRefl≼ A)) i a -isPoset≤ : IsPoset {A = Woset ℓ ℓ'} _≤_ -isPoset≤ = isposet +isPoset≼ : IsPoset {A = Woset ℓ ℓ'} _≼_ +isPoset≼ = isposet isSetWoset - isPropValued≤ - isRefl≤ - isTrans≤ - isAntisym≤ + isPropValued≼ + isRefl≼ + isTrans≼ + isAntisym≼ _↓_ : (A : Woset ℓ ℓ') → (a : ⟨ A ⟩ ) → Woset (ℓ-max ℓ ℓ') ℓ' A ↓ a = (Σ[ b ∈ ⟨ A ⟩ ] b ≺ a) @@ -292,7 +294,7 @@ isEmbedding↓ A = injEmbedding isSetWoset (unique _ _) ↓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) +↓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 @@ -316,74 +318,81 @@ isEmbedding↓ A = injEmbedding isSetWoset (unique _ _) , Σ≡Prop (λ _ → prop _ _) (Σ≡Prop (λ _ → prop _ _) refl) -_<_ : Rel (Woset ℓ ℓ) (Woset ℓ ℓ) (ℓ-suc ℓ) -A < B = fiber (B ↓_) A +_≺_ : Rel (Woset ℓ ℓ) (Woset ℓ ℓ) (ℓ-suc ℓ) +A ≺ B = fiber (B ↓_) A + +-- To avoid having this wind up in a higher universe, we define the same with equivalences +_≺'_ : Rel (Woset ℓ ℓ) (Woset ℓ ℓ) ℓ +A ≺' B = Σ[ b ∈ ⟨ B ⟩ ] WosetEquiv (B ↓ b) A + +≺≃≺' : (A B : Woset ℓ ℓ) → A ≺ B ≃ A ≺' B +≺≃≺' A B = invEquiv (Σ-cong-equiv (idEquiv ⟨ B ⟩) λ b → WosetPath (B ↓ b) A) ↓Decreasing : (A : Woset ℓ ℓ) → ∀ a - → (A ↓ a) < A + → (A ↓ a) ≺ A ↓Decreasing A a = a , refl -↓Respects< : (A : Woset ℓ ℓ) → ∀ a b +↓Respects≺ : (A : Woset ℓ ℓ) → ∀ a b → WosetStr._≺_ (str A) a b - → (A ↓ a) < (A ↓ b) -↓Respects< A a b a≺b = (a , a≺b) , (↓Absorb A b a a≺b) + → (A ↓ a) ≺ (A ↓ b) +↓Respects≺ A a b a≺b = (a , a≺b) , (↓Absorb A b a a≺b) -↓Respects<⁻ : (A : Woset ℓ ℓ) → ∀ a b - → (A ↓ 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 +↓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) + where _≺ᵣ_ = WosetStr._≺_ (str A) - Date: Thu, 16 Feb 2023 21:00:11 +0000 Subject: [PATCH 16/21] Substantial overhaul; better level polymorphism --- Cubical/Data/Cardinal/Base.agda | 8 +- Cubical/Data/Cardinal/Properties.agda | 91 +- Cubical/HITs/SetTruncation/Properties.agda | 34 +- Cubical/Relation/Binary/Base.agda | 2 +- Cubical/Relation/Binary/Order/Woset/Base.agda | 15 +- .../Binary/Order/Woset/Simulation.agda | 829 ++++++++++++++---- 6 files changed, 725 insertions(+), 254 deletions(-) diff --git a/Cubical/Data/Cardinal/Base.agda b/Cubical/Data/Cardinal/Base.agda index b70750d21b..72b8ebd6db 100644 --- a/Cubical/Data/Cardinal/Base.agda +++ b/Cubical/Data/Cardinal/Base.agda @@ -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/Cardinal/Properties.agda b/Cubical/Data/Cardinal/Properties.agda index a84951b561..3bb30f186a 100644 --- a/Cubical/Data/Cardinal/Properties.agda +++ b/Cubical/Data/Cardinal/Properties.agda @@ -30,52 +30,57 @@ 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)) @@ -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/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/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda index 6e7e963539..92b357a359 100644 --- a/Cubical/Relation/Binary/Base.agda +++ b/Cubical/Relation/Binary/Base.agda @@ -25,7 +25,7 @@ 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 ℓ')) diff --git a/Cubical/Relation/Binary/Order/Woset/Base.agda b/Cubical/Relation/Binary/Order/Woset/Base.agda index e88368b0db..730c2fe618 100644 --- a/Cubical/Relation/Binary/Order/Woset/Base.agda +++ b/Cubical/Relation/Binary/Order/Woset/Base.agda @@ -33,7 +33,7 @@ open BinaryRelation private variable - ℓ ℓ' ℓ'' ℓ₀ ℓ₀' ℓ₁ ℓ₁' : Level + ℓ ℓ' ℓ'' ℓ₀ ℓ₀' ℓ₁ ℓ₁' ℓ₂ ℓ₂' : Level record IsWoset {A : Type ℓ} (_≺_ : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where no-eta-equality @@ -91,6 +91,19 @@ record IsWosetEquiv {A : Type ℓ₀} {B : Type ℓ₁} 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 diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index a02411abe8..db75081176 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -8,7 +8,8 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Structure -open import Cubical.HITs.SetQuotients +open import Cubical.HITs.PropositionalTruncation as ∥₁ +open import Cubical.HITs.SetQuotients as /₂ open import Cubical.Induction.WellFounded @@ -17,15 +18,66 @@ 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.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 - ℓ ℓ' : Level + ℓ ℓ' ℓa ℓa' ℓb ℓb' ℓc ℓc' ℓd ℓd' : Level -isSimulation : (A B : Woset ℓ ℓ') (f : ⟨ A ⟩ → ⟨ B ⟩) → Type (ℓ-max ℓ ℓ') +-- We start with the truncated version and derive the untruncated +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) @@ -37,16 +89,26 @@ isSimulation A B f = monotone × lifting lifting = ∀ a b → b ≺ₛ (f a) → fiber {A = less a} (f ∘ fst) b -isSimulation→isEmbedding : (A B : Woset ℓ ℓ') → ∀ f +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' inda b' fa'≡fb' → isWeaklyExtensional→≺Equiv→≡ + (λ a' ind b' fa'≡fb' → isWeaklyExtensional→≺Equiv→≡ _≺ᵣ_ weakR a' b' λ c → propBiimpl→Equiv (propR c a') (propR c b') (λ c≺ᵣa' → subst (_≺ᵣ b') - (sym (inda c c≺ᵣa' + (sym (ind c c≺ᵣa' (efib b' (f c) (subst (f c ≺ₛ_) fa'≡fb' (rrel c a' c≺ᵣa')) .fst .fst) @@ -55,7 +117,7 @@ isSimulation→isEmbedding A B f (rrel , efib) (efib b' (f c) (subst (f c ≺ₛ_) fa'≡fb' (rrel c a' c≺ᵣa')) .fst .snd)) λ c≺ᵣb' → subst (_≺ᵣ a') - (inda (efib a' (f c) (subst (f c ≺ₛ_) + (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) @@ -66,101 +128,111 @@ isSimulation→isEmbedding A B f (rrel , efib) where _≺ᵣ_ = WosetStr._≺_ (str A) _≺ₛ_ = WosetStr._≺_ (str B) - IsWosetR = WosetStr.isWoset (str A) - IsWosetS = WosetStr.isWoset (str B) - - setB = IsWoset.is-set IsWosetS - - wellR = IsWoset.is-well-founded IsWosetR - - weakR = IsWoset.is-weakly-extensional IsWosetR + wosR = WosetStr.isWoset (str A) + wosS = WosetStr.isWoset (str B) - propR = IsWoset.is-prop-valued IsWosetR + setB = IsWoset.is-set wosS -isPropIsSimulation : (A B : Woset ℓ ℓ') → ∀ f → isProp (isSimulation A B f) + 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₀) - λ w x → isEmbeddingFstΣProp + λ _ _ → 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 ℓ ℓ') (Woset ℓ ℓ') (ℓ-max ℓ ℓ') +_≼_ : 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 -private - isRefl≼ : BinaryRelation.isRefl {A = Woset ℓ ℓ'} _≼_ - isRefl≼ A = (idfun ⟨ A ⟩) , ((λ _ _ a≺ᵣa' → a≺ᵣa') - , λ _ b b≺ₛfa → (b , b≺ₛfa) , refl) - - isSimulation-∘ : (A B C : Woset ℓ ℓ') → ∀ 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≼ : BinaryRelation.isTrans {A = Woset ℓ ℓ'} _≼_ - isTrans≼ A B C (f , simf) (g , simg) - = (g ∘ f) , (isSimulation-∘ A B C f g simf simg) - - isPropValued≼ : BinaryRelation.isPropValued {A = Woset ℓ ℓ'} _≼_ - isPropValued≼ A B (f , (rreff , fibf)) (g , (rrefg , fibg)) - = Σ≡Prop (λ _ → isPropIsSimulation A B _) - (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 A) - _≺ₛ_ = 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 - - isAntisym≼ : BinaryRelation.isAntisym {A = Woset ℓ ℓ'} _≼_ - isAntisym≼ A B (f , simf) (g , simg) = WosetPath A B .fst (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 +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 @@ -170,6 +242,34 @@ isPoset≼ = isposet 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 @@ -318,96 +418,293 @@ isEmbedding↓ A = injEmbedding isSetWoset (unique _ _) , Σ≡Prop (λ _ → prop _ _) (Σ≡Prop (λ _ → prop _ _) refl) -_≺_ : Rel (Woset ℓ ℓ) (Woset ℓ ℓ) (ℓ-suc ℓ) -A ≺ B = fiber (B ↓_) A +↓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 --- To avoid having this wind up in a higher universe, we define the same with equivalences -_≺'_ : Rel (Woset ℓ ℓ) (Woset ℓ ℓ) ℓ -A ≺' B = Σ[ b ∈ ⟨ B ⟩ ] WosetEquiv (B ↓ b) A +↓Monotone : (A : Woset ℓ ℓ') → ∀ a + → (A ↓ a) ≼ A +↓Monotone A a = f , sim + where _≺ᵣ_ = WosetStr._≺_ (str (A ↓ a)) + _≺ₛ_ = WosetStr._≺_ (str A) -≺≃≺' : (A B : Woset ℓ ℓ) → A ≺ B ≃ A ≺' B -≺≃≺' A B = invEquiv (Σ-cong-equiv (idEquiv ⟨ B ⟩) λ b → WosetPath (B ↓ b) A) + trans = IsWoset.is-trans (WosetStr.isWoset (str A)) -↓Decreasing : (A : Woset ℓ ℓ) → ∀ a - → (A ↓ a) ≺ A -↓Decreasing A a = a , refl + f : ⟨ A ↓ a ⟩ → ⟨ A ⟩ + f (a' , _) = a' -↓Respects≺ : (A : Woset ℓ ℓ) → ∀ a b - → WosetStr._≺_ (str A) a b - → (A ↓ a) ≺ (A ↓ b) -↓Respects≺ A a b a≺b = (a , a≺b) , (↓Absorb A b a a≺b) + sim : isSimulation (A ↓ a) A f + sim = mono , lifting + where mono : ∀ a' a'' → a' ≺ᵣ a'' → (f a') ≺ₛ (f a'') + mono _ _ a'≺ᵣa'' = a'≺ᵣa'' -↓Respects≺⁻ : (A : Woset ℓ ℓ) → ∀ a b - → (A ↓ a) ≺ (A ↓ b) + 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 -↓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 + → (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) - -≺Absorb↓ : (A B : Woset ℓ ℓ) - → Σ[ b ∈ ⟨ B ⟩ ] A ≺ (B ↓ b) + 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 -≺Absorb↓ A B (b , (b' , b'≺b) , B↓b↓b'≡A) = b' - , sym (↓Absorb B b b' b'≺b) ∙ B↓b↓b'≡A + → 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) --- Necessary intermediates to show that _<_ is well-ordered -private - isPropValued≺ : BinaryRelation.isPropValued (_≺_ {ℓ = ℓ}) - isPropValued≺ A B = isEmbedding→hasPropFibers (isEmbedding↓ B) A - - isAcc↓ : (A : Woset ℓ ℓ) → ∀ a → Acc _≺_ (A ↓ a) - isAcc↓ A = WFI.induction well λ a ind → acc (λ B B Date: Sat, 28 Oct 2023 19:39:02 +0000 Subject: [PATCH 17/21] Fix URL --- Cubical/Relation/Binary/Order/Woset/Simulation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index db75081176..302fb78614 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -715,7 +715,7 @@ isWoset≺ = iswoset {- 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#2612 + https://www.cs.bham.ac.uk/~mhe/agda/Ordinals.OrdinalOfOrdinalsSuprema.html -} private From dcd6d47df4417b410e1fcd7c7f3a4821cdac1ce8 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sun, 29 Oct 2023 04:35:40 +0000 Subject: [PATCH 18/21] Prove properties about ordinal arithmetic --- Cubical/Data/Empty/Base.agda | 3 + Cubical/Data/Ordinal/Base.agda | 3 + Cubical/Data/Ordinal/Properties.agda | 283 +++++++++++++++++++++++++++ Cubical/Data/Sum/Properties.agda | 18 +- 4 files changed, 298 insertions(+), 9 deletions(-) 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/Base.agda b/Cubical/Data/Ordinal/Base.agda index 22d66253d5..116fb8c4f9 100644 --- a/Cubical/Data/Ordinal/Base.agda +++ b/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 ℓ ℓ diff --git a/Cubical/Data/Ordinal/Properties.agda b/Cubical/Data/Ordinal/Properties.agda index 324199df52..0cfbd9d98c 100644 --- a/Cubical/Data/Ordinal/Properties.agda +++ b/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 Date: Sun, 29 Oct 2023 06:56:52 +0000 Subject: [PATCH 19/21] Fix missed definition name change --- Cubical/Data/Cardinal/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Data/Cardinal/Properties.agda b/Cubical/Data/Cardinal/Properties.agda index 3bb30f186a..1c7371cf0c 100644 --- a/Cubical/Data/Cardinal/Properties.agda +++ b/Cubical/Data/Cardinal/Properties.agda @@ -83,7 +83,7 @@ module _ where → 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 _ _)) From 215d886002051516dc69d9a6927eaf62129ea6e6 Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sun, 29 Oct 2023 07:03:08 +0000 Subject: [PATCH 20/21] Fix whitespace --- Cubical/Relation/Binary/Order/Woset/Simulation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index 302fb78614..da88ac9f81 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -539,7 +539,7 @@ A ≺ B = Σ[ b ∈ ⟨ B ⟩ ] WosetEquiv (B ↓ b) A 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) From 5ac0cf04cd75474c78f77809d3155f3680121dab Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Fri, 23 Feb 2024 01:47:40 +0000 Subject: [PATCH 21/21] Improved comments as per code review --- Cubical/Relation/Binary/Order/Woset/Simulation.agda | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Cubical/Relation/Binary/Order/Woset/Simulation.agda b/Cubical/Relation/Binary/Order/Woset/Simulation.agda index da88ac9f81..51b789b6e8 100644 --- a/Cubical/Relation/Binary/Order/Woset/Simulation.agda +++ b/Cubical/Relation/Binary/Order/Woset/Simulation.agda @@ -1,4 +1,7 @@ {-# 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 @@ -27,7 +30,9 @@ private variable ℓ ℓ' ℓa ℓa' ℓb ℓb' ℓc ℓc' ℓd ℓd' : Level --- We start with the truncated version and derive the untruncated +-- 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