diff --git a/Cubical/Algebra/CommMonoid/Properties.agda b/Cubical/Algebra/CommMonoid/Properties.agda index 4926c3dc0b..c6e7ec1b9e 100644 --- a/Cubical/Algebra/CommMonoid/Properties.agda +++ b/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 diff --git a/Cubical/Algebra/DistLattice/Downset.agda b/Cubical/Algebra/DistLattice/Downset.agda index 907c419732..3c52245edf 100644 --- a/Cubical/Algebra/DistLattice/Downset.agda +++ b/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 diff --git a/Cubical/Algebra/Monoid/Base.agda b/Cubical/Algebra/Monoid/Base.agda index dbf68fb538..27491a8937 100644 --- a/Cubical/Algebra/Monoid/Base.agda +++ b/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) diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda index f2dc3d1f52..5427849bf4 100644 --- a/Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda +++ b/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 diff --git a/Cubical/Categories/Constructions/SubObject.agda b/Cubical/Categories/Constructions/SubObject.agda index 2a5040bd49..2e94416488 100644 --- a/Cubical/Categories/Constructions/SubObject.agda +++ b/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 diff --git a/Cubical/Data/Cardinal/Properties.agda b/Cubical/Data/Cardinal/Properties.agda index 1c7371cf0c..d4041dafed 100644 --- a/Cubical/Data/Cardinal/Properties.agda +++ b/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)) diff --git a/Cubical/Data/Ordinal/Properties.agda b/Cubical/Data/Ordinal/Properties.agda index 0cfbd9d98c..f4ea61dd03 100644 --- a/Cubical/Data/Ordinal/Properties.agda +++ b/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 diff --git a/Cubical/Data/Rationals/Order.agda b/Cubical/Data/Rationals/Order.agda index a18910dbec..0136e99319 100644 --- a/Cubical/Data/Rationals/Order.agda +++ b/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