Basic Order Theory (agda#1154)

* Add inverses to monoids/comm monoids

* Add meets and joins to order properties

* Rewrite isConnected and rename isStronglyConnected

* Decidable total and linear orders imply discrete

* Remove discrete requirement

* Move decidable->discrete from toset to poset

* Define binary meets/joins and prove properties

* The negation of a linear order is a poset

* Define bounds on a poset

* Mild refactoring

Rename preorder to proset; rename strict poset
to quoset (quasiorder) and add strict orders
as quasiorders with weak linearity

* Remove unnecessary constructors

* Define tight relations

* Reintroduce constructors

* Lattice basics

* Distributive lattices

* Replace compEquiv usages

* Total orders are distributive pseudolattices

* Add pseudolattice assumption to make more useful

* Mappings on posets

* Downsets and upsets are preserved

* Defined complete lattices

* Duals and closures

* Embeddings form a complete lattice

* Dual closures

* Bicomplete subsets

* Poset equivalences

* Galois connections

* Fix typo

* Fix whitespace

* Fix build failures

* Move PosetDownset to where principalDownsets are

* Fix build failures

* Split mappings and subsets

* Fix whitespace

* Proofs regarding residuals and involutions

* Cleaner proof

Author: LuuBluum

Cubical/Algebra/CommMonoid/Properties.agda

@@ -57,3 +57,19 @@ module CommMonoidTheory (M' : CommMonoid ℓ) where
  commAssocSwap : (x y z w : M) → (x · y) · (z · w) ≡ (x · z) · (y · w)
  commAssocSwap x y z w = ·Assoc (x · y) z w ∙∙ cong (_· w) (commAssocr x y z)
                                                ∙∙ sym (·Assoc (x · z) y w)
+
+ hasInverse : (x : M) → Type ℓ
+ hasInverse x = Σ[ -x ∈ M ] -x · x ≡ ε
+
+ isPropHasInverse : ∀ x → isProp (hasInverse x)
+ isPropHasInverse x yinv zinv
+   = Σ≡Prop (λ a → is-set (a · x) ε)
+    (PathPΣ (MonoidTheory.isPropHasInverse (CommMonoid→Monoid M') x
+                                           (hasInverseToMonoid x yinv)
+                                           (hasInverseToMonoid x zinv))
+                                               .fst)
+   where
+     hasInverseToMonoid : ∀ x
+                        → hasInverse x
+                        → MonoidTheory.hasInverse (CommMonoid→Monoid M') x
+     hasInverseToMonoid x (y , yinv) = y , yinv , ·Comm x y ∙ yinv

Cubical/Algebra/DistLattice/Downset.agda

@@ -16,6 +16,7 @@ open import Cubical.Algebra.Lattice
 open import Cubical.Algebra.DistLattice.Base
 
 open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Poset.Subset
 
 open Iso
 

Cubical/Algebra/Monoid/Base.agda

@@ -140,3 +140,13 @@ module MonoidTheory {ℓ} (M : Monoid ℓ) where
     (y · x) · z ≡⟨ congL _·_ left-inverse ⟩
     ε · z       ≡⟨ ·IdL z ⟩
     z ∎
+
+  -- Added for its use in division rings
+  hasInverse : (x : ⟨ M ⟩) → Type ℓ
+  hasInverse x = Σ[ -x ∈ ⟨ M ⟩ ] (-x · x ≡ ε) × (x · -x ≡ ε)
+
+  isPropHasInverse : ∀ x → isProp (hasInverse x)
+  isPropHasInverse x (y , invly , _) (z , _ , invrz)
+    = Σ≡Prop (λ a → isProp× (is-set (a · x) ε)
+                             (is-set (x · a) ε))
+              (inv-lemma x y z invly invrz)

Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda

@@ -13,6 +13,7 @@ open import Cubical.Data.Nat using (ℕ)
 open import Cubical.Data.Sigma.Properties
 open import Cubical.Data.FinData
 open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Poset.Subset
 
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.Localisation

Cubical/Categories/Constructions/SubObject.agda

@@ -11,7 +11,7 @@ open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Morphism
 
-open import Cubical.Relation.Binary.Order.Preorder
+open import Cubical.Relation.Binary.Order.Proset
 
 open Category
 
@@ -83,9 +83,9 @@ SliceHom.S-comm
     ∎
 
 module _ (isSetCOb : isSet (C .ob)) where
-  subObjCatPreorderStr : PreorderStr _ (SubObjCat .ob)
-  PreorderStr._≲_ subObjCatPreorderStr x y = SubObjCat [ x , y ]
-  IsPreorder.is-set (PreorderStr.isPreorder subObjCatPreorderStr) = isSetΣ (isSetSliceOb isSetCOb) λ x → isProp→isSet (∈-isProp isSubObj x)
-  IsPreorder.is-prop-valued (PreorderStr.isPreorder subObjCatPreorderStr) = isPropSubObjMor
-  IsPreorder.is-refl (PreorderStr.isPreorder subObjCatPreorderStr) = isReflSubObjMor
-  IsPreorder.is-trans (PreorderStr.isPreorder subObjCatPreorderStr) = isTransSubObjMor
+  subObjCatPreorderStr : ProsetStr _ (SubObjCat .ob)
+  ProsetStr._≲_ subObjCatPreorderStr x y = SubObjCat [ x , y ]
+  IsProset.is-set (ProsetStr.isProset subObjCatPreorderStr) = isSetΣ (isSetSliceOb isSetCOb) λ x → isProp→isSet (∈-isProp isSubObj x)
+  IsProset.is-prop-valued (ProsetStr.isProset subObjCatPreorderStr) = isPropSubObjMor
+  IsProset.is-refl (ProsetStr.isProset subObjCatPreorderStr) = isReflSubObjMor
+  IsProset.is-trans (ProsetStr.isProset subObjCatPreorderStr) = isTransSubObjMor

Cubical/Data/Cardinal/Properties.agda

@@ -25,8 +25,7 @@ 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
+open import Cubical.Relation.Binary.Order.Proset
 
 private
   variable
@@ -171,9 +170,9 @@ module _ where
              λ (A , _) (B , _) (C , _)
                → ∥₁.map2 λ A↪B B↪C → compEmbedding B↪C A↪B
 
-  isPreorder≲ : IsPreorder {ℓ-suc ℓ} _≲_
+  isPreorder≲ : IsProset {ℓ-suc ℓ} _≲_
   isPreorder≲
-    = ispreorder isSetCard isPropValued≲ isRefl≲ isTrans≲
+    = isproset isSetCard isPropValued≲ isRefl≲ isTrans≲
 
 isLeast𝟘 : ∀{ℓ} → isLeast isPreorder≲ (Card {ℓ} , id↪ (Card {ℓ})) (𝟘 {ℓ})
 isLeast𝟘 = ∥₂.elim (λ x → isProp→isSet (isPropValued≲ 𝟘 x))

Cubical/Data/Ordinal/Properties.agda

@@ -60,7 +60,7 @@ propOrd {ℓ} P prop = P , (wosetstr _<_ (iswoset set prp well weak trans))
 𝟘 {ℓ} = propOrd (⊥* {ℓ}) (isProp⊥*)
 𝟙 {ℓ} = propOrd (Unit* {ℓ}) (isPropUnit*)
 
-isLeast𝟘 : ∀{ℓ} → isLeast (isPoset→isPreorder isPoset≼) ((Ord {ℓ}) , (id↪ (Ord {ℓ}))) (𝟘 {ℓ})
+isLeast𝟘 : ∀{ℓ} → isLeast (isPoset→isProset isPoset≼) ((Ord {ℓ}) , (id↪ (Ord {ℓ}))) (𝟘 {ℓ})
 isLeast𝟘 _ = ⊥.elim* , (⊥.elim* , ⊥.elim*)
 
 -- The successor of 𝟘 is 𝟙
@@ -144,8 +144,8 @@ suc≺ α = (inr tt*) , (eq , makeIsWosetEquiv eq eqsucα eqαsuc)
     eq = isoToEquiv rUnit*×Iso
 
     eqα𝟙 : _
-    eqα𝟙 (x , _) (y , _) (inl tt≺tt) = ⊥.rec (IsStrictPoset.is-irrefl
-                                                (isWoset→isStrictPoset
+    eqα𝟙 (x , _) (y , _) (inl tt≺tt) = ⊥.rec (IsQuoset.is-irrefl
+                                                (isWoset→isQuoset
                                                    (WosetStr.isWoset (str 𝟙)))
                                                tt* tt≺tt)
     eqα𝟙 (x , _) (y , _) (inr (_ , x≺y)) = x≺y
@@ -161,8 +161,8 @@ suc≺ α = (inr tt*) , (eq , makeIsWosetEquiv eq eqsucα eqαsuc)
 
     eq𝟙α : _
     eq𝟙α (_ , x) (_ , y) (inr (_ , tt≺tt)) = ⊥.rec
-                                               (IsStrictPoset.is-irrefl
-                                                (isWoset→isStrictPoset
+                                               (IsQuoset.is-irrefl
+                                                (isWoset→isQuoset
                                                   (WosetStr.isWoset (str 𝟙)))
                                                 tt* tt≺tt)
     eq𝟙α (_ , x) (_ , y) (inl x≺y) = x≺y

Cubical/Data/Rationals/Order.agda

@@ -216,8 +216,8 @@ module _ where
   isAsym< : isAsym _<_
   isAsym< = isIrrefl×isTrans→isAsym _<_ (isIrrefl< , isTrans<)
 
-  isStronglyConnected≤ : isStronglyConnected _≤_
-  isStronglyConnected≤ =
+  isTotal≤ : isTotal _≤_
+  isTotal≤ =
     elimProp2 {P = λ a b → (a ≤ b) ⊔′ (b ≤ a)}
               (λ _ _ → isPropPropTrunc)
                λ a b → ∣ lem a b ∣₁
@@ -230,12 +230,34 @@ module _ where
 
   isConnected< : isConnected _<_
   isConnected< =
-    elimProp2 {P = λ a b → ¬ a ≡ b → (a < b) ⊔′ (b < a)}
-              (λ _ _ → isProp→ isPropPropTrunc)
-               λ a b ¬a≡b → ∣ lem a b ¬a≡b ∣₁
+    elimProp2 {P = λ a b → (¬ a < b) × (¬ b < a) → a ≡ b}
+              (λ a b → isProp→ (isSetℚ a b))
+               lem
     where
-      -- Agda can't infer the relation involved, so the signature looks a bit weird here
-      lem : (a b : ℤ.ℤ × ℕ₊₁) → ¬ [_] {R = _∼_} a ≡ [ b ] → ([ a ] < [ b ]) ⊎ ([ b ] < [ a ])
+      lem : (a b : ℤ.ℤ × ℕ₊₁) → (¬ [ a ] < [ b ]) × (¬ [ b ] < [ a ]) → [ a ] ≡ [ b ]
+      lem (a , b) (c , d) (¬ad<cb , ¬cb<ad) with (a ℤ.· ℕ₊₁→ℤ d) ℤ.≟ (c ℤ.· ℕ₊₁→ℤ b)
+      ... | ℤ.lt ad<cb = ⊥.rec (¬ad<cb ad<cb)
+      ... | ℤ.eq ad≡cb = eq/ (a , b) (c , d) ad≡cb
+      ... | ℤ.gt cb<ad = ⊥.rec (¬cb<ad cb<ad)
+
+  isProp# : isPropValued _#_
+  isProp# x y = isProp⊎ (isProp< x y) (isProp< y x) (isAsym< x y)
+
+  isIrrefl# : isIrrefl _#_
+  isIrrefl# x (inl x<x) = isIrrefl< x x<x
+  isIrrefl# x (inr x<x) = isIrrefl< x x<x
+
+  isSym# : isSym _#_
+  isSym# _ _ (inl x<y) = inr x<y
+  isSym# _ _ (inr y<x) = inl y<x
+
+  inequalityImplies# : inequalityImplies _#_
+  inequalityImplies#
+    = elimProp2 {P = λ a b → ¬ a ≡ b → a # b}
+                (λ a b → isProp→ (isProp# a b))
+                 lem
+    where
+      lem : (a b : ℤ.ℤ × ℕ₊₁) → ¬ [_] {R = _∼_} a ≡ [ b ] → [ a ] # [ b ]
       lem (a , b) (c , d) ¬a≡b with (a ℤ.· ℕ₊₁→ℤ d) ℤ.≟ (c ℤ.· ℕ₊₁→ℤ b)
       ... | ℤ.lt ad<cb = inl ad<cb
       ... | ℤ.eq ad≡cb = ⊥.rec (¬a≡b (eq/ (a , b) (c , d) ad≡cb))
@@ -250,20 +272,9 @@ module _ where
       lem : (a b c : ℤ.ℤ × ℕ₊₁) → [ a ] < [ b ] → ([ a ] < [ c ]) ⊔′ ([ c ] < [ b ])
       lem a b c a<b with discreteℚ [ a ] [ c ]
       ... | yes a≡c = ∣ inr (subst (_< [ b ]) a≡c a<b) ∣₁
-      ... | no a≢c = ∥₁.map (⊎.map (λ a<c → a<c)
-                                    (λ c<a → isTrans< [ c ] [ a ] [ b ] c<a a<b))
-                             (isConnected< [ a ] [ c ] a≢c)
-
-  isProp# : isPropValued _#_
-  isProp# x y = isProp⊎ (isProp< x y) (isProp< y x) (isAsym< x y)
-
-  isIrrefl# : isIrrefl _#_
-  isIrrefl# x (inl x<x) = isIrrefl< x x<x
-  isIrrefl# x (inr x<x) = isIrrefl< x x<x
-
-  isSym# : isSym _#_
-  isSym# _ _ (inl x<y) = inr x<y
-  isSym# _ _ (inr y<x) = inl y<x
+      ... | no a≢c = ∣ ⊎.map (λ a<c → a<c)
+                             (λ c<a → isTrans< [ c ] [ a ] [ b ] c<a a<b)
+                             (inequalityImplies# [ a ] [ c ] a≢c) ∣₁
 
   isCotrans# : isCotrans _#_
   isCotrans#
@@ -274,10 +285,7 @@ module _ where
         lem : (a b c : ℤ.ℤ × ℕ₊₁) → [ a ] # [ b ] → ([ a ] # [ c ]) ⊔′ ([ b ] # [ c ])
         lem a b c a#b with discreteℚ [ b ] [ c ]
         ... | yes b≡c = ∣ inl (subst ([ a ] #_) b≡c a#b) ∣₁
-        ... | no  b≢c = ∥₁.map inr (isConnected< [ b ] [ c ] b≢c)
-
-  inequalityImplies# : inequalityImplies _#_
-  inequalityImplies# a b = ∥₁.rec (isProp# a b) (λ a#b → a#b) ∘ (isConnected< a b)
+        ... | no  b≢c = ∣ inr (inequalityImplies# [ b ] [ c ] b≢c) ∣₁
 
 ≤-+o : ∀ m n o → m ≤ n → m ℚ.+ o ≤ n ℚ.+ o
 ≤-+o =
@@ -614,7 +622,7 @@ m ≟ n with discreteℚ m n
 ... | yes m≡n = ≡Weaken≤ n m (sym m≡n)
 ... | no  m≢n = ∥₁.elim (λ _ → isProp≤ n m)
                         (⊎.rec (⊥.rec ∘ m≮n) (<Weaken≤ n m))
-                        (isConnected< m n m≢n)
+                         ∣ inequalityImplies# m n m≢n ∣₁
 
 0<+ : ∀ m n → 0 < m ℚ.+ n → (0 < m) ⊎ (0 < n)
 0<+ m n 0<m+n with <Dec 0 m | <Dec 0 n

Cubical/Foundations/Transport.agda

@@ -74,6 +74,10 @@ substSubst⁻ {x = x} {y = y} B p v = transportTransport⁻ {A = B x} {B = B y}
 substEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {a a' : A} (P : A → Type ℓ') (p : a ≡ a') → P a ≃ P a'
 substEquiv P p = (subst P p , isEquivTransport (λ i → P (p i)))
 
+subst2Equiv : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {a a' : A} {b b' : B} (P : A → B → Type ℓ'')
+            (p : a ≡ a') (q : b ≡ b') → P a b ≃ P a' b'
+subst2Equiv P p q = (subst2 P p q , isEquivTransport (λ i → P (p i) (q i)))
+
 liftEquiv : ∀ {ℓ ℓ'} {A B : Type ℓ} (P : Type ℓ → Type ℓ') (e : A ≃ B) → P A ≃ P B
 liftEquiv P e = substEquiv P (ua e)
 

Cubical/Functions/Embedding.agda

@@ -15,7 +15,10 @@ open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Univalence using (ua; univalence; pathToEquiv)
 open import Cubical.Functions.Fibration
 
+open import Cubical.HITs.PropositionalTruncation.Base
+
 open import Cubical.Data.Sigma
+open import Cubical.Data.Sum.Base
 open import Cubical.Functions.Fibration
 open import Cubical.Functions.FunExtEquiv
 open import Cubical.Relation.Nullary using (Discrete; yes; no)
@@ -24,11 +27,10 @@ open import Cubical.Structures.Axioms
 open import Cubical.Reflection.StrictEquiv
 
 open import Cubical.Data.Nat using (ℕ; zero; suc)
-open import Cubical.Data.Sigma
 
 private
   variable
-    ℓ ℓ' ℓ'' : Level
+    ℓ ℓ' ℓ'' ℓ''' : Level
     A B C : Type ℓ
     f h : A → B
     w x : A
@@ -430,6 +432,14 @@ _≃Emb_ = EmbeddingIdentityPrinciple.f≃g
 EmbeddingIP : {B : Type ℓ} (f g : Embedding B ℓ') → f ≃Emb g ≃ (f ≡ g)
 EmbeddingIP = EmbeddingIdentityPrinciple.EmbeddingIP
 
+-- Using the above, we can show that the collection of embeddings forms a set
+isSetEmbedding : {B : Type ℓ} {ℓ' : Level} → isSet (Embedding B ℓ')
+isSetEmbedding M N
+  = isOfHLevelRespectEquiv 1
+      (EmbeddingIP M N)
+      (isProp× (isPropΠ2 (λ b _ → isEmbedding→hasPropFibers (N .snd .snd) b))
+               (isPropΠ2  λ b _ → isEmbedding→hasPropFibers (M .snd .snd) b))
+
 -- Cantor's theorem for sets
 Set-Embedding-into-Powerset : {A : Type ℓ} → isSet A → A ↪ ℙ A
 Set-Embedding-into-Powerset {A = A} setA
@@ -462,3 +472,65 @@ Set-Embedding-into-Powerset {A = A} setA
 
 EmbeddingΣProp : {A : Type ℓ} → {B : A → Type ℓ'} → (∀ a → isProp (B a)) → Σ A B ↪ A
 EmbeddingΣProp f = fst , (λ _ _ → isEmbeddingFstΣProp f)
+
+-- Since embeddings are equivalent to subsets, we can create some notation around this
+_∈ₑ_ : {A : Type ℓ} → A → Embedding A ℓ' → Type (ℓ-max ℓ ℓ')
+x ∈ₑ (_ , (f , _)) = fiber f x
+
+isProp∈ₑ : {A : Type ℓ} (x : A) (S : Embedding A ℓ') → isProp (x ∈ₑ S)
+isProp∈ₑ x S = isEmbedding→hasPropFibers (S .snd .snd) x
+
+_⊆ₑ_ : {A : Type ℓ} → Embedding A ℓ' → Embedding A ℓ'' → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
+X ⊆ₑ Y = ∀ x → x ∈ₑ X → x ∈ₑ Y
+
+isProp⊆ₑ : {A : Type ℓ} (X : Embedding A ℓ') (Y : Embedding A ℓ'')
+         → isProp (X ⊆ₑ Y)
+isProp⊆ₑ _ Y = isPropΠ2 λ x _ → isProp∈ₑ x Y
+
+isRefl⊆ₑ : {A : Type ℓ} → (S : Embedding A ℓ') → S ⊆ₑ S
+isRefl⊆ₑ S x x∈S = x∈S
+
+isAntisym⊆ₑ : {A : Type ℓ}
+             (X Y : Embedding A ℓ')
+            → X ⊆ₑ Y
+            → Y ⊆ₑ X
+            → X ≡ Y
+isAntisym⊆ₑ X Y X⊆Y Y⊆X = equivFun (EmbeddingIP X Y) (X⊆Y , Y⊆X)
+
+isTrans⊆ₑ : {A : Type ℓ}
+            (X : Embedding A ℓ')
+            (Y : Embedding A ℓ'')
+            (Z : Embedding A ℓ''')
+          → X ⊆ₑ Y
+          → Y ⊆ₑ Z
+          → X ⊆ₑ Z
+isTrans⊆ₑ X Y Z X⊆Y Y⊆Z x = (Y⊆Z x) ∘ (X⊆Y x)
+
+_∩ₑ_ : {A : Type ℓ}
+       (X : Embedding A ℓ')
+       (Y : Embedding A ℓ'')
+     → Embedding A (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
+_∩ₑ_ {A = A} X Y = (Σ[ x ∈ A ] x ∈ₑ X × x ∈ₑ Y) ,
+                    EmbeddingΣProp λ x → isProp× (isProp∈ₑ x X)
+                                                 (isProp∈ₑ x Y)
+
+_∪ₑ_ : {A : Type ℓ}
+       (X : Embedding A ℓ')
+       (Y : Embedding A ℓ'')
+     → Embedding A (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
+_∪ₑ_ {A = A} X Y = (Σ[ x ∈ A ] ∥ (x ∈ₑ X) ⊎ (x ∈ₑ Y) ∥₁) ,
+                    EmbeddingΣProp λ _ → squash₁
+
+⋂ₑ_ : {A : Type ℓ}
+      {I : Type ℓ'}
+      (P : I → Embedding A ℓ'')
+     → Embedding A (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
+⋂ₑ_ {A = A} P = (Σ[ x ∈ A ] (∀ i → x ∈ₑ P i)) ,
+                EmbeddingΣProp λ x → isPropΠ λ i → isProp∈ₑ x (P i)
+
+⋃ₑ_ : {A : Type ℓ}
+      {I : Type ℓ'}
+      (P : I → Embedding A ℓ'')
+    → Embedding A (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
+⋃ₑ_ {A = A} {I = I} P = (Σ[ x ∈ A ] (∃[ i ∈ I ] x ∈ₑ P i)) ,
+                        EmbeddingΣProp λ _ → squash₁

Cubical/Functions/Image.agda

@@ -30,12 +30,7 @@ module _ (f : A → B) where
   Image = Σ[ y ∈ B ] isInImage y
 
   imageInclusion : Image ↪ B
-  imageInclusion = fst ,
-    hasPropFibers→isEmbedding {f = fst}
-      λ y → isOfHLevelRetractFromIso 1 (ϕ y) isPropPropTrunc
-      where
-        ϕ : (y : B) → Iso _ _
-        ϕ y = invIso (fiberProjIso B isInImage y)
+  imageInclusion = EmbeddingΣProp isPropIsInImage
 
   restrictToImage : A → Image
   restrictToImage x = (f x) , ∣ x , refl ∣₁