From 85f8a71e97dc248c2a766f5c03357ffb524f5b95 Mon Sep 17 00:00:00 2001 From: Brad Dragun <35275808+LuuBluum@users.noreply.github.com> Date: Sat, 16 Sep 2023 03:07:53 -0700 Subject: [PATCH] Cardinality and Order (#969) * Proof that embeddings are monotone over sums Also cleaned up several aspects of things. * Embeddings are monotone over products * Define cardinal exponentiation * Minor formatting clean-up * Removal of some excessive imports * Renamed annihiliation by 0 to be less vague * Renamed Cantor's Theorem results * Cleaned up order property definitions * Replace renaming * Require preordering for order properties * Remove extra level variable that's unused * Removed redundant implicit level term * Replace type families with embeddings as subtypes More consistent with the idea of a "subset" and also makes reasoning easier by keeping the sigma types out of the type signatures. * Cleaned up types for embeddings in order props * Added function in Embedding to simplify constructs Sigma-types where the type family is always a prop embed into the first argument's type * Minor clean-up * Better respecting camel case * Name-cleaning and removing unused imports * Reintroduce erroneously-removed newline * Renamed loset to toset, strict loset to loset Also required losets to be weakly linear * Fixed paths in top-level file * Defined induced relations over embeddings * Better capitalization * Renamed one more detail * Moved order properties into their own folders * Reduced imports for cardinals * Removed unused apartness import * Changed capitalization back for conversions * Proved induced relations preserve order properties * Loosened embedding to mere function for bounds * Fixed whitespace * Fix rebase issues * Resolve PR comments --- Cubical/Algebra/DistLattice/BigOps.agda | 2 +- Cubical/Algebra/Lattice/Properties.agda | 2 +- Cubical/Algebra/OrderedCommMonoid/Base.agda | 2 +- .../OrderedCommMonoid/PropCompletion.agda | 2 +- .../Algebra/OrderedCommMonoid/Properties.agda | 2 +- Cubical/Algebra/Semilattice/Base.agda | 2 +- Cubical/Algebra/ZariskiLattice/Base.agda | 2 +- .../ZariskiLattice/StructureSheaf.agda | 2 +- .../StructureSheafPullback.agda | 2 +- .../ZariskiLattice/UniversalProperty.agda | 2 +- Cubical/Categories/DistLatticeSheaf/Base.agda | 2 +- .../DistLatticeSheaf/ComparisonLemma.agda | 2 +- .../Categories/DistLatticeSheaf/Diagram.agda | 2 +- .../DistLatticeSheaf/Extension.agda | 2 +- Cubical/Categories/Instances/Poset.agda | 2 +- Cubical/Data/Cardinality.agda | 5 + Cubical/Data/Cardinality/Base.agda | 54 ++++ Cubical/Data/Cardinality/Properties.agda | 194 +++++++++++ Cubical/Data/FinSet/Induction.agda | 4 +- Cubical/Data/Sigma/Properties.agda | 19 ++ Cubical/Data/Sum/Properties.agda | 119 ++++++- Cubical/Data/SumFin/Properties.agda | 20 +- Cubical/Functions/Embedding.agda | 36 +++ Cubical/Functions/Surjection.agda | 31 ++ Cubical/HITs/SetTruncation/Properties.agda | 7 + Cubical/Relation/Binary/Base.agda | 95 +++++- Cubical/Relation/Binary/Order.agda | 10 + Cubical/Relation/Binary/Order/Apartness.agda | 5 + .../Relation/Binary/Order/Apartness/Base.agda | 130 ++++++++ .../Binary/Order/Apartness/Properties.agda | 53 +++ Cubical/Relation/Binary/Order/Loset.agda | 5 + Cubical/Relation/Binary/Order/Loset/Base.agda | 134 ++++++++ .../Binary/Order/Loset/Properties.agda | 91 ++++++ Cubical/Relation/Binary/Order/Poset.agda | 5 + .../{Poset.agda => Order/Poset/Base.agda} | 2 +- .../Binary/Order/Poset/Properties.agda | 71 ++++ Cubical/Relation/Binary/Order/Preorder.agda | 5 + .../Relation/Binary/Order/Preorder/Base.agda | 135 ++++++++ .../Binary/Order/Preorder/Properties.agda | 57 ++++ Cubical/Relation/Binary/Order/Properties.agda | 302 ++++++++++++++++++ .../Relation/Binary/Order/StrictPoset.agda | 5 + .../Binary/Order/StrictPoset/Base.agda | 126 ++++++++ .../Binary/Order/StrictPoset/Properties.agda | 94 ++++++ Cubical/Relation/Binary/Order/Toset.agda | 5 + Cubical/Relation/Binary/Order/Toset/Base.agda | 146 +++++++++ .../Binary/Order/Toset/Properties.agda | 91 ++++++ 46 files changed, 2044 insertions(+), 42 deletions(-) create mode 100644 Cubical/Data/Cardinality.agda create mode 100644 Cubical/Data/Cardinality/Base.agda create mode 100644 Cubical/Data/Cardinality/Properties.agda create mode 100644 Cubical/Relation/Binary/Order.agda create mode 100644 Cubical/Relation/Binary/Order/Apartness.agda create mode 100644 Cubical/Relation/Binary/Order/Apartness/Base.agda create mode 100644 Cubical/Relation/Binary/Order/Apartness/Properties.agda create mode 100644 Cubical/Relation/Binary/Order/Loset.agda create mode 100644 Cubical/Relation/Binary/Order/Loset/Base.agda create mode 100644 Cubical/Relation/Binary/Order/Loset/Properties.agda create mode 100644 Cubical/Relation/Binary/Order/Poset.agda rename Cubical/Relation/Binary/{Poset.agda => Order/Poset/Base.agda} (98%) create mode 100644 Cubical/Relation/Binary/Order/Poset/Properties.agda create mode 100644 Cubical/Relation/Binary/Order/Preorder.agda create mode 100644 Cubical/Relation/Binary/Order/Preorder/Base.agda create mode 100644 Cubical/Relation/Binary/Order/Preorder/Properties.agda create mode 100644 Cubical/Relation/Binary/Order/Properties.agda create mode 100644 Cubical/Relation/Binary/Order/StrictPoset.agda create mode 100644 Cubical/Relation/Binary/Order/StrictPoset/Base.agda create mode 100644 Cubical/Relation/Binary/Order/StrictPoset/Properties.agda create mode 100644 Cubical/Relation/Binary/Order/Toset.agda create mode 100644 Cubical/Relation/Binary/Order/Toset/Base.agda create mode 100644 Cubical/Relation/Binary/Order/Toset/Properties.agda diff --git a/Cubical/Algebra/DistLattice/BigOps.agda b/Cubical/Algebra/DistLattice/BigOps.agda index 9138e42e53..a812d64641 100644 --- a/Cubical/Algebra/DistLattice/BigOps.agda +++ b/Cubical/Algebra/DistLattice/BigOps.agda @@ -29,7 +29,7 @@ open import Cubical.Algebra.CommMonoid open import Cubical.Algebra.Semilattice open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset private diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda index 3bc28d5fae..bd5f3ae8bf 100644 --- a/Cubical/Algebra/Lattice/Properties.agda +++ b/Cubical/Algebra/Lattice/Properties.agda @@ -21,7 +21,7 @@ open import Cubical.Algebra.CommMonoid open import Cubical.Algebra.Semilattice open import Cubical.Algebra.Lattice.Base -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset private variable diff --git a/Cubical/Algebra/OrderedCommMonoid/Base.agda b/Cubical/Algebra/OrderedCommMonoid/Base.agda index 22aaf7cc15..c7091f0359 100644 --- a/Cubical/Algebra/OrderedCommMonoid/Base.agda +++ b/Cubical/Algebra/OrderedCommMonoid/Base.agda @@ -10,7 +10,7 @@ open import Cubical.Foundations.Structure using (⟨_⟩; str) open import Cubical.Algebra.CommMonoid.Base -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset private variable diff --git a/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda b/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda index df93645aca..cdacdc7dad 100644 --- a/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda +++ b/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda @@ -28,7 +28,7 @@ open import Cubical.HITs.PropositionalTruncation renaming (rec to propTruncRec; open import Cubical.Algebra.CommMonoid.Base open import Cubical.Algebra.OrderedCommMonoid -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset private variable diff --git a/Cubical/Algebra/OrderedCommMonoid/Properties.agda b/Cubical/Algebra/OrderedCommMonoid/Properties.agda index 208db81eb6..1e849d1b2f 100644 --- a/Cubical/Algebra/OrderedCommMonoid/Properties.agda +++ b/Cubical/Algebra/OrderedCommMonoid/Properties.agda @@ -11,7 +11,7 @@ open import Cubical.Data.Sigma open import Cubical.Algebra.CommMonoid open import Cubical.Algebra.OrderedCommMonoid.Base -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset private diff --git a/Cubical/Algebra/Semilattice/Base.agda b/Cubical/Algebra/Semilattice/Base.agda index dd06511816..3d6f9226ac 100644 --- a/Cubical/Algebra/Semilattice/Base.agda +++ b/Cubical/Algebra/Semilattice/Base.agda @@ -34,7 +34,7 @@ open import Cubical.Displayed.Record open import Cubical.Displayed.Universe open import Cubical.Relation.Binary -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Reflection.RecordEquiv diff --git a/Cubical/Algebra/ZariskiLattice/Base.agda b/Cubical/Algebra/ZariskiLattice/Base.agda index a32b123fd4..7bc8b026f9 100644 --- a/Cubical/Algebra/ZariskiLattice/Base.agda +++ b/Cubical/Algebra/ZariskiLattice/Base.agda @@ -22,7 +22,7 @@ open import Cubical.Data.FinData open import Cubical.Data.Unit open import Cubical.Relation.Nullary open import Cubical.Relation.Binary -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Algebra.Ring open import Cubical.Algebra.Ring.Properties diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda index e736e3ddd0..2b53e779a5 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda +++ b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda @@ -34,7 +34,7 @@ open import Cubical.Data.FinData open import Cubical.Data.Unit open import Cubical.Relation.Nullary open import Cubical.Relation.Binary -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Algebra.Ring open import Cubical.Algebra.Ring.Properties diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda index a73a8870b4..01a8dcd11f 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda +++ b/Cubical/Algebra/ZariskiLattice/StructureSheafPullback.agda @@ -34,7 +34,7 @@ open import Cubical.Data.FinData open import Cubical.Data.Unit open import Cubical.Relation.Nullary open import Cubical.Relation.Binary -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Algebra.Ring open import Cubical.Algebra.Ring.Properties diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index fd8ee41fe2..2216c737b3 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -23,7 +23,7 @@ open import Cubical.Data.FinData open import Cubical.Data.Unit open import Cubical.Relation.Nullary open import Cubical.Relation.Binary -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Algebra.Ring open import Cubical.Algebra.Ring.Properties diff --git a/Cubical/Categories/DistLatticeSheaf/Base.agda b/Cubical/Categories/DistLatticeSheaf/Base.agda index 0cd74a873a..b2b0e01110 100644 --- a/Cubical/Categories/DistLatticeSheaf/Base.agda +++ b/Cubical/Categories/DistLatticeSheaf/Base.agda @@ -10,7 +10,7 @@ open import Cubical.Data.Nat using (ℕ) open import Cubical.Data.Nat.Order open import Cubical.Data.FinData -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Algebra.Semilattice open import Cubical.Algebra.Lattice diff --git a/Cubical/Categories/DistLatticeSheaf/ComparisonLemma.agda b/Cubical/Categories/DistLatticeSheaf/ComparisonLemma.agda index dad5af7040..3eaf2dfd27 100644 --- a/Cubical/Categories/DistLatticeSheaf/ComparisonLemma.agda +++ b/Cubical/Categories/DistLatticeSheaf/ComparisonLemma.agda @@ -26,7 +26,7 @@ open import Cubical.Data.FinData open import Cubical.Data.FinData.Order open import Cubical.Data.Sum -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.HITs.PropositionalTruncation as PT open import Cubical.Algebra.Semilattice diff --git a/Cubical/Categories/DistLatticeSheaf/Diagram.agda b/Cubical/Categories/DistLatticeSheaf/Diagram.agda index f5d0a68583..cc2f0b4780 100644 --- a/Cubical/Categories/DistLatticeSheaf/Diagram.agda +++ b/Cubical/Categories/DistLatticeSheaf/Diagram.agda @@ -21,7 +21,7 @@ open import Cubical.Data.FinData.Order renaming (_<'Fin_ to _<_) open import Cubical.Data.Sum open import Cubical.Relation.Nullary -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Categories.Category open import Cubical.Categories.Functor diff --git a/Cubical/Categories/DistLatticeSheaf/Extension.agda b/Cubical/Categories/DistLatticeSheaf/Extension.agda index 600e1188f2..4687ad8189 100644 --- a/Cubical/Categories/DistLatticeSheaf/Extension.agda +++ b/Cubical/Categories/DistLatticeSheaf/Extension.agda @@ -23,7 +23,7 @@ open import Cubical.Data.FinData open import Cubical.Data.FinData.Order open import Cubical.Data.Sum -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.HITs.PropositionalTruncation open import Cubical.Algebra.Semilattice diff --git a/Cubical/Categories/Instances/Poset.agda b/Cubical/Categories/Instances/Poset.agda index 720326e9b8..f7a8baf73d 100644 --- a/Cubical/Categories/Instances/Poset.agda +++ b/Cubical/Categories/Instances/Poset.agda @@ -3,7 +3,7 @@ module Cubical.Categories.Instances.Poset where open import Cubical.Foundations.Prelude -open import Cubical.Relation.Binary.Poset +open import Cubical.Relation.Binary.Order.Poset open import Cubical.Categories.Category diff --git a/Cubical/Data/Cardinality.agda b/Cubical/Data/Cardinality.agda new file mode 100644 index 0000000000..2c992fe9c8 --- /dev/null +++ b/Cubical/Data/Cardinality.agda @@ -0,0 +1,5 @@ +{-# 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/Cardinality/Base.agda b/Cubical/Data/Cardinality/Base.agda new file mode 100644 index 0000000000..56f161145f --- /dev/null +++ b/Cubical/Data/Cardinality/Base.agda @@ -0,0 +1,54 @@ +{- + +This file contains: + +- Treatment of set truncation as cardinality + as per the HoTT book, section 10.2 + +-} +{-# OPTIONS --safe #-} +module Cubical.Data.Cardinality.Base where + +open import Cubical.HITs.SetTruncation as ∥₂ +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Empty +open import Cubical.Data.Sigma +open import Cubical.Data.Sum +open import Cubical.Data.Unit + +private + variable + ℓ : Level + +-- First, we define a cardinal as the set truncation of Set +Card : Type (ℓ-suc ℓ) +Card {ℓ} = ∥ hSet ℓ ∥₂ + +-- Verify that it's a set +isSetCard : isSet (Card {ℓ}) +isSetCard = isSetSetTrunc + +-- Set truncation of a set is its cardinality +card : hSet ℓ → Card {ℓ} +card = ∣_∣₂ + +-- Some special cardinalities +𝟘 : Card {ℓ} +𝟘 = card (⊥* , isProp→isSet isProp⊥*) + +𝟙 : Card {ℓ} +𝟙 = card (Unit* , isSetUnit*) + +-- Now we define some arithmetic +_+_ : Card {ℓ} → Card {ℓ} → Card {ℓ} +_+_ = ∥₂.rec2 isSetCard λ (A , isSetA) (B , isSetB) + → card ((A ⊎ B) , isSet⊎ isSetA isSetB) + +_·_ : Card {ℓ} → Card {ℓ} → Card {ℓ} +_·_ = ∥₂.rec2 isSetCard λ (A , isSetA) (B , isSetB) + → card ((A × B) , isSet× isSetA isSetB) + +_^_ : Card {ℓ} → Card {ℓ} → Card {ℓ} +_^_ = ∥₂.rec2 isSetCard λ (A , isSetA) (B , _) + → card ((B → A) , isSet→ isSetA) diff --git a/Cubical/Data/Cardinality/Properties.agda b/Cubical/Data/Cardinality/Properties.agda new file mode 100644 index 0000000000..77a6dba379 --- /dev/null +++ b/Cubical/Data/Cardinality/Properties.agda @@ -0,0 +1,194 @@ +{- + +This file contains: + +- Properties of cardinality +- Preordering of cardinalities + +-} +{-# OPTIONS --safe #-} +module Cubical.Data.Cardinality.Properties where + +open import Cubical.HITs.SetTruncation as ∥₂ +open import Cubical.Data.Cardinality.Base + +open import Cubical.Algebra.CommSemiring + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure +open import Cubical.Functions.Embedding +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.HITs.PropositionalTruncation as ∥₁ +open import Cubical.Relation.Binary.Base +open import Cubical.Relation.Binary.Order.Preorder.Base +open import Cubical.Relation.Binary.Order.Properties + +private + variable + ℓ : Level + +-- Cardinality is a commutative semiring +module _ where + private + +Assoc : (A B C : Card {ℓ}) → 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 = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _)) + λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (sym (isoToPath Σ-assoc-Iso))) + + +IdR𝟘 : (A : Card {ℓ}) → A + 𝟘 ≡ A + +IdR𝟘 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath ⊎-IdR-⊥*-Iso)) + + +IdL𝟘 : (A : Card {ℓ}) → 𝟘 + A ≡ A + +IdL𝟘 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath ⊎-IdL-⊥*-Iso)) + + ·IdR𝟙 : (A : Card {ℓ}) → A · 𝟙 ≡ A + ·IdR𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath rUnit*×Iso)) + + ·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 = ∥₂.elim2 (λ _ _ → isProp→isSet (isSetCard _ _)) + λ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath ⊎-swap-Iso)) + + ·Comm : (A B : Card {ℓ}) → (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+ = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _)) + λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath ×DistL⊎Iso)) + + AnnihilL : (A : Card {ℓ}) → 𝟘 · A ≡ 𝟘 + AnnihilL = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath (ΣEmpty*Iso λ _ → _))) + + isCardCommSemiring : IsCommSemiring {ℓ-suc ℓ} 𝟘 𝟙 _+_ _·_ + isCardCommSemiring = makeIsCommSemiring isSetCard +Assoc +IdR𝟘 +Comm ·Assoc ·IdR𝟙 ·LDist+ AnnihilL ·Comm + +-- Exponentiation is also well-behaved + +^AnnihilR𝟘 : (A : Card {ℓ}) → A ^ 𝟘 ≡ 𝟙 +^AnnihilR𝟘 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath (iso⊥ _))) + where iso⊥ : ∀ A → Iso (⊥* → A) Unit* + Iso.fun (iso⊥ A) _ = tt* + Iso.inv (iso⊥ A) _ () + Iso.rightInv (iso⊥ A) _ = refl + Iso.leftInv (iso⊥ A) _ i () + +^IdR𝟙 : (A : Card {ℓ}) → A ^ 𝟙 ≡ A +^IdR𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath (iso⊤ _))) + where iso⊤ : ∀ A → Iso (Unit* → A) A + Iso.fun (iso⊤ _) f = f tt* + Iso.inv (iso⊤ _) a _ = a + Iso.rightInv (iso⊤ _) _ = refl + Iso.leftInv (iso⊤ _) _ = refl + +^AnnihilL𝟙 : (A : Card {ℓ}) → 𝟙 ^ A ≡ 𝟙 +^AnnihilL𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) + λ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath (iso⊤ _))) + where iso⊤ : ∀ A → Iso (A → Unit*) Unit* + Iso.fun (iso⊤ _) _ = tt* + Iso.inv (iso⊤ _) _ _ = tt* + Iso.rightInv (iso⊤ _) _ = refl + Iso.leftInv (iso⊤ _) _ = refl + +^LDist+ : (A B C : Card {ℓ}) → 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· = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _)) + λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath (is _ _ _))) + where is : ∀ A B C → Iso (B × C → A) (C → B → A) + is A B C = (B × C → A) Iso⟨ domIso Σ-swap-Iso ⟩ + (C × B → A) Iso⟨ curryIso ⟩ + (C → B → A) ∎Iso + +^RDist· : (A B C : Card {ℓ}) → (A · B) ^ C ≡ (A ^ C) · (B ^ C) +^RDist· = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _)) + λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet) + (isoToPath Σ-Π-Iso)) + + +-- With basic arithmetic done, we can now define an ordering over cardinals +module _ where + private + _≲'_ : Card {ℓ} → Card {ℓ} → hProp ℓ + _≲'_ = ∥₂.rec2 isSetHProp λ (A , _) (B , _) → ∥ A ↪ B ∥₁ , isPropPropTrunc + + _≲_ : Rel (Card {ℓ}) (Card {ℓ}) ℓ + A ≲ B = ⟨ 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) + +isLeast𝟘 : ∀{ℓ} → isLeast isPreorder≲ (Card {ℓ} , id↪ (Card {ℓ})) (𝟘 {ℓ}) +isLeast𝟘 = ∥₂.elim (λ x → isProp→isSet (IsPreorder.is-prop-valued + isPreorder≲ 𝟘 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≲ + = ∥₂.elim4 (λ w x y z → isSetΠ2 λ _ _ → isProp→isSet (IsPreorder.is-prop-valued + isPreorder≲ + (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≲ + = ∥₂.elim4 (λ w x y z → isSetΠ2 λ _ _ → isProp→isSet (IsPreorder.is-prop-valued + isPreorder≲ + (w · x) + (y · z))) + λ (A , _) (B , _) (C , _) (D , _) + → ∥₁.map2 λ A↪C B↪D → ×Monotone↪ A↪C B↪D diff --git a/Cubical/Data/FinSet/Induction.agda b/Cubical/Data/FinSet/Induction.agda index 81cb16ba85..624e69fa32 100644 --- a/Cubical/Data/FinSet/Induction.agda +++ b/Cubical/Data/FinSet/Induction.agda @@ -72,13 +72,13 @@ module _ -- 𝔽in preserves addition 𝟘+X≡X : {X : FinSet ℓ} → 𝟘 + X ≡ X - 𝟘+X≡X {X = X} i .fst = ua (⊎-swap-≃ ⋆ ⊎-equiv (idEquiv (X .fst)) 𝟘≃Empty ⋆ ⊎-⊥-≃) i + 𝟘+X≡X {X = X} i .fst = ua (⊎-swap-≃ ⋆ ⊎-equiv (idEquiv (X .fst)) 𝟘≃Empty ⋆ ⊎-IdR-⊥-≃) i 𝟘+X≡X {X = X} i .snd = isProp→PathP {B = λ i → isFinSet (𝟘+X≡X {X = X} i .fst)} (λ _ → isPropIsFinSet) ((𝟘 + X) .snd) (X .snd) i 𝔽in1≡𝟙 : 𝔽in 1 ≡ 𝟙 - 𝔽in1≡𝟙 i .fst = ua (⊎-equiv (idEquiv (𝟙 .fst)) 𝟘≃Empty ⋆ ⊎-⊥-≃) i + 𝔽in1≡𝟙 i .fst = ua (⊎-equiv (idEquiv (𝟙 .fst)) 𝟘≃Empty ⋆ ⊎-IdR-⊥-≃) i 𝔽in1≡𝟙 i .snd = isProp→PathP {B = λ i → isFinSet (𝔽in1≡𝟙 i .fst)} (λ _ → isPropIsFinSet) (𝔽in 1 .snd) (𝟙 .snd) i diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda index 4f2713a1ed..9feb97602e 100644 --- a/Cubical/Data/Sigma/Properties.agda +++ b/Cubical/Data/Sigma/Properties.agda @@ -136,12 +136,24 @@ inv lUnit×Iso = tt ,_ rightInv lUnit×Iso _ = refl leftInv lUnit×Iso _ = refl +lUnit*×Iso : ∀{ℓ} → Iso (Unit* {ℓ} × A) A +fun lUnit*×Iso = snd +inv lUnit*×Iso = tt* ,_ +rightInv lUnit*×Iso _ = refl +leftInv lUnit*×Iso _ = refl + rUnit×Iso : Iso (A × Unit) A fun rUnit×Iso = fst inv rUnit×Iso = _, tt rightInv rUnit×Iso _ = refl leftInv rUnit×Iso _ = refl +rUnit*×Iso : ∀{ℓ} → Iso (A × Unit* {ℓ}) A +fun rUnit*×Iso = fst +inv rUnit*×Iso = _, tt* +rightInv rUnit*×Iso _ = refl +leftInv rUnit*×Iso _ = refl + module _ {A : Type ℓ} {A' : Type ℓ'} where Σ-swap-Iso : Iso (A × A') (A' × A) fun Σ-swap-Iso (x , y) = (y , x) @@ -421,6 +433,13 @@ module _ (A : ⊥ → Type ℓ) where ΣEmpty : Σ ⊥ A ≃ ⊥ ΣEmpty = isoToEquiv ΣEmptyIso +module _ {ℓ : Level} (A : ⊥* {ℓ} → Type ℓ) where + + open Iso + + ΣEmpty*Iso : Iso (Σ ⊥* A) ⊥* + fun ΣEmpty*Iso (* , _) = * + -- fiber of projection map module _ diff --git a/Cubical/Data/Sum/Properties.agda b/Cubical/Data/Sum/Properties.agda index 491a377570..b469b59ccf 100644 --- a/Cubical/Data/Sum/Properties.agda +++ b/Cubical/Data/Sum/Properties.agda @@ -2,17 +2,18 @@ module Cubical.Data.Sum.Properties where open import Cubical.Core.Everything +open import Cubical.Foundations.Function open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Functions.Embedding open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism -open import Cubical.Data.Empty +open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Nat open import Cubical.Data.Sigma open import Cubical.Relation.Nullary -open import Cubical.Data.Sum.Base +open import Cubical.Data.Sum.Base as ⊎ open Iso @@ -99,6 +100,12 @@ isOfHLevel⊎ n lA lB c c' = (⊎Path.decodeEncode c c') (⊎Path.isOfHLevelCover n lA lB c c') +isProp⊎ : isProp A → isProp B → (A → B → ⊥) → isProp (A ⊎ B) +isProp⊎ propA _ _ (inl x) (inl y) i = inl (propA x y i) +isProp⊎ _ _ AB⊥ (inl x) (inr y) = ⊥.rec (AB⊥ x y) +isProp⊎ _ _ AB⊥ (inr x) (inl y) = ⊥.rec (AB⊥ y x) +isProp⊎ _ propB _ (inr x) (inr y) i = inr (propB x y i) + isSet⊎ : isSet A → isSet B → isSet (A ⊎ B) isSet⊎ = isOfHLevel⊎ 0 @@ -159,14 +166,41 @@ leftInv ⊎-assoc-Iso (inr _) = refl ⊎-assoc-≃ : (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C) ⊎-assoc-≃ = isoToEquiv ⊎-assoc-Iso -⊎-⊥-Iso : Iso (A ⊎ ⊥) A -fun ⊎-⊥-Iso (inl x) = x -inv ⊎-⊥-Iso x = inl x -rightInv ⊎-⊥-Iso _ = refl -leftInv ⊎-⊥-Iso (inl _) = refl +⊎-IdR-⊥-Iso : Iso (A ⊎ ⊥) A +fun ⊎-IdR-⊥-Iso (inl x) = x +inv ⊎-IdR-⊥-Iso x = inl x +rightInv ⊎-IdR-⊥-Iso _ = refl +leftInv ⊎-IdR-⊥-Iso (inl _) = refl + +⊎-IdL-⊥-Iso : Iso (⊥ ⊎ A) A +fun ⊎-IdL-⊥-Iso (inr x) = x +inv ⊎-IdL-⊥-Iso x = inr x +rightInv ⊎-IdL-⊥-Iso _ = refl +leftInv ⊎-IdL-⊥-Iso (inr _) = refl + +⊎-IdL-⊥*-Iso : ∀{ℓ} → Iso (⊥* {ℓ} ⊎ A) A +fun ⊎-IdL-⊥*-Iso (inr x) = x +inv ⊎-IdL-⊥*-Iso x = inr x +rightInv ⊎-IdL-⊥*-Iso _ = refl +leftInv ⊎-IdL-⊥*-Iso (inr _) = refl + +⊎-IdR-⊥*-Iso : ∀{ℓ} → Iso (A ⊎ ⊥* {ℓ}) A +fun ⊎-IdR-⊥*-Iso (inl x) = x +inv ⊎-IdR-⊥*-Iso x = inl x +rightInv ⊎-IdR-⊥*-Iso _ = refl +leftInv ⊎-IdR-⊥*-Iso (inl _) = refl -⊎-⊥-≃ : A ⊎ ⊥ ≃ A -⊎-⊥-≃ = isoToEquiv ⊎-⊥-Iso +⊎-IdR-⊥-≃ : A ⊎ ⊥ ≃ A +⊎-IdR-⊥-≃ = isoToEquiv ⊎-IdR-⊥-Iso + +⊎-IdL-⊥-≃ : ⊥ ⊎ A ≃ A +⊎-IdL-⊥-≃ = isoToEquiv ⊎-IdL-⊥-Iso + +⊎-IdR-⊥*-≃ : ∀{ℓ} → A ⊎ ⊥* {ℓ} ≃ A +⊎-IdR-⊥*-≃ = isoToEquiv ⊎-IdR-⊥*-Iso + +⊎-IdL-⊥*-≃ : ∀{ℓ} → ⊥* {ℓ} ⊎ A ≃ A +⊎-IdL-⊥*-≃ = isoToEquiv ⊎-IdL-⊥*-Iso Π⊎Iso : Iso ((x : A ⊎ B) → E x) (((a : A) → E (inl a)) × ((b : B) → E (inr b))) fun Π⊎Iso f .fst a = f (inl a) @@ -188,12 +222,73 @@ 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 + Π⊎≃ : ((x : A ⊎ B) → E x) ≃ ((a : A) → E (inl a)) × ((b : B) → E (inr b)) Π⊎≃ = isoToEquiv Π⊎Iso Σ⊎≃ : (Σ (A ⊎ B) E) ≃ ((Σ A (λ a → E (inl a))) ⊎ (Σ B (λ b → E (inr b)))) Σ⊎≃ = isoToEquiv Σ⊎Iso -map-⊎ : (A → C) → (B → D) → A ⊎ B → C ⊎ D -map-⊎ f _ (inl a) = inl (f a) -map-⊎ _ g (inr b) = inr (g b) +⊎Monotone↪ : A ↪ C → B ↪ D → (A ⊎ B) ↪ (C ⊎ D) +⊎Monotone↪ (f , embf) (g , embg) = (map f g) , emb + where coverToMap : ∀ x y → ⊎Path.Cover x y + → ⊎Path.Cover (map f g x) (map f g y) + coverToMap (inl _) (inl _) cover = lift (cong f (lower cover)) + coverToMap (inr _) (inr _) cover = lift (cong g (lower cover)) + + equiv : ∀ x y → isEquiv (coverToMap x y) + equiv (inl a₀) (inl a₁) + = ((invEquiv LiftEquiv) + ∙ₑ ((cong f) , (embf a₀ a₁)) + ∙ₑ LiftEquiv) .snd + equiv (inl a₀) (inr b₁) .equiv-proof () + equiv (inr b₀) (inl a₁) .equiv-proof () + equiv (inr b₀) (inr b₁) + = ((invEquiv LiftEquiv) + ∙ₑ ((cong g) , (embg b₀ b₁)) + ∙ₑ LiftEquiv) .snd + + lemma : ∀ x y + → ∀ (p : x ≡ y) + → cong (map f g) p ≡ + ⊎Path.decode + (map f g x) + (map f g y) + (coverToMap x y (⊎Path.encode x y p)) + lemma (inl a₀) _ + = J (λ y p + → cong (map f g) p ≡ + ⊎Path.decode (map f g (inl a₀)) + (map f g y) + (coverToMap (inl a₀) y + (⊎Path.encode (inl a₀) y p))) + (sym $ cong (cong inl) (cong (cong f) (transportRefl _))) + lemma (inr b₀) _ + = J (λ y p + → cong (map f g) p ≡ + ⊎Path.decode + (map f g (inr b₀)) + (map f g y) + (coverToMap (inr b₀) y (⊎Path.encode (inr b₀) y p))) + (sym $ cong (cong inr) (cong (cong g) (transportRefl _))) + + emb : isEmbedding (map f g) + emb x y = subst (λ eq → isEquiv eq) + (sym (funExt (lemma x y))) + ((x ≡ y ≃⟨ invEquiv (⊎Path.Cover≃Path x y) ⟩ + ⊎Path.Cover x y ≃⟨ (coverToMap x y) , (equiv x y) ⟩ + ⊎Path.Cover + (map f g x) + (map f g y) ≃⟨ ⊎Path.Cover≃Path + (map f g x) + (map f g y) ⟩ + map f g x ≡ map f g y ■) .snd) diff --git a/Cubical/Data/SumFin/Properties.agda b/Cubical/Data/SumFin/Properties.agda index ae453f7166..41a7d2ffe9 100644 --- a/Cubical/Data/SumFin/Properties.agda +++ b/Cubical/Data/SumFin/Properties.agda @@ -17,7 +17,7 @@ open import Cubical.Data.Nat.Order import Cubical.Data.Fin as Fin import Cubical.Data.Fin.LehmerCode as LehmerCode open import Cubical.Data.SumFin.Base as SumFin -open import Cubical.Data.Sum +open import Cubical.Data.Sum as ⊎ open import Cubical.Data.Sigma open import Cubical.HITs.PropositionalTruncation as Prop @@ -68,7 +68,7 @@ enumElim P f i = subst P (SumFin→Fin→SumFin i) (f (SumFin→Fin i .fst) (Sum -- Closure properties of SumFin under type constructors SumFin⊎≃ : (m n : ℕ) → (Fin m ⊎ Fin n) ≃ (Fin (m + n)) -SumFin⊎≃ 0 n = ⊎-swap-≃ ⋆ ⊎-⊥-≃ +SumFin⊎≃ 0 n = ⊎-swap-≃ ⋆ ⊎-IdR-⊥-≃ SumFin⊎≃ (suc m) n = ⊎-assoc-≃ ⋆ ⊎-equiv (idEquiv ⊤) (SumFin⊎≃ m n) SumFinΣ≃ : (n : ℕ)(f : Fin n → ℕ) → (Σ (Fin n) (λ x → Fin (f x))) ≃ (Fin (totalSum f)) @@ -82,7 +82,7 @@ SumFin×≃ : (m n : ℕ) → (Fin m × Fin n) ≃ (Fin (m · n)) SumFin×≃ m n = SumFinΣ≃ m (λ _ → n) ⋆ pathToEquiv (λ i → Fin (totalSumConst {m = m} n i)) SumFinΠ≃ : (n : ℕ)(f : Fin n → ℕ) → ((x : Fin n) → Fin (f x)) ≃ (Fin (totalProd f)) -SumFinΠ≃ 0 _ = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-⊥-≃) +SumFinΠ≃ 0 _ = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-IdR-⊥-≃) SumFinΠ≃ (suc n) f = Π⊎≃ ⋆ Σ-cong-equiv (ΠUnit (λ tt → Fin (f (inl tt)))) (λ _ → SumFinΠ≃ n (λ x → f (inr x))) @@ -96,7 +96,7 @@ SumFin∥∥≃ : (n : ℕ) → ∥ Fin n ∥₁ ≃ Fin (isNotZero n) SumFin∥∥≃ 0 = propTruncIdempotent≃ (isProp⊥) SumFin∥∥≃ (suc n) = isContr→≃Unit (inhProp→isContr ∣ inl tt ∣₁ isPropPropTrunc) - ⋆ isContr→≃Unit (isContrUnit) ⋆ invEquiv (⊎-⊥-≃) + ⋆ isContr→≃Unit (isContrUnit) ⋆ invEquiv (⊎-IdR-⊥-≃) ℕ→Bool : ℕ → Bool ℕ→Bool 0 = false @@ -115,7 +115,7 @@ SumFin¬ (suc n) = uninhabEquiv (λ f → f fzero) ⊥.rec -- SumFin 1 is equivalent to unit Fin1≃Unit : Fin 1 ≃ Unit -Fin1≃Unit = ⊎-⊥-≃ +Fin1≃Unit = ⊎-IdR-⊥-≃ isContrSumFin1 : isContr (Fin 1) isContrSumFin1 = isOfHLevelRespectEquiv 0 (invEquiv Fin1≃Unit) isContrUnit @@ -123,12 +123,12 @@ isContrSumFin1 = isOfHLevelRespectEquiv 0 (invEquiv Fin1≃Unit) isContrUnit -- SumFin 2 is equivalent to Bool SumFin2≃Bool : Fin 2 ≃ Bool -SumFin2≃Bool = ⊎-equiv (idEquiv _) ⊎-⊥-≃ ⋆ isoToEquiv Iso-⊤⊎⊤-Bool +SumFin2≃Bool = ⊎-equiv (idEquiv _) ⊎-IdR-⊥-≃ ⋆ isoToEquiv Iso-⊤⊎⊤-Bool -- decidable predicate over SumFin SumFinℙ≃ : (n : ℕ) → (Fin n → Bool) ≃ Fin (2 ^ n) -SumFinℙ≃ 0 = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-⊥-≃) +SumFinℙ≃ 0 = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-IdR-⊥-≃) SumFinℙ≃ (suc n) = Π⊎≃ ⋆ Σ-cong-equiv (UnitToType≃ Bool ⋆ invEquiv SumFin2≃Bool) (λ _ → SumFinℙ≃ n) @@ -146,7 +146,7 @@ trueCount {n = suc n} f = Bool→ℕ (f (inl tt)) + (trueCount (f ∘ inr)) SumFinDec⊎≃ : (n : ℕ)(t : Bool) → (Bool→Type t ⊎ Fin n) ≃ (Fin (Bool→ℕ t + n)) SumFinDec⊎≃ _ true = idEquiv _ -SumFinDec⊎≃ _ false = ⊎-swap-≃ ⋆ ⊎-⊥-≃ +SumFinDec⊎≃ _ false = ⊎-swap-≃ ⋆ ⊎-IdR-⊥-≃ SumFinSub≃ : (n : ℕ)(f : Fin n → Bool) → Σ _ (Bool→Type ∘ f) ≃ Fin (trueCount f) SumFinSub≃ 0 _ = ΣEmpty _ @@ -169,14 +169,14 @@ SumFin∃→ : (n : ℕ)(f : Fin n → Bool) → Σ _ (Bool→Type ∘ f) → Bo SumFin∃→ 0 _ = ΣEmpty _ .fst SumFin∃→ (suc n) f = Bool→Type⊎' _ _ - ∘ map-⊎ (ΣUnit (Bool→Type ∘ f ∘ inl) .fst) (SumFin∃→ n (f ∘ inr)) + ∘ ⊎.map (ΣUnit (Bool→Type ∘ f ∘ inl) .fst) (SumFin∃→ n (f ∘ inr)) ∘ Σ⊎≃ .fst SumFin∃← : (n : ℕ)(f : Fin n → Bool) → Bool→Type (trueForSome n f) → Σ _ (Bool→Type ∘ f) SumFin∃← 0 _ = ⊥.rec SumFin∃← (suc n) f = invEq Σ⊎≃ - ∘ map-⊎ (invEq (ΣUnit (Bool→Type ∘ f ∘ inl))) (SumFin∃← n (f ∘ inr)) + ∘ ⊎.map (invEq (ΣUnit (Bool→Type ∘ f ∘ inl))) (SumFin∃← n (f ∘ inr)) ∘ Bool→Type⊎ _ _ SumFin∃≃ : (n : ℕ)(f : Fin n → Bool) → ∥ Σ (Fin n) (Bool→Type ∘ f) ∥₁ ≃ Bool→Type (trueForSome n f) diff --git a/Cubical/Functions/Embedding.agda b/Cubical/Functions/Embedding.agda index bf5c11648d..bcc5a7b83e 100644 --- a/Cubical/Functions/Embedding.agda +++ b/Cubical/Functions/Embedding.agda @@ -181,6 +181,9 @@ isEquiv→isEmbedding e = λ _ _ → congEquiv (_ , e) .snd Equiv→Embedding : A ≃ B → A ↪ B Equiv→Embedding (f , isEquivF) = (f , isEquiv→isEmbedding isEquivF) +id↪ : ∀ {ℓ} → (A : Type ℓ) → A ↪ A +id↪ A = Equiv→Embedding (idEquiv A) + iso→isEmbedding : ∀ {ℓ} {A B : Type ℓ} → (isom : Iso A B) ------------------------------- @@ -438,3 +441,36 @@ _≃Emb_ = EmbeddingIdentityPrinciple.f≃g EmbeddingIP : {B : Type ℓ} (f g : Embedding B ℓ') → f ≃Emb g ≃ (f ≡ g) EmbeddingIP = EmbeddingIdentityPrinciple.EmbeddingIP + +-- Cantor's theorem for sets +Set-Embedding-into-Powerset : {A : Type ℓ} → isSet A → A ↪ ℙ A +Set-Embedding-into-Powerset {A = A} setA + = fun , (injEmbedding isSetℙ (λ y → sym (H₃ (H₂ y)))) + where fun : A → ℙ A + fun a b = (a ≡ b) , (setA a b) + + H₂ : {a b : A} → fun a ≡ fun b → a ∈ (fun b) + H₂ {a} fa≡fb = transport (cong (fst ∘ (_$ a)) fa≡fb) refl + + H₃ : {a b : A} → b ∈ (fun a) → a ≡ b + H₃ b∈fa = b∈fa + +×Monotone↪ : ∀ {ℓa ℓb ℓc ℓd} + {A : Type ℓa} {B : Type ℓb} {C : Type ℓc} {D : Type ℓd} + → A ↪ C → B ↪ D → (A × B) ↪ (C × D) +×Monotone↪ {A = A} {B = B} {C = C} {D = D} (f , embf) (g , embg) + = (map-× f g) , emb + where apmap : ∀ x y → x ≡ y → map-× f g x ≡ map-× f g y + apmap x y x≡y = ΣPathP (cong (f ∘ fst) x≡y , cong (g ∘ snd) x≡y) + + equiv : ∀ x y → isEquiv (apmap x y) + equiv x y = ((invEquiv ΣPathP≃PathPΣ) + ∙ₑ (≃-× ((cong f) , (embf (fst x) (fst y))) + ((cong g) , (embg (snd x) (snd y)))) + ∙ₑ ΣPathP≃PathPΣ) .snd + + emb : isEmbedding (map-× f g) + emb x y = equiv x y + +EmbeddingΣProp : {A : Type ℓ} → {B : A → Type ℓ'} → (∀ a → isProp (B a)) → Σ A B ↪ A +EmbeddingΣProp f = fst , (λ _ _ → isEmbeddingFstΣProp f) diff --git a/Cubical/Functions/Surjection.agda b/Cubical/Functions/Surjection.agda index 664c48a61c..40f25e5c7f 100644 --- a/Cubical/Functions/Surjection.agda +++ b/Cubical/Functions/Surjection.agda @@ -2,13 +2,18 @@ module Cubical.Functions.Surjection where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Powerset open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv open import Cubical.Foundations.Univalence open import Cubical.Foundations.Function open import Cubical.Functions.Embedding +open import Cubical.Functions.Fixpoint +open import Cubical.Relation.Nullary + +open import Cubical.Data.Empty open import Cubical.Data.Sigma open import Cubical.Data.Unit open import Cubical.HITs.PropositionalTruncation as PT @@ -91,3 +96,29 @@ compSurjection (f , sur-f) (g , sur-g) = λ c → PT.rec isPropPropTrunc (λ (b , gb≡c) → PT.rec isPropPropTrunc (λ (a , fa≡b) → ∣ a , (cong g fa≡b ∙ gb≡c) ∣₁) (sur-f b)) (sur-g c) + +-- Lawvere's fixed point theorem +↠Fixpoint : ∀ {A : Type ℓ} {B : Type ℓ'} + → (A ↠ (A → B)) + → (n : B → B) + → ∥ Fixpoint n ∥₁ +↠Fixpoint {A = A} {B = B} (f , surf) n + = map (λ (a , fib) → g a , sym (cong n (funExt⁻ fib a))) (surf g) + where g : A → B + g a = n ( f a a ) + +-- Cantor's theorem, that no type surjects into its power set +¬Surjection-into-Powerset : ∀ {A : Type ℓ} → ¬ (A ↠ ℙ A) +¬Surjection-into-Powerset {A = A} (f , surf) + = PT.rec isProp⊥ (λ (_ , fx≡g) → H₁ fx≡g (H₂ fx≡g (H₁ fx≡g))) (surf g) + where _∉_ : ∀ {A} → A → ℙ A → Type ℓ + x ∉ A = ¬ (x ∈ A) + + g : ℙ A + g = λ x → (x ∉ f x , isProp¬ _) + + H₁ : {x : A} → f x ≡ g → x ∉ (f x) + H₁ {x} fx≡g x∈fx = transport (cong (fst ∘ (_$ x)) fx≡g) x∈fx x∈fx + + H₂ : {x : A} → f x ≡ g → x ∉ (f x) → x ∈ (f x) + H₂ {x} fx≡g x∈g = transport (cong (fst ∘ (_$ x)) (sym fx≡g)) x∈g diff --git a/Cubical/HITs/SetTruncation/Properties.agda b/Cubical/HITs/SetTruncation/Properties.agda index 31c11082d3..dfbf5c7943 100644 --- a/Cubical/HITs/SetTruncation/Properties.agda +++ b/Cubical/HITs/SetTruncation/Properties.agda @@ -79,6 +79,13 @@ elim3 : {B : (x y z : ∥ A ∥₂) → Type ℓ} 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) + -- the recursor for maps into groupoids following the "HIT proof" in: -- https://arxiv.org/abs/1507.01150 diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda index 39f9bfc89d..68bb8f5d55 100644 --- a/Cubical/Relation/Binary/Base.agda +++ b/Cubical/Relation/Binary/Base.agda @@ -8,9 +8,16 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Fiberwise +open import Cubical.Functions.Embedding +open import Cubical.Functions.Logic using (_⊔′_) + +open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Sigma +open import Cubical.Data.Sum.Base as ⊎ open import Cubical.HITs.SetQuotients.Base -open import Cubical.HITs.PropositionalTruncation.Base +open import Cubical.HITs.PropositionalTruncation as ∥₁ + +open import Cubical.Relation.Nullary.Base private variable @@ -47,14 +54,74 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where isRefl : Type (ℓ-max ℓ ℓ') isRefl = (a : A) → R a a + isIrrefl : Type (ℓ-max ℓ ℓ') + isIrrefl = (a : A) → ¬ R a a + isSym : Type (ℓ-max ℓ ℓ') isSym = (a b : A) → R a b → R b a + isAsym : Type (ℓ-max ℓ ℓ') + isAsym = (a b : A) → R a b → ¬ R b a + isAntisym : Type (ℓ-max ℓ ℓ') isAntisym = (a b : A) → R a b → R b a → a ≡ b isTrans : Type (ℓ-max ℓ ℓ') - isTrans = (a b c : A) → R a b → R b c → R a c + isTrans = (a b c : A) → R a b → R b c → R a c + + -- Sum types don't play nicely with props, so we truncate + isCotrans : Type (ℓ-max ℓ ℓ') + isCotrans = (a b c : A) → R a b → (R a c ⊔′ R b c) + + isWeaklyLinear : Type (ℓ-max ℓ ℓ') + isWeaklyLinear = (a b c : A) → R a b → R a c ⊔′ R c b + + isConnected : Type (ℓ-max ℓ ℓ') + isConnected = (a b : A) → ¬ (a ≡ b) → R a b ⊔′ R b a + + isStronglyConnected : Type (ℓ-max ℓ ℓ') + isStronglyConnected = (a b : A) → R a b ⊔′ R b a + + isStronglyConnected→isConnected : isStronglyConnected → isConnected + isStronglyConnected→isConnected strong a b _ = strong a b + + isIrrefl×isTrans→isAsym : isIrrefl × isTrans → isAsym + isIrrefl×isTrans→isAsym (irrefl , trans) a₀ a₁ Ra₀a₁ Ra₁a₀ + = irrefl a₀ (trans a₀ a₁ a₀ Ra₀a₁ Ra₁a₀) + + IrreflKernel : Rel A A (ℓ-max ℓ ℓ') + IrreflKernel a b = R a b × (¬ a ≡ b) + + ReflClosure : Rel A A (ℓ-max ℓ ℓ') + ReflClosure a b = R a b ⊎ (a ≡ b) + + SymKernel : Rel A A ℓ' + SymKernel a b = R a b × R b a + + SymClosure : Rel A A ℓ' + SymClosure a b = R a b ⊎ R b a + + AsymKernel : Rel A A ℓ' + AsymKernel a b = R a b × (¬ R b a) + + NegationRel : Rel A A ℓ' + NegationRel a b = ¬ (R a b) + + module _ + {ℓ'' : Level} + (P : Embedding A ℓ'') + + where + + private + subtype : Type ℓ'' + subtype = (fst P) + + toA : subtype → A + toA = fst (snd P) + + InducedRelation : Rel subtype subtype ℓ' + InducedRelation a b = R (toA a) (toA b) record isEquivRel : Type (ℓ-max ℓ ℓ') where constructor equivRel @@ -155,3 +222,27 @@ Iso.rightInv (RelIso→Iso _ _ uni uni' f) a' = uni' (RelIso.rightInv f a') Iso.leftInv (RelIso→Iso _ _ uni uni' f) a = uni (RelIso.leftInv f a) + +isIrreflIrreflKernel : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isIrrefl (IrreflKernel R) +isIrreflIrreflKernel _ _ (_ , ¬a≡a) = ¬a≡a refl + +isReflReflClosure : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isRefl (ReflClosure R) +isReflReflClosure _ _ = inr refl + +isConnectedStronglyConnectedIrreflKernel : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') + → isStronglyConnected R + → isConnected (IrreflKernel R) +isConnectedStronglyConnectedIrreflKernel R strong a b ¬a≡b + = ∥₁.map (λ x → ⊎.rec (λ Rab → inl (Rab , ¬a≡b)) + (λ Rba → inr (Rba , (λ b≡a → ¬a≡b (sym b≡a)))) x) + (strong a b) + +isSymSymKernel : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isSym (SymKernel R) +isSymSymKernel _ _ _ (Rab , Rba) = Rba , Rab + +isSymSymClosure : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isSym (SymClosure R) +isSymSymClosure _ _ _ (inl Rab) = inr Rab +isSymSymClosure _ _ _ (inr Rba) = inl Rba + +isAsymAsymKernel : ∀ {ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isAsym (AsymKernel R) +isAsymAsymKernel _ _ _ (Rab , _) (_ , ¬Rab) = ¬Rab Rab diff --git a/Cubical/Relation/Binary/Order.agda b/Cubical/Relation/Binary/Order.agda new file mode 100644 index 0000000000..9c15bb7931 --- /dev/null +++ b/Cubical/Relation/Binary/Order.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --safe #-} +module Cubical.Relation.Binary.Order where + +open import Cubical.Relation.Binary.Order.Apartness public +open import Cubical.Relation.Binary.Order.Preorder public +open import Cubical.Relation.Binary.Order.Poset public +open import Cubical.Relation.Binary.Order.Toset public +open import Cubical.Relation.Binary.Order.StrictPoset public +open import Cubical.Relation.Binary.Order.Loset public +open import Cubical.Relation.Binary.Order.Properties public diff --git a/Cubical/Relation/Binary/Order/Apartness.agda b/Cubical/Relation/Binary/Order/Apartness.agda new file mode 100644 index 0000000000..9d8a3c62fa --- /dev/null +++ b/Cubical/Relation/Binary/Order/Apartness.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} +module Cubical.Relation.Binary.Order.Apartness where + +open import Cubical.Relation.Binary.Order.Apartness.Base public +open import Cubical.Relation.Binary.Order.Apartness.Properties public diff --git a/Cubical/Relation/Binary/Order/Apartness/Base.agda b/Cubical/Relation/Binary/Order/Apartness/Base.agda new file mode 100644 index 0000000000..35dc95528f --- /dev/null +++ b/Cubical/Relation/Binary/Order/Apartness/Base.agda @@ -0,0 +1,130 @@ +{-# OPTIONS --safe #-} +{- + An apartness relation is a relation that distinguishes + elements which are different from each other +-} +module Cubical.Relation.Binary.Order.Apartness.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +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.Data.Sigma +open import Cubical.Data.Sum + +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.Nullary + +open import Cubical.HITs.PropositionalTruncation + +open Iso +open BinaryRelation + + +private + variable + ℓ ℓ' ℓ'' ℓ₀ ℓ₀' ℓ₁ ℓ₁' : Level + +record IsApartness {A : Type ℓ} (_#_ : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where + no-eta-equality + constructor isapartness + + field + is-set : isSet A + is-prop-valued : isPropValued _#_ + is-irrefl : isIrrefl _#_ + is-cotrans : isCotrans _#_ + is-sym : isSym _#_ + +unquoteDecl IsApartnessIsoΣ = declareRecordIsoΣ IsApartnessIsoΣ (quote IsApartness) + + +record ApartnessStr (ℓ' : Level) (A : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where + + constructor apartnessstr + + field + _#_ : A → A → Type ℓ' + isApartness : IsApartness _#_ + + infixl 7 _#_ + + open IsApartness isApartness public + +Apartness : ∀ ℓ ℓ' → Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) +Apartness ℓ ℓ' = TypeWithStr ℓ (ApartnessStr ℓ') + +apartness : (A : Type ℓ) (_#_ : A → A → Type ℓ') (h : IsApartness _#_) → Apartness ℓ ℓ' +apartness A _#_ h = A , apartnessstr _#_ h + +record IsApartnessEquiv {A : Type ℓ₀} {B : Type ℓ₁} + (M : ApartnessStr ℓ₀' A) (e : A ≃ B) (N : ApartnessStr ℓ₁' B) + : Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁') + where + constructor + isapartnessequiv + -- Shorter qualified names + private + module M = ApartnessStr M + module N = ApartnessStr N + + field + pres# : (x y : A) → x M.# y ≃ equivFun e x N.# equivFun e y + + +ApartnessEquiv : (M : Apartness ℓ₀ ℓ₀') (M : Apartness ℓ₁ ℓ₁') → Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁')) +ApartnessEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsApartnessEquiv (M .snd) e (N .snd) + +isPropIsApartness : {A : Type ℓ} (_#_ : A → A → Type ℓ') → isProp (IsApartness _#_) +isPropIsApartness _#_ = isOfHLevelRetractFromIso 1 IsApartnessIsoΣ + (isPropΣ isPropIsSet + λ isSetA → isPropΣ (isPropΠ2 (λ _ _ → isPropIsProp)) + λ isPropValued# → isProp×2 + (isPropΠ λ _ → isProp¬ _) + (isPropΠ4 λ _ _ _ _ → squash₁) + (isPropΠ3 λ _ _ _ → isPropValued# _ _)) + +𝒮ᴰ-Apartness : DUARel (𝒮-Univ ℓ) (ApartnessStr ℓ') (ℓ-max ℓ ℓ') +𝒮ᴰ-Apartness = + 𝒮ᴰ-Record (𝒮-Univ _) IsApartnessEquiv + (fields: + data[ _#_ ∣ autoDUARel _ _ ∣ pres# ] + prop[ isApartness ∣ (λ _ _ → isPropIsApartness _) ]) + where + open ApartnessStr + open IsApartness + open IsApartnessEquiv + +ApartnessPath : (M N : Apartness ℓ ℓ') → ApartnessEquiv M N ≃ (M ≡ N) +ApartnessPath = ∫ 𝒮ᴰ-Apartness .UARel.ua + +-- an easier way of establishing an equivalence of apartness relations +module _ {P : Apartness ℓ₀ ℓ₀'} {S : Apartness ℓ₁ ℓ₁'} (e : ⟨ P ⟩ ≃ ⟨ S ⟩) where + private + module P = ApartnessStr (P .snd) + module S = ApartnessStr (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 IsApartnessEquiv + open IsApartness + + makeIsApartnessEquiv : IsApartnessEquiv (P .snd) e (S .snd) + pres# makeIsApartnessEquiv x y = propBiimpl→Equiv (P.isApartness .is-prop-valued _ _) + (S.isApartness .is-prop-valued _ _) + (isMon _ _) (isMonInv' _ _) + where + isMonInv' : ∀ x y → equivFun e x S.# equivFun e y → x P.# y + isMonInv' x y ex#ey = transport (λ i → retEq e x i P.# retEq e y i) (isMonInv _ _ ex#ey) diff --git a/Cubical/Relation/Binary/Order/Apartness/Properties.agda b/Cubical/Relation/Binary/Order/Apartness/Properties.agda new file mode 100644 index 0000000000..77f24ce04f --- /dev/null +++ b/Cubical/Relation/Binary/Order/Apartness/Properties.agda @@ -0,0 +1,53 @@ +{-# OPTIONS --safe #-} +module Cubical.Relation.Binary.Order.Apartness.Properties where + +open import Cubical.Foundations.Prelude + +open import Cubical.Functions.Embedding + +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Sum as ⊎ + +open import Cubical.Relation.Binary.Base +open import Cubical.Relation.Binary.Order.Apartness.Base + +open import Cubical.HITs.PropositionalTruncation as ∥₁ + +open import Cubical.Relation.Nullary + +private + variable + ℓ ℓ' ℓ'' : Level + +open BinaryRelation + +isApartness→ImpliesInequality : {A : Type ℓ} {_#_ : Rel A A ℓ'} + → IsApartness _#_ → ∀ x y → x # y → ¬ (x ≡ y) +isApartness→ImpliesInequality {_#_ = _#_} apart x y x#y x≡y + = IsApartness.is-irrefl apart y (subst (λ a → a # y) x≡y x#y) + +isApartness→isEquivRelNegationRel : {A : Type ℓ} {_#_ : Rel A A ℓ'} + → IsApartness _#_ → isEquivRel (NegationRel _#_) +isApartness→isEquivRelNegationRel apart + = equivRel (λ a a#a → IsApartness.is-irrefl apart a a#a) + (λ a b ¬a#b b#a → ¬a#b (IsApartness.is-sym apart b a b#a)) + λ a b c ¬a#b ¬b#c a#c + → ∥₁.rec isProp⊥ (⊎.rec ¬a#b + (λ c#b → ¬b#c (IsApartness.is-sym apart c b c#b))) + (IsApartness.is-cotrans apart a c b a#c) + +module _ + {A : Type ℓ} + {R : Rel A A ℓ'} + where + + open BinaryRelation + + isApartnessInduced : IsApartness R → (B : Type ℓ'') → (f : B ↪ A) + → IsApartness (InducedRelation R (B , f)) + isApartnessInduced apa B (f , emb) + = isapartness (Embedding-into-isSet→isSet (f , emb) (IsApartness.is-set apa)) + (λ a b → IsApartness.is-prop-valued apa (f a) (f b)) + (λ a → IsApartness.is-irrefl apa (f a)) + (λ a b c → IsApartness.is-cotrans apa (f a) (f b) (f c)) + λ a b → IsApartness.is-sym apa (f a) (f b) diff --git a/Cubical/Relation/Binary/Order/Loset.agda b/Cubical/Relation/Binary/Order/Loset.agda new file mode 100644 index 0000000000..03419a5a7e --- /dev/null +++ b/Cubical/Relation/Binary/Order/Loset.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe #-} +module Cubical.Relation.Binary.Order.Loset where + +open import Cubical.Relation.Binary.Order.Loset.Base public +open import Cubical.Relation.Binary.Order.Loset.Properties public diff --git a/Cubical/Relation/Binary/Order/Loset/Base.agda b/Cubical/Relation/Binary/Order/Loset/Base.agda new file mode 100644 index 0000000000..0f2d3bd941 --- /dev/null +++ b/Cubical/Relation/Binary/Order/Loset/Base.agda @@ -0,0 +1,134 @@ +{-# OPTIONS --safe #-} +{- + Losets are linearly-ordered sets, + i.e. strict posets that are also weakly linear + and connected, or more plainly a strict poset + where every element can be compared +-} +module Cubical.Relation.Binary.Order.Loset.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +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.Data.Sigma + +open import Cubical.HITs.PropositionalTruncation + +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.Nullary.Properties + +open Iso +open BinaryRelation + + +private + variable + ℓ ℓ' ℓ'' ℓ₀ ℓ₀' ℓ₁ ℓ₁' : Level + +record IsLoset {A : Type ℓ} (_<_ : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where + no-eta-equality + constructor isloset + + field + is-set : isSet A + is-prop-valued : isPropValued _<_ + is-irrefl : isIrrefl _<_ + is-trans : isTrans _<_ + is-asym : isAsym _<_ + is-weakly-linear : isWeaklyLinear _<_ + is-connected : isConnected _<_ + +unquoteDecl IsLosetIsoΣ = declareRecordIsoΣ IsLosetIsoΣ (quote IsLoset) + + +record LosetStr (ℓ' : Level) (A : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where + + constructor losetstr + + field + _<_ : A → A → Type ℓ' + isLoset : IsLoset _<_ + + infixl 7 _<_ + + open IsLoset isLoset public + +Loset : ∀ ℓ ℓ' → Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) +Loset ℓ ℓ' = TypeWithStr ℓ (LosetStr ℓ') + +loset : (A : Type ℓ) (_<_ : A → A → Type ℓ') (h : IsLoset _<_) → Loset ℓ ℓ' +loset A _<_ h = A , losetstr _<_ h + +record IsLosetEquiv {A : Type ℓ₀} {B : Type ℓ₁} + (M : LosetStr ℓ₀' A) (e : A ≃ B) (N : LosetStr ℓ₁' B) + : Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁') + where + constructor + islosetequiv + -- Shorter qualified names + private + module M = LosetStr M + module N = LosetStr N + + field + pres< : (x y : A) → x M.< y ≃ equivFun e x N.< equivFun e y + + +LosetEquiv : (M : Loset ℓ₀ ℓ₀') (M : Loset ℓ₁ ℓ₁') → Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁')) +LosetEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsLosetEquiv (M .snd) e (N .snd) + +isPropIsLoset : {A : Type ℓ} (_<_ : A → A → Type ℓ') → isProp (IsLoset _<_) +isPropIsLoset _<_ = isOfHLevelRetractFromIso 1 IsLosetIsoΣ + (isPropΣ isPropIsSet + λ isSetA → isPropΣ (isPropΠ2 (λ _ _ → isPropIsProp)) + λ isPropValued< → isProp×4 (isPropΠ (λ x → isProp¬ (x < x))) + (isPropΠ5 (λ _ _ _ _ _ → isPropValued< _ _)) + (isPropΠ3 (λ x y _ → isProp¬ (y < x))) + (isPropΠ4 λ _ _ _ _ → squash₁) + (isPropΠ3 λ _ _ _ → squash₁)) + +𝒮ᴰ-Loset : DUARel (𝒮-Univ ℓ) (LosetStr ℓ') (ℓ-max ℓ ℓ') +𝒮ᴰ-Loset = + 𝒮ᴰ-Record (𝒮-Univ _) IsLosetEquiv + (fields: + data[ _<_ ∣ autoDUARel _ _ ∣ pres< ] + prop[ isLoset ∣ (λ _ _ → isPropIsLoset _) ]) + where + open LosetStr + open IsLoset + open IsLosetEquiv + +LosetPath : (M N : Loset ℓ ℓ') → LosetEquiv M N ≃ (M ≡ N) +LosetPath = ∫ 𝒮ᴰ-Loset .UARel.ua + +-- an easier way of establishing an equivalence of losets +module _ {P : Loset ℓ₀ ℓ₀'} {S : Loset ℓ₁ ℓ₁'} (e : ⟨ P ⟩ ≃ ⟨ S ⟩) where + private + module P = LosetStr (P .snd) + module S = LosetStr (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 IsLosetEquiv + open IsLoset + + makeIsLosetEquiv : IsLosetEquiv (P .snd) e (S .snd) + pres< makeIsLosetEquiv x y = propBiimpl→Equiv (P.isLoset .is-prop-valued _ _) + (S.isLoset .is-prop-valued _ _) + (isMon _ _) (isMonInv' _ _) + where + isMonInv' : ∀ x y → equivFun e x S.< equivFun e y → x P.< y + isMonInv' x y ex