From 0b8ce43ed12e14437f07097cb7b188c282c79b62 Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Thu, 2 Apr 2026 20:15:31 +0200 Subject: [PATCH 01/19] add properties of OCR and OCR-morphisms, including univalence and canonical embedding from the integers --- .../Algebra/CommRing/Instances/Fast/Int.agda | 114 +++ Cubical/Algebra/OrderedCommRing.agda | 1 + Cubical/Algebra/OrderedCommRing/Base.agda | 40 +- .../OrderedCommRing/Instances/Fast/Int.agda | 97 +++ .../Algebra/OrderedCommRing/Morphisms.agda | 360 +++++++++ .../Algebra/OrderedCommRing/Properties.agda | 683 ++++++++++++++++++ .../Algebra/OrderedCommRing/Univalence.agda | 78 ++ Cubical/Algebra/Ring/Properties.agda | 11 + 8 files changed, 1379 insertions(+), 5 deletions(-) create mode 100644 Cubical/Algebra/OrderedCommRing/Morphisms.agda create mode 100644 Cubical/Algebra/OrderedCommRing/Properties.agda create mode 100644 Cubical/Algebra/OrderedCommRing/Univalence.agda diff --git a/Cubical/Algebra/CommRing/Instances/Fast/Int.agda b/Cubical/Algebra/CommRing/Instances/Fast/Int.agda index e01dde2d62..eddd1e13e9 100644 --- a/Cubical/Algebra/CommRing/Instances/Fast/Int.agda +++ b/Cubical/Algebra/CommRing/Instances/Fast/Int.agda @@ -1,8 +1,12 @@ module Cubical.Algebra.CommRing.Instances.Fast.Int where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing + +open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc) open import Cubical.Data.Fast.Int as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_) open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing) @@ -21,3 +25,113 @@ isCommRing (snd ℤCommRing) = isCommRingℤ isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR -Cancel Int.+Comm Int.·Assoc Int.·IdR ·DistR+ Int.·Comm + +private + variable + ℓ : Level + +module CanonicalHomFromℤ (R : CommRing ℓ) where + + private + module R where + open CommRingStr (snd R) public + open RingTheory (CommRing→Ring R) public + + suc-fromℕ : ∀ x → R.fromℕ (suc x) ≡ R.1r R.+ R.fromℕ x + suc-fromℕ zero = sym (R.+IdR R.1r) + suc-fromℕ (suc x) = refl + + fromℕ-pres+ : (x y : ℕ) → R.fromℕ (x ℕ.+ y) ≡ R.fromℕ x R.+ R.fromℕ y + fromℕ-pres+ zero y = sym (R.+IdL _) + fromℕ-pres+ (suc zero) y = suc-fromℕ y + fromℕ-pres+ (suc (suc x)) y = cong (R.1r R.+_) (fromℕ-pres+ (suc x) y) ∙ R.+Assoc _ _ _ + + fromℤ-pres- : (x : ℤ) → R.fromℤ (-ℤ x) ≡ R.- R.fromℤ x + fromℤ-pres- (pos zero) = sym R.0Selfinverse + fromℤ-pres- (pos (suc n)) = refl + fromℤ-pres- (negsuc n) = sym (R.-Idempotent _) + + suc-fromℤ : ∀ z → R.fromℤ (1 +ℤ z) ≡ R.1r R.+ R.fromℤ (z) + suc-fromℤ (pos n) = suc-fromℕ n + suc-fromℤ (negsuc zero) = sym (R.+InvR R.1r) + suc-fromℤ (negsuc (suc n)) = + sym (cong (R._+ (R.- R.fromℕ (suc n))) (R.+InvR _) ∙ R.+IdL _) + ∙∙ sym (R.+Assoc _ _ _) + ∙∙ cong (R.1r R.+_) (R.-Dist _ _) + + fromℤ-pres+' : (n m : ℕ) → + R.fromℤ (pos n +ℤ negsuc m) ≡ + R.fromℤ (pos n) R.+ R.fromℤ (negsuc m) + fromℤ-pres+' zero m = sym (R.+IdL _) + fromℤ-pres+' (suc n) m = + (cong R.fromℤ (sym (+Assoc 1 (pos n) (negsuc m))) + ∙ suc-fromℤ (pos n +ℤ negsuc m)) + ∙∙ cong (R.1r R.+_) (fromℤ-pres+' n m) + ∙∙ R.+Assoc _ _ _ + ∙ cong (R._+ R.fromℤ (negsuc m)) + (sym (suc-fromℕ n)) + + fromℤ-pres+ : (x y : ℤ) → R.fromℤ (x +ℤ y) ≡ R.fromℤ x R.+ R.fromℤ y + fromℤ-pres+ (pos n) (pos m) = fromℕ-pres+ n m + fromℤ-pres+ (pos n) (negsuc m) = fromℤ-pres+' n m + fromℤ-pres+ (negsuc n) (pos m) = fromℤ-pres+' m n ∙ R.+Comm _ _ + fromℤ-pres+ (negsuc n) (negsuc m) = + cong (R.-_) + (cong (R.1r R.+_) (cong R.fromℕ (sym (ℕ.+-suc n m))) + ∙ sym (suc-fromℕ (n ℕ.+ suc m)) + ∙ fromℕ-pres+ (suc n) (suc m)) + ∙ sym (R.-Dist _ _) + + fromℕ-pres· : (x y : ℕ) → R.fromℕ (x ℕ.· y) ≡ R.fromℕ x R.· R.fromℕ y + fromℕ-pres· zero y = sym (R.0LeftAnnihilates _) + fromℕ-pres· (suc x) y = + fromℕ-pres+ y (x ℕ.· y) + ∙∙ cong₂ (R._+_) (sym (R.·IdL _)) (fromℕ-pres· x y) + ∙∙ sym (R.·DistL+ _ _ _) + ∙ cong (R._· R.fromℕ y) (sym (suc-fromℕ x)) + fromℤ-pres· : (x y : ℤ) → R.fromℤ (x ·ℤ y) ≡ R.fromℤ x R.· R.fromℤ y + fromℤ-pres· (pos n) (pos m) = fromℕ-pres· n m + fromℤ-pres· (pos n) (negsuc m) = + cong R.fromℤ (sym (-DistR· (pos n) (pos (suc m)))) + ∙∙ (fromℤ-pres- (pos (n ℕ.· suc m)) + ∙ cong R.-_ (fromℕ-pres· n (suc m))) + ∙∙ sym (R.-DistR· _ _) + fromℤ-pres· (negsuc n) (pos m) = + cong R.fromℤ (sym (-DistL· (pos (suc n)) (pos m))) + ∙∙ (fromℤ-pres- (pos ((suc n) ℕ.· m)) + ∙ cong R.-_ (fromℕ-pres· (suc n) m)) + ∙∙ sym (R.-DistL· _ _) + fromℤ-pres· (negsuc n) (negsuc m) = + fromℕ-pres· (suc n) (suc m) + ∙∙ cong₂ R._·_ (sym (R.-Idempotent _)) refl + ∙∙ R.-Swap· _ _ + + isHomFromℤ : IsCommRingHom (ℤCommRing .snd) R.fromℤ (R .snd) + isHomFromℤ .IsCommRingHom.pres0 = refl + isHomFromℤ .IsCommRingHom.pres1 = refl + isHomFromℤ .IsCommRingHom.pres+ = fromℤ-pres+ + isHomFromℤ .IsCommRingHom.pres· = fromℤ-pres· + isHomFromℤ .IsCommRingHom.pres- = fromℤ-pres- + + fromℤHom : CommRingHom ℤCommRing R + fst fromℤHom = R.fromℤ + snd fromℤHom = isHomFromℤ + + module _ (φ : CommRingHom ℤCommRing R) where + + open IsCommRingHom (snd φ) + + isUniqueFromℕ : ∀ n → R.fromℕ n ≡ φ $cr pos n + isUniqueFromℕ zero = sym pres0 + isUniqueFromℕ (suc zero) = sym pres1 + isUniqueFromℕ (suc k@(suc n)) = cong₂ R._+_ (sym pres1) (isUniqueFromℕ k) + ∙ sym (pres+ 1 (pos k)) + + isUniqueFromℤ : ∀ n → R.fromℤ n ≡ φ $cr n + isUniqueFromℤ (pos n) = isUniqueFromℕ n + isUniqueFromℤ (negsuc n) = cong R.-_ (isUniqueFromℕ (suc n)) + ∙ sym (pres- (pos (suc n))) + + isContrHom[ℤCR,-] : isContr (CommRingHom ℤCommRing R) + fst isContrHom[ℤCR,-] = fromℤHom + snd isContrHom[ℤCR,-] = CommRingHom≡ ∘ funExt ∘ isUniqueFromℤ diff --git a/Cubical/Algebra/OrderedCommRing.agda b/Cubical/Algebra/OrderedCommRing.agda index 2aca413aff..ba0a384be4 100644 --- a/Cubical/Algebra/OrderedCommRing.agda +++ b/Cubical/Algebra/OrderedCommRing.agda @@ -1,3 +1,4 @@ module Cubical.Algebra.OrderedCommRing where open import Cubical.Algebra.OrderedCommRing.Base public +open import Cubical.Algebra.OrderedCommRing.Properties public diff --git a/Cubical/Algebra/OrderedCommRing/Base.agda b/Cubical/Algebra/OrderedCommRing/Base.agda index 29cd5dbb4b..0bf5ca7948 100644 --- a/Cubical/Algebra/OrderedCommRing/Base.agda +++ b/Cubical/Algebra/OrderedCommRing/Base.agda @@ -4,20 +4,25 @@ module Cubical.Algebra.OrderedCommRing.Base where -} open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels open import Cubical.Foundations.SIP +open import Cubical.Algebra.CommRing.Base + import Cubical.Functions.Logic as L -open import Cubical.Relation.Nullary.Base +open import Cubical.HITs.PropositionalTruncation as PT -open import Cubical.Algebra.CommRing.Base +open import Cubical.Reflection.RecordEquiv open import Cubical.Relation.Binary.Base -open import Cubical.Relation.Binary.Order.Poset hiding (isPseudolattice) -open import Cubical.Relation.Binary.Order.StrictOrder - +open import Cubical.Relation.Binary.Order.Poset hiding ( + isPseudolattice ; isPropIsPseudolattice) open import Cubical.Relation.Binary.Order.Pseudolattice +open import Cubical.Relation.Binary.Order.StrictOrder +open import Cubical.Relation.Nullary open BinaryRelation @@ -53,6 +58,8 @@ record IsOrderedCommRing ; _∧l_ to _⊓_ ; _∨l_ to _⊔_) public open IsStrictOrder isStrictOrder hiding (is-set) renaming (is-prop-valued to is-prop-valued< ; is-trans to is-trans<) public +unquoteDecl IsOrderedCommRingIsoΣ = declareRecordIsoΣ IsOrderedCommRingIsoΣ (quote IsOrderedCommRing) + record OrderedCommRingStr (ℓ' : Level) (R : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where constructor orderedcommringstr field @@ -134,3 +141,26 @@ OrderedCommRing→CommRing : OrderedCommRing ℓ ℓ' → CommRing ℓ OrderedCommRing→CommRing R .fst = R .fst OrderedCommRing→CommRing R .snd = commringstr _ _ _ _ _ isCommRing where open OrderedCommRingStr (str R) + +isPropIsOrderedCommRing : {R : Type ℓ} + → (0r 1r : R) + → (_+_ _·_ : R → R → R) (-_ : R → R) + → (_<_ _≤_ : R → R → Type ℓ') + → isProp (IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_) +isPropIsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_ = isOfHLevelRetractFromIso 1 + IsOrderedCommRingIsoΣ $ + isPropΣ (isPropIsCommRing _ _ _ _ _) λ isCR → + isPropΣ (isPropIsPseudolattice _) λ isPL → + isPropΣ (isPropIsStrictOrder _) λ isSO → + isProp× (isPropΠ3 λ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $ + isProp× (isPropΠ2 λ x y → isOfHLevel≃ 1 + (IsPoset.is-prop-valued (IsPseudolattice.isPoset isPL) x y) + (isProp¬ (y < x))) $ + isProp× (isPropΠ4 λ _ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $ + isProp× (isPropΠ4 λ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $ + isProp× (isPropΠ3 λ _ _ _ → PT.squash₁) $ + isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $ + isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $ + isProp× (isPropΠ5 λ _ _ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $ + isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) + (isSO .IsStrictOrder.is-prop-valued _ _) diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda index 45a38d41c6..cb25a0bd4b 100644 --- a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda +++ b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda @@ -8,15 +8,20 @@ open import Cubical.Data.Empty as ⊥ open import Cubical.HITs.PropositionalTruncation +open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc) +open import Cubical.Data.Nat.Order as ℕ using () renaming (_≤_ to _≤ℕ_ ; _<_ to _<ℕ_) +import Cubical.Data.Nat.Order.Inductive as ℕ open import Cubical.Data.Fast.Int as ℤ renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_) open import Cubical.Data.Fast.Int.Order renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_) +open import Cubical.Algebra.Ring open import Cubical.Algebra.CommRing open import Cubical.Algebra.CommRing.Instances.Fast.Int open import Cubical.Algebra.OrderedCommRing +open import Cubical.Algebra.OrderedCommRing.Morphisms open import Cubical.Relation.Nullary @@ -64,3 +69,95 @@ isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ isOrderedCommRingℤ .·MonoR≤ = λ _ _ _ → 0≤o→≤-·o isOrderedCommRingℤ .·MonoR< = λ _ _ _ → 0n = ⊥.rec (R.is-asym _ _ fmn)) + + isOCRHomFromℤ : IsOrderedCommRingHom (snd ℤOrderedCommRing) R.fromℤ (snd R) + isOCRHomFromℤ .IsOrderedCommRingHom.isCommRingHom = isHomFromℤ + isOCRHomFromℤ .IsOrderedCommRingHom.pres≤ = fromℤ-pres≤ + isOCRHomFromℤ .IsOrderedCommRingHom.reflect< = fromℤ-reflect< + + isOCRMonoFromℤ : IsOrderedCommRingMono (snd ℤOrderedCommRing) R.fromℤ (snd R) + isOCRMonoFromℤ .IsOrderedCommRingMono.isOrderedCommRingHom = isOCRHomFromℤ + isOCRMonoFromℤ .IsOrderedCommRingMono.pres< = fromℤ-pres< + + fromℤOCR : OrderedCommRingHom ℤOrderedCommRing R + fst fromℤOCR = R.fromℤ + snd fromℤOCR = isOCRHomFromℤ + + fromℤOCRMono : OrderedCommRingMono ℤOrderedCommRing R + fst fromℤOCRMono = R.fromℤ + snd fromℤOCRMono = isOCRMonoFromℤ + + isContrHom[ℤOCR,-] : isContr (OrderedCommRingHom ℤOrderedCommRing R) + fst isContrHom[ℤOCR,-] = fromℤOCR + snd isContrHom[ℤOCR,-] = + OrderedCommRingHom≡ ∘ funExt ∘ isUniqueFromℤ ∘ OrderedCommRingHom→CommRingHom + + isContrMono[ℤOCR,-] : isContr (OrderedCommRingMono ℤOrderedCommRing R) + fst isContrMono[ℤOCR,-] = fromℤOCRMono + snd isContrMono[ℤOCR,-] = + OrderedCommRingMono≡ ∘ funExt ∘ isUniqueFromℤ ∘ OrderedCommRingMono→CommRingHom diff --git a/Cubical/Algebra/OrderedCommRing/Morphisms.agda b/Cubical/Algebra/OrderedCommRing/Morphisms.agda new file mode 100644 index 0000000000..4e74bb721e --- /dev/null +++ b/Cubical/Algebra/OrderedCommRing/Morphisms.agda @@ -0,0 +1,360 @@ +module Cubical.Algebra.OrderedCommRing.Morphisms where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.SIP + +open import Cubical.Algebra.CommRing.Base +open import Cubical.Algebra.OrderedCommRing.Base + +open import Cubical.Data.Sigma + +open import Cubical.Reflection.RecordEquiv + +private + variable + ℓ ℓ' ℓ<≤ ℓ<≤' : Level + +record IsOrderedCommRingHom {A : Type ℓ} {B : Type ℓ'} + (R : OrderedCommRingStr ℓ<≤ A) + (f : A → B) + (S : OrderedCommRingStr ℓ<≤' B) + : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ<≤ ℓ<≤'))) + where + no-eta-equality + private + module R = OrderedCommRingStr R + module S = OrderedCommRingStr S + Rcring = str (OrderedCommRing→CommRing (_ , R)) + Scring = str (OrderedCommRing→CommRing (_ , S)) + + field + isCommRingHom : IsCommRingHom Rcring f Scring + pres≤ : ∀ x y → x R.≤ y → f x S.≤ f y + reflect< : ∀ x y → f x S.< f y → x R.< y + + open IsCommRingHom isCommRingHom public + +unquoteDecl IsOrderedCommRingHomIsoΣ = declareRecordIsoΣ IsOrderedCommRingHomIsoΣ (quote IsOrderedCommRingHom) + +OrderedCommRingHom : OrderedCommRing ℓ ℓ<≤ → OrderedCommRing ℓ' ℓ<≤' → Type _ +OrderedCommRingHom R S = + Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsOrderedCommRingHom (R .snd) f (S .snd) + +isPropIsOrderedCommRingHom : {A : Type ℓ} {B : Type ℓ'} + → (R : OrderedCommRingStr ℓ<≤ A) + → (f : A → B) + → (S : OrderedCommRingStr ℓ<≤' B) + → isProp (IsOrderedCommRingHom R f S) +isPropIsOrderedCommRingHom R f S = isOfHLevelRetractFromIso 1 + IsOrderedCommRingHomIsoΣ $ + isProp×2 (isPropIsCommRingHom _ f _) + (isPropΠ2 λ _ _ → isProp→ (S.is-prop-valued≤ _ _)) + (isPropΠ2 λ _ _ → isProp→ (R.is-prop-valued< _ _)) + where + open module R = OrderedCommRingStr R + open module S = OrderedCommRingStr S + +isSetOrderedCommRingHom : (R : OrderedCommRing ℓ ℓ<≤) (S : OrderedCommRing ℓ' ℓ<≤') + → isSet (OrderedCommRingHom R S) +isSetOrderedCommRingHom R S = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f → + isPropIsOrderedCommRingHom (snd R) f (snd S)) + where open OrderedCommRingStr (str S) using (is-set) + +module _ + {R : OrderedCommRing ℓ ℓ<≤} + {S : OrderedCommRing ℓ' ℓ<≤'} + {f : ⟨ R ⟩ → ⟨ S ⟩} where + + private + module R = OrderedCommRingStr (str R) + module S = OrderedCommRingStr (str S) + RCR = OrderedCommRing→CommRing R + SCR = OrderedCommRing→CommRing S + + module _ + (p1 : f R.1r ≡ S.1r) + (p+ : ∀ x y → f (x R.+ y) ≡ f x S.+ f y) + (p· : ∀ x y → f (x R.· y) ≡ f x S.· f y) + (p<⁻ : ∀ x y → f x S.< f y → x R.< y) + where + + open IsOrderedCommRingHom + + private + p≤ : ∀ x y → x R.≤ y → f x S.≤ f y + p≤ x y = invEq (S.≤≃¬> (f x) (f y)) ∘ (_∘ p<⁻ y x) ∘ equivFun (R.≤≃¬> x y) + + makeIsOrderedCommRingHom : IsOrderedCommRingHom (str R) f (str S) + makeIsOrderedCommRingHom .isCommRingHom = makeIsCommRingHom p1 p+ p· + makeIsOrderedCommRingHom .pres≤ = p≤ + makeIsOrderedCommRingHom .reflect< = p<⁻ + + module _ (isHomf : IsOrderedCommRingHom (str R) f (str S)) where + + isOrderedCommRingHom→IsCommRingHom : IsCommRingHom (str RCR) f (str SCR) + isOrderedCommRingHom→IsCommRingHom = isCommRingHom + where open IsOrderedCommRingHom isHomf + +OrderedCommRingHom→CommRingHom : {A : OrderedCommRing ℓ ℓ<≤} + → {B : OrderedCommRing ℓ' ℓ<≤'} + → OrderedCommRingHom A B + → CommRingHom + (OrderedCommRing→CommRing A) + (OrderedCommRing→CommRing B) +fst (OrderedCommRingHom→CommRingHom f) = fst f +snd (OrderedCommRingHom→CommRingHom f) = isOrderedCommRingHom→IsCommRingHom (snd f) + +_$ocr_ : {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} + → (φ : OrderedCommRingHom R S) → (x : ⟨ R ⟩) → ⟨ S ⟩ +φ $ocr x = φ .fst x + +opaque + OrderedCommRingHom≡ : {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} + → {φ ψ : OrderedCommRingHom R S} + → fst φ ≡ fst ψ + → φ ≡ ψ + OrderedCommRingHom≡ = Σ≡Prop λ f → isPropIsOrderedCommRingHom _ f _ + + OrderedCommRingHomPathP : (R : OrderedCommRing ℓ ℓ<≤) (S T : OrderedCommRing ℓ' ℓ<≤') + → (p : S ≡ T) + → (φ : OrderedCommRingHom R S) + → (ψ : OrderedCommRingHom R T) + → PathP (λ i → R .fst → p i .fst) (φ .fst) (ψ .fst) + → PathP (λ i → OrderedCommRingHom R (p i)) φ ψ + OrderedCommRingHomPathP R S T p φ ψ q = ΣPathP (q , isProp→PathP (λ _ → + isPropIsOrderedCommRingHom _ _ _) _ _) + +record IsOrderedCommRingMono {A : Type ℓ} {B : Type ℓ'} + (R : OrderedCommRingStr ℓ<≤ A) + (f : A → B) + (S : OrderedCommRingStr ℓ<≤' B) + : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ<≤ ℓ<≤'))) + where + no-eta-equality + private + module R = OrderedCommRingStr R + module S = OrderedCommRingStr S + + field + isOrderedCommRingHom : IsOrderedCommRingHom R f S + pres< : (x y : A) → x R.< y → f x S.< f y + + open IsOrderedCommRingHom isOrderedCommRingHom public + +unquoteDecl IsOrderedCommRingMonoIsoΣ = declareRecordIsoΣ IsOrderedCommRingMonoIsoΣ (quote IsOrderedCommRingMono) + +OrderedCommRingMono : OrderedCommRing ℓ ℓ<≤ → OrderedCommRing ℓ' ℓ<≤' → Type _ +OrderedCommRingMono R S = + Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsOrderedCommRingMono (R .snd) f (S .snd) + +OrderedCommRingMono→OrderedCommRingHom : {A : OrderedCommRing ℓ ℓ<≤} + → {B : OrderedCommRing ℓ' ℓ<≤'} + → OrderedCommRingMono A B + → OrderedCommRingHom A B +fst (OrderedCommRingMono→OrderedCommRingHom f) = fst f +snd (OrderedCommRingMono→OrderedCommRingHom f) = isOrderedCommRingHom + where open IsOrderedCommRingMono (snd f) + +OrderedCommRingMono→CommRingHom : {A : OrderedCommRing ℓ ℓ<≤} + → {B : OrderedCommRing ℓ' ℓ<≤'} + → OrderedCommRingMono A B + → CommRingHom + (OrderedCommRing→CommRing A) + (OrderedCommRing→CommRing B) +OrderedCommRingMono→CommRingHom = + OrderedCommRingHom→CommRingHom ∘ OrderedCommRingMono→OrderedCommRingHom + +isPropIsOrderedCommRingMono : {A : Type ℓ} {B : Type ℓ'} + → (R : OrderedCommRingStr ℓ<≤ A) + → (f : A → B) + → (S : OrderedCommRingStr ℓ<≤' B) + → isProp (IsOrderedCommRingMono R f S) +isPropIsOrderedCommRingMono R f S = isOfHLevelRetractFromIso 1 + IsOrderedCommRingMonoIsoΣ $ + isProp× (isPropIsOrderedCommRingHom R f S) + (isPropΠ2 λ _ _ → isProp→ (S.is-prop-valued< _ _)) + where + open module S = OrderedCommRingStr S + +isSetOrderedCommRingMono : (R : OrderedCommRing ℓ ℓ<≤) (S : OrderedCommRing ℓ' ℓ<≤') + → isSet (OrderedCommRingMono R S) +isSetOrderedCommRingMono R S = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f → + isPropIsOrderedCommRingMono (snd R) f (snd S)) + where open OrderedCommRingStr (str S) using (is-set) + +module _ + {R : OrderedCommRing ℓ ℓ<≤} + {S : OrderedCommRing ℓ' ℓ<≤'} + {f : ⟨ R ⟩ → ⟨ S ⟩} where + + private + module R = OrderedCommRingStr (str R) + module S = OrderedCommRingStr (str S) + + module _ + (p1 : f R.1r ≡ S.1r) + (p+ : ∀ x y → f (x R.+ y) ≡ f x S.+ f y) + (p· : ∀ x y → f (x R.· y) ≡ f x S.· f y) + (p< : ∀ x y → x R.< y → f x S.< f y) + (p<⁻ : ∀ x y → f x S.< f y → x R.< y) + where + + open IsOrderedCommRingMono + + makeIsOrderedCommRingMono : IsOrderedCommRingMono (str R) f (str S) + makeIsOrderedCommRingMono .isOrderedCommRingHom = makeIsOrderedCommRingHom p1 p+ p· p<⁻ + makeIsOrderedCommRingMono .pres< = p< + + module _ (isMonof : IsOrderedCommRingMono (str R) f (str S)) where + + isOrderedCommRingMono→reflect≤ : ∀ x y → f x S.≤ f y → x R.≤ y + isOrderedCommRingMono→reflect≤ x y = + invEq (R.≤≃¬> x y) ∘ (_∘ pres< y x) ∘ equivFun (S.≤≃¬> (f x) (f y)) + where open IsOrderedCommRingMono isMonof + + isOrderedCommRingMono→isOrderedCommRingHom : IsOrderedCommRingHom (str R) f (str S) + isOrderedCommRingMono→isOrderedCommRingHom = isOrderedCommRingHom + where open IsOrderedCommRingMono isMonof + + isOrderedCommRingMono→isInjective : ∀ x y → f x ≡ f y → x ≡ y + isOrderedCommRingMono→isInjective x y fx≡fy = R.is-antisym x y + (isOrderedCommRingMono→reflect≤ x y (subst (S._≤_ (f x)) fx≡fy (S.is-refl _))) + (isOrderedCommRingMono→reflect≤ y x (subst (S._≤_ (f y)) (sym fx≡fy) (S.is-refl _))) + +opaque + OrderedCommRingMono≡ : {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} + → {φ ψ : OrderedCommRingMono R S} + → fst φ ≡ fst ψ + → φ ≡ ψ + OrderedCommRingMono≡ = Σ≡Prop λ f → isPropIsOrderedCommRingMono _ f _ + + OrderedCommRingMonoPathP : (R : OrderedCommRing ℓ ℓ<≤) (S T : OrderedCommRing ℓ' ℓ<≤') + → (p : S ≡ T) + → (φ : OrderedCommRingMono R S) + → (ψ : OrderedCommRingMono R T) + → PathP (λ i → R .fst → p i .fst) (φ .fst) (ψ .fst) + → PathP (λ i → OrderedCommRingMono R (p i)) φ ψ + OrderedCommRingMonoPathP R S T p φ ψ q = ΣPathP (q , isProp→PathP (λ _ → + isPropIsOrderedCommRingMono _ _ _) _ _) + +record IsOrderedCommRingEquiv {A : Type ℓ} {B : Type ℓ'} + (R : OrderedCommRingStr ℓ<≤ A) (e : A ≃ B) (S : OrderedCommRingStr ℓ<≤' B) + : Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ<≤) ℓ') ℓ<≤') + where + no-eta-equality + private + module R = OrderedCommRingStr R + module S = OrderedCommRingStr S + Rcring = str (OrderedCommRing→CommRing (_ , R)) + Scring = str (OrderedCommRing→CommRing (_ , S)) + f = equivFun e + + field + pres0 : f R.0r ≡ S.0r + pres1 : f R.1r ≡ S.1r + pres+ : (x y : A) → f (x R.+ y) ≡ f x S.+ f y + pres· : (x y : A) → f (x R.· y) ≡ f x S.· f y + pres- : (x : A) → f (R.- x) ≡ S.- (f x) + pres≤ : (x y : A) → (x R.≤ y) ≃ (f x S.≤ f y) + pres< : (x y : A) → (x R.< y) ≃ (f x S.< f y) + +unquoteDecl IsOrderedCommRingEquivIsoΣ = declareRecordIsoΣ IsOrderedCommRingEquivIsoΣ (quote IsOrderedCommRingEquiv) + +OrderedCommRingEquiv : OrderedCommRing ℓ ℓ<≤ → OrderedCommRing ℓ' ℓ<≤' → Type _ +OrderedCommRingEquiv R S = + Σ[ e ∈ (R .fst ≃ S .fst) ] IsOrderedCommRingEquiv (R .snd) e (S .snd) + + +OrderedCommRingEquiv→OrderedCommRingMono : {A : OrderedCommRing ℓ ℓ<≤} + → {B : OrderedCommRing ℓ' ℓ<≤'} + → OrderedCommRingEquiv A B + → OrderedCommRingMono A B +fst (OrderedCommRingEquiv→OrderedCommRingMono e) = equivFun (fst e) +snd (OrderedCommRingEquiv→OrderedCommRingMono e) = isOCRMono + where + module E = IsOrderedCommRingEquiv (snd e) + open IsCommRingHom + open IsOrderedCommRingHom renaming (isCommRingHom to isCRHom) + open IsOrderedCommRingMono renaming (isOrderedCommRingHom to isOCRHom) + + isOCRMono : IsOrderedCommRingMono _ _ _ + isOCRMono .isOCRHom .isCRHom .pres0 = E.pres0 + isOCRMono .isOCRHom .isCRHom .pres1 = E.pres1 + isOCRMono .isOCRHom .isCRHom .pres+ = E.pres+ + isOCRMono .isOCRHom .isCRHom .pres· = E.pres· + isOCRMono .isOCRHom .isCRHom .pres- = E.pres- + isOCRMono .isOCRHom .pres≤ = λ x y → equivFun (E.pres≤ x y) + isOCRMono .isOCRHom .reflect< = λ x y → invEq (E.pres< x y) + isOCRMono .pres< = λ x y → equivFun (E.pres< x y) + +OrderedCommRingEquiv→OrderedCommRingHom : {A : OrderedCommRing ℓ ℓ<≤} + → {B : OrderedCommRing ℓ' ℓ<≤'} + → OrderedCommRingEquiv A B + → OrderedCommRingHom A B +OrderedCommRingEquiv→OrderedCommRingHom = + OrderedCommRingMono→OrderedCommRingHom ∘ OrderedCommRingEquiv→OrderedCommRingMono + +OrderedCommRingEquiv→CommRingHom : {A : OrderedCommRing ℓ ℓ<≤} + → {B : OrderedCommRing ℓ' ℓ<≤'} + → OrderedCommRingEquiv A B + → CommRingHom + (OrderedCommRing→CommRing A) + (OrderedCommRing→CommRing B) +OrderedCommRingEquiv→CommRingHom = + OrderedCommRingHom→CommRingHom ∘ OrderedCommRingEquiv→OrderedCommRingHom + +isPropIsOrderedCommRingEquiv : {A : Type ℓ} {B : Type ℓ'} + → (R : OrderedCommRingStr ℓ<≤ A) + → (e : A ≃ B) + → (S : OrderedCommRingStr ℓ<≤' B) + → isProp (IsOrderedCommRingEquiv R e S) +isPropIsOrderedCommRingEquiv R e S = isOfHLevelRetractFromIso 1 + IsOrderedCommRingEquivIsoΣ $ + isProp× (S.is-set _ _) $ + isProp× (S.is-set _ _) $ + isProp× (isPropΠ2 λ _ _ → S.is-set _ _) $ + isProp× (isPropΠ2 λ _ _ → S.is-set _ _) $ + isProp× (isPropΠ λ _ → S.is-set _ _) $ + isProp× (isPropΠ2 λ _ _ → isOfHLevel≃ 1 (R.is-prop-valued≤ _ _) (S.is-prop-valued≤ _ _)) + (isPropΠ2 λ _ _ → isOfHLevel≃ 1 (R.is-prop-valued< _ _) (S.is-prop-valued< _ _)) + where + open module R = OrderedCommRingStr R + open module S = OrderedCommRingStr S + +isSetOrderedCommRingEquiv : (R : OrderedCommRing ℓ ℓ<≤) (S : OrderedCommRing ℓ' ℓ<≤') + → isSet (OrderedCommRingEquiv R S) +isSetOrderedCommRingEquiv R S = isSetΣSndProp (isOfHLevel≃ 2 R.is-set S.is-set) (λ e → + isPropIsOrderedCommRingEquiv (snd R) e (snd S)) + where + open module R = OrderedCommRingStr (str R) + open module S = OrderedCommRingStr (str S) + +-- an easier way of establishing an equivalence of ordered commutative rings +module _ {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} (e : ⟨ R ⟩ ≃ ⟨ S ⟩) + where + private + module R = OrderedCommRingStr (str R) + module S = OrderedCommRingStr (str S) + + module _ (isMono : IsOrderedCommRingMono (str R) (equivFun e) (str S)) where + + private + module M = IsOrderedCommRingMono isMono + + open IsOrderedCommRingEquiv + + makeIsOrderedCommRingEquiv : IsOrderedCommRingEquiv (str R) e (str S) + makeIsOrderedCommRingEquiv .pres0 = M.pres0 + makeIsOrderedCommRingEquiv .pres1 = M.pres1 + makeIsOrderedCommRingEquiv .pres+ = M.pres+ + makeIsOrderedCommRingEquiv .pres· = M.pres· + makeIsOrderedCommRingEquiv .pres- = M.pres- + makeIsOrderedCommRingEquiv .pres≤ = λ x y → propBiimpl→Equiv + (R.is-prop-valued≤ _ _) (S.is-prop-valued≤ _ _) + (M.pres≤ x y) (isOrderedCommRingMono→reflect≤ isMono x y) + makeIsOrderedCommRingEquiv .pres< = λ x y → propBiimpl→Equiv + (R.is-prop-valued< _ _) (S.is-prop-valued< _ _) + (M.pres< x y) (M.reflect< x y) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda new file mode 100644 index 0000000000..1a9a11c117 --- /dev/null +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -0,0 +1,683 @@ +module Cubical.Algebra.OrderedCommRing.Properties where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure + +open import Cubical.Algebra.CommMonoid +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommSemiring +open import Cubical.Algebra.OrderedCommRing.Base +open import Cubical.Algebra.Ring +open import Cubical.Algebra.Semigroup + +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Sigma +open import Cubical.Data.Sum + +open import Cubical.HITs.PropositionalTruncation as PT + +open import Cubical.Relation.Binary.Order.Apartness +open import Cubical.Relation.Binary.Order.Poset hiding (isPseudolattice) +open import Cubical.Relation.Binary.Order.Pseudolattice +open import Cubical.Relation.Binary.Order.Quoset +open import Cubical.Relation.Binary.Order.QuosetReasoning +open import Cubical.Relation.Binary.Order.StrictOrder + +open import Cubical.Relation.Nullary + +open import Cubical.Tactics.CommRingSolver + +private + variable + ℓ ℓ' ℓ'' : Level + +OrderedCommRing→StrictOrder : OrderedCommRing ℓ ℓ' → StrictOrder ℓ ℓ' +OrderedCommRing→StrictOrder R .fst = R .fst +OrderedCommRing→StrictOrder R .snd = strictorderstr _ isStrictOrder where + open OrderedCommRingStr (str R) + +OrderedCommRing→Ring : OrderedCommRing ℓ ℓ' → Ring ℓ +OrderedCommRing→Ring = CommRing→Ring ∘ OrderedCommRing→CommRing + +OrderedCommRing→Poset : OrderedCommRing ℓ ℓ' → Poset ℓ ℓ' +OrderedCommRing→Poset = Pseudolattice→Poset ∘ OrderedCommRing→PseudoLattice + +OrderedCommRing→Quoset : OrderedCommRing ℓ ℓ' → Quoset ℓ ℓ' +OrderedCommRing→Quoset = StrictOrder→Quoset ∘ OrderedCommRing→StrictOrder + +OrderedCommRing→Apartness : OrderedCommRing ℓ ℓ' → Apartness ℓ ℓ' +OrderedCommRing→Apartness = StrictOrder→Apartness ∘ OrderedCommRing→StrictOrder + +module _ (R' : OrderedCommRing ℓ ℓ') where + private + R = fst R' + RCR = OrderedCommRing→CommRing R' + open RingTheory (OrderedCommRing→Ring R') + open OrderedCommRingStr (snd R') + open PseudolatticeTheory (OrderedCommRing→PseudoLattice R') public renaming ( + L≤∨ to L≤⊔ ; R≤∨ to R≤⊔ ; ∨Comm to ⊔Comm ; ∨Idem to ⊔Idem ; ∨LUB to ⊔LUB + ; ∧≤L to ⊓≤L ; ∧≤R to ⊓≤R ; ∧Comm to ⊓Comm ; ∧Idem to ⊓Idem ; ∧GLB to ⊓GLB) + + module OrderedCommRingReasoning where + open <-≤-Reasoning + (fst R') + (str (OrderedCommRing→Poset R')) + (str (OrderedCommRing→Quoset R')) + (λ x {y} {z} → <-≤-trans x y z) + (λ x {y} {z} → ≤-<-trans x y z) + (λ {x} {y} → <-≤-weaken x y) + public + + open <-syntax public + open ≤-syntax public + open ≡-syntax public + + _<+[_] : ∀ {x y} → x < y → ∀ z → x + z < y + z + _<+[_] x : ∀ x y → x ≤ y → ¬ (y < x) + ≤→¬> x y = equivFun (≤≃¬> x y) + + ¬<→≥ : ∀ x y → ¬ (x < y) → y ≤ x + ¬<→≥ x y = invEq (≤≃¬> y x) + + +MonoL< : ∀ x y z → x < y → z + x < z + y + +MonoL< x y z = subst2 _<_ (+Comm _ _) (+Comm _ _) ∘ +MonoR< x y z + + +Mono< : ∀ x y z w → x < y → z < w → x + z < y + w + +Mono< x y z w x _ _ zx≤zy ∘ ·MonoL< _ _ z 0 _ _ zx≤zy ∘ ·MonoR< _ _ z 0 _ _ (·MonoL≤ _ _ z (<-≤-weaken 0r z 0 _ _ (·MonoR≤ _ _ z (<-≤-weaken 0r z 0 y x ∘ <→≥)) + + abs ∣_∣ : R → R + abs z = z ⊔ (- z) + ∣_∣ = abs + + Date: Sat, 4 Apr 2026 18:50:34 +0200 Subject: [PATCH 02/19] =?UTF-8?q?add=20`isUniqueFrom=E2=84=A4OCR`=20and=20?= =?UTF-8?q?`isUniqueFrom=E2=84=A4OCRMono`=20in=20`CanonicalMonoFrom?= =?UTF-8?q?=E2=84=A4`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../OrderedCommRing/Instances/Fast/Int.agda | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda index cb25a0bd4b..48ccb6ddff 100644 --- a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda +++ b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda @@ -152,12 +152,20 @@ module CanonicalMonoFromℤ (R : OrderedCommRing ℓ ℓ') where fst fromℤOCRMono = R.fromℤ snd fromℤOCRMono = isOCRMonoFromℤ + isUniqueFromℤOCR : (φ : OrderedCommRingHom ℤOrderedCommRing R) + → ∀ n → R.fromℤ n ≡ fst φ n + isUniqueFromℤOCR φ = isUniqueFromℤ (OrderedCommRingHom→CommRingHom φ) + where open IsOrderedCommRingHom (snd φ) + + isUniqueFromℤOCRMono : (φ : OrderedCommRingMono ℤOrderedCommRing R) + → ∀ n → R.fromℤ n ≡ fst φ n + isUniqueFromℤOCRMono φ = isUniqueFromℤ (OrderedCommRingMono→CommRingHom φ) + where open IsOrderedCommRingMono (snd φ) + isContrHom[ℤOCR,-] : isContr (OrderedCommRingHom ℤOrderedCommRing R) fst isContrHom[ℤOCR,-] = fromℤOCR - snd isContrHom[ℤOCR,-] = - OrderedCommRingHom≡ ∘ funExt ∘ isUniqueFromℤ ∘ OrderedCommRingHom→CommRingHom + snd isContrHom[ℤOCR,-] = OrderedCommRingHom≡ ∘ funExt ∘ isUniqueFromℤOCR isContrMono[ℤOCR,-] : isContr (OrderedCommRingMono ℤOrderedCommRing R) fst isContrMono[ℤOCR,-] = fromℤOCRMono - snd isContrMono[ℤOCR,-] = - OrderedCommRingMono≡ ∘ funExt ∘ isUniqueFromℤ ∘ OrderedCommRingMono→CommRingHom + snd isContrMono[ℤOCR,-] = OrderedCommRingMono≡ ∘ funExt ∘ isUniqueFromℤOCRMono From 9a827882189e8ed66bd0e8d746a93b5a71c45f6c Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Sat, 4 Apr 2026 19:48:36 +0200 Subject: [PATCH 03/19] =?UTF-8?q?call=20the=20ring=20solver=20only=20when?= =?UTF-8?q?=20there=20is=20not=20already=20a=20specific=20lemma=20solving?= =?UTF-8?q?=20the=20equality=20;=20use=20`=5F<+[=5F]`,=20`=5F=E2=89=A4?= =?UTF-8?q?=C2=B7[=5F,=5F]`,=20etc.=20in=20equational=20reasoning=20;=20sh?= =?UTF-8?q?orten=20comment=20about=20`=C2=B7CancelL<`,=20`=C2=B7CancelR<`?= =?UTF-8?q?=20;=20add=20`/2+/2=E2=89=A1mean`=20and=20`mean=E2=82=8A`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Algebra/OrderedCommRing/Properties.agda | 70 ++++++++++--------- 1 file changed, 36 insertions(+), 34 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index 1a9a11c117..415151ce09 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -148,11 +148,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where ·CancelR≤ : ∀ x y z → 0r < z → x · z ≤ y · z → x ≤ y ·CancelR≤ x y z 0 _ _ zx≤zy ∘ ·MonoR< _ _ z 0 _ _ (·MonoL≤ _ _ z (<-≤-weaken 0r z 0 Date: Sat, 4 Apr 2026 19:52:35 +0200 Subject: [PATCH 04/19] =?UTF-8?q?replace=20`<-=E2=89=A4-weaken=20=5F=20=5F?= =?UTF-8?q?=200<1`=20with=20`0=E2=89=A41`=20in=20`R=E2=82=80=E2=82=8ACommS?= =?UTF-8?q?emiring`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cubical/Algebra/OrderedCommRing/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index 415151ce09..622f7957d0 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -508,7 +508,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where R₀₊CommSemiring : CommSemiring _ fst R₀₊CommSemiring = R₀₊ CommSemiringStr.0r (snd R₀₊CommSemiring) = 0r , is-refl _ - CommSemiringStr.1r (snd R₀₊CommSemiring) = 1r , <-≤-weaken _ _ 0<1 + CommSemiringStr.1r (snd R₀₊CommSemiring) = 1r , 0≤1 CommSemiringStr._+_ (snd R₀₊CommSemiring) = _+₀₊_ CommSemiringStr._·_ (snd R₀₊CommSemiring) = _·₀₊_ CommSemiringStr.isCommSemiring (snd R₀₊CommSemiring) = From 4531d699b4a9c34707f2a1a1f15a6f12b6a1c15a Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Sat, 4 Apr 2026 23:29:16 +0200 Subject: [PATCH 05/19] move export of `PseudolatticeTheory`, add type annotation to `subtype` --- Cubical/Algebra/OrderedCommRing/Properties.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index 622f7957d0..1dc65943df 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -57,9 +57,6 @@ module _ (R' : OrderedCommRing ℓ ℓ') where RCR = OrderedCommRing→CommRing R' open RingTheory (OrderedCommRing→Ring R') open OrderedCommRingStr (snd R') - open PseudolatticeTheory (OrderedCommRing→PseudoLattice R') public renaming ( - L≤∨ to L≤⊔ ; R≤∨ to R≤⊔ ; ∨Comm to ⊔Comm ; ∨Idem to ⊔Idem ; ∨LUB to ⊔LUB - ; ∧≤L to ⊓≤L ; ∧≤R to ⊓≤R ; ∧Comm to ⊓Comm ; ∧Idem to ⊓Idem ; ∧GLB to ⊓GLB) module OrderedCommRingReasoning where open <-≤-Reasoning @@ -114,6 +111,9 @@ module _ (R' : OrderedCommRing ℓ ℓ') where module OrderedCommRingTheory where open ApartnessStr (str (OrderedCommRing→Apartness R')) using (_#_) public + open PseudolatticeTheory (OrderedCommRing→PseudoLattice R') public renaming ( + L≤∨ to L≤⊔ ; R≤∨ to R≤⊔ ; ∨Comm to ⊔Comm ; ∨Idem to ⊔Idem ; ∨LUB to ⊔LUB + ; ∧≤L to ⊓≤L ; ∧≤R to ⊓≤R ; ∧Comm to ⊓Comm ; ∧Idem to ⊓Idem ; ∧GLB to ⊓GLB) 0≤1 : 0r ≤ 1r 0≤1 = <-≤-weaken 0r 1r 0<1 @@ -362,6 +362,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where (+Closed : (x y : R) → P x → P y → P (x + y)) where + subtype : Type (ℓ-max ℓ ℓ'') subtype = Σ[ x ∈ R ] P x isSetSubtype : isSet subtype From f788f6db663497109ae9b7b1047a8525d3fea8b0 Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Sat, 4 Apr 2026 23:33:02 +0200 Subject: [PATCH 06/19] add `using ()` to avoid exporting more than what is needed --- Cubical/Algebra/OrderedCommRing/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index 1dc65943df..88b3904a33 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -111,7 +111,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where module OrderedCommRingTheory where open ApartnessStr (str (OrderedCommRing→Apartness R')) using (_#_) public - open PseudolatticeTheory (OrderedCommRing→PseudoLattice R') public renaming ( + open PseudolatticeTheory (OrderedCommRing→PseudoLattice R') public using () renaming ( L≤∨ to L≤⊔ ; R≤∨ to R≤⊔ ; ∨Comm to ⊔Comm ; ∨Idem to ⊔Idem ; ∨LUB to ⊔LUB ; ∧≤L to ⊓≤L ; ∧≤R to ⊓≤R ; ∧Comm to ⊓Comm ; ∧Idem to ⊓Idem ; ∧GLB to ⊓GLB) From 369a119d1dad22416f26793dc11c2cfd01ce7932 Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Sun, 5 Apr 2026 00:32:35 +0200 Subject: [PATCH 07/19] update `Rationals` to use fast integers operations ; fix broken proofs in `Field.Instances.Rationals` --- .../Algebra/CommRing/Instances/Rationals.agda | 1 - .../Algebra/Field/Instances/Rationals.agda | 33 +- Cubical/Data/Rationals/Base.agda | 2 +- Cubical/Data/Rationals/Order.agda | 311 ++++++++++-------- Cubical/Data/Rationals/Properties.agda | 121 ++++++- 5 files changed, 285 insertions(+), 183 deletions(-) diff --git a/Cubical/Algebra/CommRing/Instances/Rationals.agda b/Cubical/Algebra/CommRing/Instances/Rationals.agda index 92416ac328..eeb40346c9 100644 --- a/Cubical/Algebra/CommRing/Instances/Rationals.agda +++ b/Cubical/Algebra/CommRing/Instances/Rationals.agda @@ -20,4 +20,3 @@ open import Cubical.Data.Rationals as ℚ where p : IsCommRing 0 1 _+_ _·_ (-_) p = makeIsCommRing isSetℚ +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistL+ ·Comm - diff --git a/Cubical/Algebra/Field/Instances/Rationals.agda b/Cubical/Algebra/Field/Instances/Rationals.agda index 2209eb5f03..fa3bfadbd4 100644 --- a/Cubical/Algebra/Field/Instances/Rationals.agda +++ b/Cubical/Algebra/Field/Instances/Rationals.agda @@ -14,7 +14,7 @@ open import Cubical.Algebra.CommRing.Instances.Rationals open import Cubical.Algebra.Field open import Cubical.Data.Empty as Empty -open import Cubical.Data.Int as ℤ +open import Cubical.Data.Fast.Int as ℤ open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc) open import Cubical.Data.NatPlusOne open import Cubical.Data.Rationals as ℚ @@ -42,36 +42,9 @@ hasInverseℚ = SetQuotients.elimProp q (ℤ.pos zero , b) p = Empty.rec (p (numerator0→0 ((ℤ.pos zero , b)) refl)) q (ℤ.pos (suc n) , (1+ m)) _ = - eq/ ((ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m)) , (1+ m) ·₊₁ (1+ n))) ((1 , 1)) q' - where - q' = (ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m))) ℤ.· 1 - ≡⟨ ℤ.·IdR _ ⟩ - ℤ.pos (suc n) ℤ.· ℤ.pos (suc m) - ≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩ - ℤ.pos ((suc n) ℕ.· (suc m)) - ≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩ - ℤ.pos ((suc m) ℕ.· (suc n)) - ≡⟨ refl ⟩ - ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n)) - ≡⟨ sym (ℤ.·IdL _) ⟩ - 1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎ + eq/ _ _ (ℤ.·IdR _ ∙∙ ℤ.·Comm (pos (suc n)) (pos (suc m)) ∙∙ sym (ℤ.·IdL _)) q (ℤ.negsuc n , (1+ m)) _ = - eq/ ((ℤ.negsuc n ℤ.· ℤ.negsuc m) , ((1+ m) ·₊₁ (1+ n))) ((1 , 1)) q' - where - q' : (ℤ.negsuc n ℤ.· ℤ.negsuc m , (1+ m) ·₊₁ (1+ n)) ∼ (1 , 1) - q' = (ℤ.negsuc n ℤ.· ℤ.negsuc m) ℤ.· 1 - ≡⟨ ℤ.·IdR _ ⟩ - (ℤ.negsuc n ℤ.· ℤ.negsuc m) - ≡⟨ negsuc·negsuc n m ⟩ - (ℤ.pos (suc n) ℤ.· ℤ.pos (suc m)) - ≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩ - ℤ.pos ((suc n) ℕ.· (suc m)) - ≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩ - ℤ.pos ((suc m) ℕ.· (suc n)) - ≡⟨ refl ⟩ - ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n)) - ≡⟨ sym (ℤ.·IdL _) ⟩ - 1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎ + eq/ _ _ (ℤ.·IdR _ ∙∙ ℤ.·Comm (pos (suc n)) (pos (suc m)) ∙∙ sym (ℤ.·IdL _)) 0≢1-ℚ : ¬ Path ℚ 0 1 0≢1-ℚ p = 0≢1-ℤ (effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ p) diff --git a/Cubical/Data/Rationals/Base.agda b/Cubical/Data/Rationals/Base.agda index ce0f87081b..e2468e3004 100644 --- a/Cubical/Data/Rationals/Base.agda +++ b/Cubical/Data/Rationals/Base.agda @@ -7,7 +7,7 @@ open import Cubical.Foundations.Function open import Cubical.Data.Nat as ℕ using (discreteℕ) open import Cubical.Data.NatPlusOne open import Cubical.Data.Sigma -open import Cubical.Data.Int +open import Cubical.Data.Fast.Int open import Cubical.HITs.SetQuotients as SetQuotient using ([_]; eq/; discreteSetQuotients) renaming (_/_ to _//_) public diff --git a/Cubical/Data/Rationals/Order.agda b/Cubical/Data/Rationals/Order.agda index 106d6334ec..2755b7bcba 100644 --- a/Cubical/Data/Rationals/Order.agda +++ b/Cubical/Data/Rationals/Order.agda @@ -9,9 +9,9 @@ open import Cubical.Foundations.Univalence open import Cubical.Functions.Logic using (_⊔′_) open import Cubical.Data.Empty as ⊥ -open import Cubical.Data.Int.Base as ℤ using (ℤ) -open import Cubical.Data.Int.Properties as ℤ using () -open import Cubical.Data.Int.Order as ℤ using () +open import Cubical.Data.Fast.Int.Base as ℤ using (ℤ) +import Cubical.Data.Fast.Int.Properties as ℤ +import Cubical.Data.Fast.Int.Order as ℤ open import Cubical.Data.Rationals.Base as ℚ open import Cubical.Data.Rationals.Properties as ℚ open import Cubical.Data.Nat as ℕ @@ -20,7 +20,7 @@ open import Cubical.Data.Sigma open import Cubical.Data.Sum as ⊎ using (_⊎_; inl; inr; isProp⊎) open import Cubical.HITs.PropositionalTruncation as ∥₁ using (isPropPropTrunc; ∣_∣₁) -open import Cubical.HITs.SetQuotients +open import Cubical.HITs.SetQuotients renaming (_/_ to _//_) open import Cubical.Relation.Nullary open import Cubical.Relation.Binary.Base @@ -39,18 +39,18 @@ private → ((a ℤ.· ℕ₊₁→ℤ d) ℤ.≤ (c ℤ.· ℕ₊₁→ℤ b)) ≡ ((a ℤ.· ℕ₊₁→ℤ f) ℤ.≤ (e ℤ.· ℕ₊₁→ℤ b)) lemma≤ (a , b) (c , d) (e , f) cf≡ed = (ua (propBiimpl→Equiv ℤ.isProp≤ ℤ.isProp≤ - (ℤ.≤-·o-cancel {k = -1+ d} ∘ + (ℤ.≤-·o-cancel ∘ subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) (·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) ∙ cong (ℤ._· ℕ₊₁→ℤ b) cf≡ed ∙ ·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘ - ℤ.≤-·o {k = ℕ₊₁→ℕ f}) - (ℤ.≤-·o-cancel {k = -1+ f} ∘ + ℤ.≤-·o) + (ℤ.≤-·o-cancel ∘ subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d)) (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ∙ cong (ℤ._· ℕ₊₁→ℤ b) (sym cf≡ed) ∙ ·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b)) ∘ - ℤ.≤-·o {k = ℕ₊₁→ℕ d}))) + ℤ.≤-·o))) fun₀ : ℤ × ℕ₊₁ → ℚ → hProp ℓ-zero fst (fun₀ (a , b) [ c , d ]) = a ℤ.· ℕ₊₁→ℤ d ℤ.≤ c ℤ.· ℕ₊₁→ℤ b @@ -68,18 +68,18 @@ private toPath : ∀ a/b c/d (x : a/b ∼ c/d) (y : ℚ) → fun₀ a/b y ≡ fun₀ c/d y toPath (a , b) (c , d) ad≡cb = elimProp (λ _ → isSetHProp _ _) λ (e , f) → Σ≡Prop (λ _ → isPropIsProp) (ua (propBiimpl→Equiv ℤ.isProp≤ ℤ.isProp≤ - (ℤ.≤-·o-cancel {k = -1+ b} ∘ + (ℤ.≤-·o-cancel ∘ subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) ∙ cong (ℤ._· ℕ₊₁→ℤ f) ad≡cb ∙ ·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∘ - ℤ.≤-·o {k = ℕ₊₁→ℕ d}) - (ℤ.≤-·o-cancel {k = -1+ d} ∘ + ℤ.≤-·o) + (ℤ.≤-·o-cancel ∘ subst2 ℤ._≤_ (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) ∙ cong (ℤ._· ℕ₊₁→ℤ f) (sym ad≡cb) ∙ ·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘ - ℤ.≤-·o {k = ℕ₊₁→ℕ b}))) + ℤ.≤-·o))) fun : ℚ → ℚ → hProp ℓ-zero fun [ a/b ] y = fun₀ a/b y @@ -95,18 +95,18 @@ private → ((a ℤ.· ℕ₊₁→ℤ d) ℤ.< (c ℤ.· ℕ₊₁→ℤ b)) ≡ ((a ℤ.· ℕ₊₁→ℤ f) ℤ.< (e ℤ.· ℕ₊₁→ℤ b)) lemma< (a , b) (c , d) (e , f) cf≡ed = (ua (propBiimpl→Equiv ℤ.isProp< ℤ.isProp< - (ℤ.<-·o-cancel {k = -1+ d} ∘ + (ℤ.<-·o-cancel ∘ subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) (·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) ∙ cong (ℤ._· ℕ₊₁→ℤ b) cf≡ed ∙ ·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘ - ℤ.<-·o {k = -1+ f}) - (ℤ.<-·o-cancel {k = -1+ f} ∘ + ℤ.<-·o) + (ℤ.<-·o-cancel ∘ subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d)) (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ∙ cong (ℤ._· ℕ₊₁→ℤ b) (sym cf≡ed) ∙ ·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b)) ∘ - ℤ.<-·o {k = -1+ d}))) + ℤ.<-·o))) fun₀ : ℤ × ℕ₊₁ → ℚ → hProp ℓ-zero fst (fun₀ (a , b) [ c , d ]) = a ℤ.· ℕ₊₁→ℤ d ℤ.< c ℤ.· ℕ₊₁→ℤ b @@ -124,18 +124,18 @@ private toPath : ∀ a/b c/d (x : a/b ∼ c/d) (y : ℚ) → fun₀ a/b y ≡ fun₀ c/d y toPath (a , b) (c , d) ad≡cb = elimProp (λ _ → isSetHProp _ _) λ (e , f) → Σ≡Prop (λ _ → isPropIsProp) (ua (propBiimpl→Equiv ℤ.isProp< ℤ.isProp< - (ℤ.<-·o-cancel {k = -1+ b} ∘ + (ℤ.<-·o-cancel ∘ subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) ∙ cong (ℤ._· ℕ₊₁→ℤ f) ad≡cb ∙ ·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∘ - ℤ.<-·o {k = -1+ d}) - (ℤ.<-·o-cancel {k = -1+ d} ∘ + ℤ.<-·o) + (ℤ.<-·o-cancel ∘ subst2 ℤ._<_ (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) ∙ cong (ℤ._· ℕ₊₁→ℤ f) (sym ad≡cb) ∙ ·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘ - ℤ.<-·o {k = -1+ b}))) + ℤ.<-·o))) fun : ℚ → ℚ → hProp ℓ-zero fun [ a/b ] y = fun₀ a/b y @@ -143,11 +143,23 @@ private fun (squash/ x y p q i j) z = isSet→SquareP (λ _ _ → isSetHProp) (λ _ → fun x z) (λ _ → fun y z) (λ i → fun (p i) z) (λ i → fun (q i) z) j i -_≤_ : ℚ → ℚ → Type₀ -m ≤ n = fst (m ≤' n) +record _≤_ (m n : ℚ ) : Type₀ where + constructor inj + field + prf : fst (m ≤' n) -_<_ : ℚ → ℚ → Type₀ -m < n = fst (m <' n) +record _<_ (m n : ℚ ) : Type₀ where + constructor inj + field + prf : fst (m <' n) + +pattern pos≤pos p = inj (ℤ.pos≤pos p) +pattern negsuc≤pos = inj ℤ.negsuc≤pos +pattern negsuc≤negsuc p = inj (ℤ.negsuc≤negsuc p) + +pattern pos n) -≤→≯ m n m≤n n Date: Sun, 5 Apr 2026 01:20:40 +0200 Subject: [PATCH 08/19] add instances of `Rationals` as order structures and as an `OrderedCommRing` ; add positive rationals and their properties --- .../OrderedCommRing/Instances/Rationals.agda | 187 ++++++++++++++++++ .../Order/Loset/Instances/Rationals.agda | 31 +++ .../Order/Poset/Instances/Rationals.agda | 11 ++ .../Order/Proset/Instances/Rationals.agda | 11 ++ .../Pseudolattice/Instances/Rationals.agda | 19 ++ .../Order/Quoset/Instances/Rationals.agda | 11 ++ .../StrictOrder/Instances/Rationals.agda | 11 ++ .../Order/Toset/Instances/Rationals.agda | 31 +++ 8 files changed, 312 insertions(+) create mode 100644 Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda create mode 100644 Cubical/Relation/Binary/Order/Loset/Instances/Rationals.agda create mode 100644 Cubical/Relation/Binary/Order/Poset/Instances/Rationals.agda create mode 100644 Cubical/Relation/Binary/Order/Proset/Instances/Rationals.agda create mode 100644 Cubical/Relation/Binary/Order/Pseudolattice/Instances/Rationals.agda create mode 100644 Cubical/Relation/Binary/Order/Quoset/Instances/Rationals.agda create mode 100644 Cubical/Relation/Binary/Order/StrictOrder/Instances/Rationals.agda create mode 100644 Cubical/Relation/Binary/Order/Toset/Instances/Rationals.agda diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda b/Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda new file mode 100644 index 0000000000..600f38c22a --- /dev/null +++ b/Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda @@ -0,0 +1,187 @@ +module Cubical.Algebra.OrderedCommRing.Instances.Rationals where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv + +open import Cubical.Data.Empty as ⊥ + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _//_) + +open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_) +open import Cubical.Data.NatPlusOne as ℕ₊₁ +open import Cubical.Data.Fast.Int as ℤ hiding (_+_ ; _-_ ; -_ ; _·_) +import Cubical.Data.Fast.Int.Order as ℤ + +open import Cubical.Data.Rationals as ℚ + renaming (_+_ to _+ℚ_ ; _-_ to _-ℚ_; -_ to -ℚ_ ; _·_ to _·ℚ_) +open import Cubical.Data.Rationals.Order as ℚ + renaming (_<_ to _<ℚ_ ; _≤_ to _≤ℚ_) + +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Instances.Rationals + +open import Cubical.Algebra.OrderedCommRing.Base +open import Cubical.Algebra.OrderedCommRing.Properties + +open import Cubical.Relation.Nullary + +open import Cubical.Relation.Binary.Order.StrictOrder +open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Rationals + +open import Cubical.Relation.Binary.Order.Pseudolattice +open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Rationals + +open CommRingStr +open OrderedCommRingStr +open PseudolatticeStr +open StrictOrderStr + +ℚOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero +fst ℚOrderedCommRing = ℚ +0r (snd ℚOrderedCommRing) = 0 +1r (snd ℚOrderedCommRing) = 1 +_+_ (snd ℚOrderedCommRing) = _+ℚ_ +_·_ (snd ℚOrderedCommRing) = _·ℚ_ +-_ (snd ℚOrderedCommRing) = -ℚ_ +_<_ (snd ℚOrderedCommRing) = _<ℚ_ +_≤_ (snd ℚOrderedCommRing) = _≤ℚ_ +isOrderedCommRing (snd ℚOrderedCommRing) = isOrderedCommRingℚ + where + open IsOrderedCommRing + + isOrderedCommRingℚ : IsOrderedCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_ _<ℚ_ _≤ℚ_ + isOrderedCommRingℚ .isCommRing = ℚCommRing .snd .isCommRing + isOrderedCommRingℚ .isPseudolattice = ℚ≤Pseudolattice .snd .is-pseudolattice + isOrderedCommRingℚ .isStrictOrder = ℚ = λ x y → + propBiimpl→Equiv (isProp≤ x y) (isProp¬ (y <ℚ x)) (≤→≯ x y) (≮→≥ y x) + isOrderedCommRingℚ .+MonoR≤ = ≤-+o + isOrderedCommRingℚ .+MonoR< = <-+o + isOrderedCommRingℚ .posSum→pos∨pos = λ x y → ∣_∣₁ ∘ 0<+ x y + isOrderedCommRingℚ .<-≤-trans = isTrans<≤ + isOrderedCommRingℚ .≤-<-trans = isTrans≤< + isOrderedCommRingℚ .·MonoR≤ = ≤-·o + isOrderedCommRingℚ .·MonoR< = <-·o + isOrderedCommRingℚ .0<1 = pos Date: Sun, 5 Apr 2026 09:09:18 +0200 Subject: [PATCH 09/19] add definition of `PremetricSpace` --- Cubical/Relation/Premetric.agda | 3 ++ Cubical/Relation/Premetric/Base.agda | 73 ++++++++++++++++++++++++++++ 2 files changed, 76 insertions(+) create mode 100644 Cubical/Relation/Premetric.agda create mode 100644 Cubical/Relation/Premetric/Base.agda diff --git a/Cubical/Relation/Premetric.agda b/Cubical/Relation/Premetric.agda new file mode 100644 index 0000000000..845c6bc839 --- /dev/null +++ b/Cubical/Relation/Premetric.agda @@ -0,0 +1,3 @@ +module Cubical.Relation.Premetric where + +open import Cubical.Relation.Premetric.Base public diff --git a/Cubical/Relation/Premetric/Base.agda b/Cubical/Relation/Premetric/Base.agda new file mode 100644 index 0000000000..bd31c2b346 --- /dev/null +++ b/Cubical/Relation/Premetric/Base.agda @@ -0,0 +1,73 @@ +module Cubical.Relation.Premetric.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.SIP + +open import Cubical.Algebra.OrderedCommRing +open import Cubical.Algebra.OrderedCommRing.Instances.Rationals + +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Rationals.Order as ℚ +open import Cubical.Data.Sigma + +open import Cubical.HITs.PropositionalTruncation as PT + +open import Cubical.Reflection.RecordEquiv + +open OrderedCommRingTheory ℚOrderedCommRing +open PositiveRationals + +private + variable + ℓ ℓ' ℓ'' : Level + +record IsPremetric {M : Type ℓ} (_≈[_]_ : M → ℚ₊ → M → Type ℓ') : Type (ℓ-max ℓ ℓ') where + + constructor ispremetric + + field + isSetM : isSet M + isProp≈ : ∀ x y ε → isProp (x ≈[ ε ] y) + isRefl≈ : ∀ x ε → x ≈[ ε ] x + isSym≈ : ∀ x y ε → x ≈[ ε ] y → y ≈[ ε ] x + isSeparated≈ : ∀ x y → (∀ ε → x ≈[ ε ] y) → x ≡ y + isTriangular≈ : ∀ x y z ε δ → x ≈[ ε ] y → y ≈[ δ ] z → x ≈[ ε +₊ δ ] z + isRounded≈ : ∀ x y ε → x ≈[ ε ] y → ∃[ δ ∈ ℚ₊ ] (δ <₊ ε) × (x ≈[ δ ] y) + +unquoteDecl IsPremetricIsoΣ = declareRecordIsoΣ IsPremetricIsoΣ (quote IsPremetric) + + +record PremetricStr (ℓ' : Level) (M : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where + + constructor premetricstr + + field + _≈[_]_ : M → ℚ₊ → M → Type ℓ' + isPremetric : IsPremetric _≈[_]_ + + open IsPremetric isPremetric public + +PremetricSpace : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ')) +PremetricSpace ℓ ℓ' = TypeWithStr ℓ (PremetricStr ℓ') + +premetricspace : (M : Type ℓ) + → (_≈[_]_ : M → ℚ₊ → M → Type ℓ') + → IsPremetric _≈[_]_ + → PremetricSpace ℓ ℓ' +premetricspace M (_≈[_]_) pm = M , (premetricstr _≈[_]_ pm) + +isPropIsPremetric : {M : Type ℓ} → (_≈[_]_ : M → ℚ₊ → M → Type ℓ') + → isProp (IsPremetric _≈[_]_) +isPropIsPremetric _≈[_]_ = isOfHLevelRetractFromIso 1 + IsPremetricIsoΣ $ + isPropΣ isPropIsSet λ isSetM → + isPropΣ (isPropΠ3 λ _ _ _ → isPropIsProp) λ isProp≈ → + isProp×4 + (isPropΠ2 λ _ _ → isProp≈ _ _ _) + (isPropΠ4 λ _ _ _ _ → isProp≈ _ _ _) + (isPropΠ3 λ _ _ _ → isSetM _ _) + (isPropΠ6 λ _ _ _ _ _ _ → isPropΠ λ _ → isProp≈ _ _ _) + (isPropΠ4 λ _ _ _ _ → squash₁) From 5dcf17443204939d7554e4098e64a93cb6dc1397 Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Tue, 14 Apr 2026 01:30:41 +0200 Subject: [PATCH 10/19] typo --- Cubical/Algebra/OrderedCommRing/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index 88b3904a33..c8625a7fe8 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -148,7 +148,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where ·CancelR≤ : ∀ x y z → 0r < z → x · z ≤ y · z → x ≤ y ·CancelR≤ x y z 0 _ _ zx≤zy ∘ ·MonoR< _ _ z 0 Date: Tue, 14 Apr 2026 01:32:55 +0200 Subject: [PATCH 11/19] typo (#41) --- Cubical/Algebra/OrderedCommRing/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index 88b3904a33..c8625a7fe8 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -148,7 +148,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where ·CancelR≤ : ∀ x y z → 0r < z → x · z ≤ y · z → x ≤ y ·CancelR≤ x y z 0 _ _ zx≤zy ∘ ·MonoR< _ _ z 0 Date: Tue, 14 Apr 2026 07:32:30 +0200 Subject: [PATCH 12/19] remove unnecessary imports, make some proofs ~~pointless~~ pointfree --- Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda index 48ccb6ddff..93163da4ef 100644 --- a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda +++ b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda @@ -78,7 +78,6 @@ module CanonicalMonoFromℤ (R : OrderedCommRing ℓ ℓ') where open CanonicalHomFromℤ (OrderedCommRing→CommRing R) open OrderedCommRingTheory R - open OrderedCommRingReasoning R private module R where @@ -154,13 +153,11 @@ module CanonicalMonoFromℤ (R : OrderedCommRing ℓ ℓ') where isUniqueFromℤOCR : (φ : OrderedCommRingHom ℤOrderedCommRing R) → ∀ n → R.fromℤ n ≡ fst φ n - isUniqueFromℤOCR φ = isUniqueFromℤ (OrderedCommRingHom→CommRingHom φ) - where open IsOrderedCommRingHom (snd φ) + isUniqueFromℤOCR = isUniqueFromℤ ∘ OrderedCommRingHom→CommRingHom isUniqueFromℤOCRMono : (φ : OrderedCommRingMono ℤOrderedCommRing R) → ∀ n → R.fromℤ n ≡ fst φ n - isUniqueFromℤOCRMono φ = isUniqueFromℤ (OrderedCommRingMono→CommRingHom φ) - where open IsOrderedCommRingMono (snd φ) + isUniqueFromℤOCRMono = isUniqueFromℤ ∘ OrderedCommRingMono→CommRingHom isContrHom[ℤOCR,-] : isContr (OrderedCommRingHom ℤOrderedCommRing R) fst isContrHom[ℤOCR,-] = fromℤOCR From 7f32dbacb0917fb65a1cc89629539e7784df8be7 Mon Sep 17 00:00:00 2001 From: LorenzoMolena <164308953+LorenzoMolena@users.noreply.github.com> Date: Tue, 14 Apr 2026 07:36:16 +0200 Subject: [PATCH 13/19] Sync with `ocr-update` (#42) * typo * remove unnecessary imports, make some proofs ~pointless~ pointfree --- Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda index 48ccb6ddff..93163da4ef 100644 --- a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda +++ b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda @@ -78,7 +78,6 @@ module CanonicalMonoFromℤ (R : OrderedCommRing ℓ ℓ') where open CanonicalHomFromℤ (OrderedCommRing→CommRing R) open OrderedCommRingTheory R - open OrderedCommRingReasoning R private module R where @@ -154,13 +153,11 @@ module CanonicalMonoFromℤ (R : OrderedCommRing ℓ ℓ') where isUniqueFromℤOCR : (φ : OrderedCommRingHom ℤOrderedCommRing R) → ∀ n → R.fromℤ n ≡ fst φ n - isUniqueFromℤOCR φ = isUniqueFromℤ (OrderedCommRingHom→CommRingHom φ) - where open IsOrderedCommRingHom (snd φ) + isUniqueFromℤOCR = isUniqueFromℤ ∘ OrderedCommRingHom→CommRingHom isUniqueFromℤOCRMono : (φ : OrderedCommRingMono ℤOrderedCommRing R) → ∀ n → R.fromℤ n ≡ fst φ n - isUniqueFromℤOCRMono φ = isUniqueFromℤ (OrderedCommRingMono→CommRingHom φ) - where open IsOrderedCommRingMono (snd φ) + isUniqueFromℤOCRMono = isUniqueFromℤ ∘ OrderedCommRingMono→CommRingHom isContrHom[ℤOCR,-] : isContr (OrderedCommRingHom ℤOrderedCommRing R) fst isContrHom[ℤOCR,-] = fromℤOCR From 3bc2336b70394ffc90d8861e9af3ac6c08ee28f4 Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Tue, 14 Apr 2026 15:46:37 +0200 Subject: [PATCH 14/19] =?UTF-8?q?make=20more=20proofs=20pointfree,=20renam?= =?UTF-8?q?e=20`makeIsOrderedCommRingEquiv`=20=E2=86=92=20`makeIsOrderedCo?= =?UTF-8?q?mmRingEquivFromMono`,=20add=20a=20new=20`makeIsOrderedCommRingE?= =?UTF-8?q?quiv`=20that=20is=20actually=20a=20specialized=20`make`=20(i.e.?= =?UTF-8?q?=20taking=20as=20inputs=20the=20individual=20proofs=20needed=20?= =?UTF-8?q?to=20build=20the=20OCR=20equivalence)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Algebra/OrderedCommRing/Morphisms.agda | 34 +++++++++++++------ .../Algebra/OrderedCommRing/Univalence.agda | 5 ++- 2 files changed, 25 insertions(+), 14 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Morphisms.agda b/Cubical/Algebra/OrderedCommRing/Morphisms.agda index 4e74bb721e..ecc2fcfd3e 100644 --- a/Cubical/Algebra/OrderedCommRing/Morphisms.agda +++ b/Cubical/Algebra/OrderedCommRing/Morphisms.agda @@ -286,9 +286,9 @@ snd (OrderedCommRingEquiv→OrderedCommRingMono e) = isOCRMono isOCRMono .isOCRHom .isCRHom .pres+ = E.pres+ isOCRMono .isOCRHom .isCRHom .pres· = E.pres· isOCRMono .isOCRHom .isCRHom .pres- = E.pres- - isOCRMono .isOCRHom .pres≤ = λ x y → equivFun (E.pres≤ x y) - isOCRMono .isOCRHom .reflect< = λ x y → invEq (E.pres< x y) - isOCRMono .pres< = λ x y → equivFun (E.pres< x y) + isOCRMono .isOCRHom .pres≤ = (equivFun ∘_) ∘ E.pres≤ + isOCRMono .isOCRHom .reflect< = (invEq ∘_) ∘ E.pres< + isOCRMono .pres< = (equivFun ∘_) ∘ E.pres< OrderedCommRingEquiv→OrderedCommRingHom : {A : OrderedCommRing ℓ ℓ<≤} → {B : OrderedCommRing ℓ' ℓ<≤'} @@ -346,15 +346,27 @@ module _ {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} ( open IsOrderedCommRingEquiv - makeIsOrderedCommRingEquiv : IsOrderedCommRingEquiv (str R) e (str S) - makeIsOrderedCommRingEquiv .pres0 = M.pres0 - makeIsOrderedCommRingEquiv .pres1 = M.pres1 - makeIsOrderedCommRingEquiv .pres+ = M.pres+ - makeIsOrderedCommRingEquiv .pres· = M.pres· - makeIsOrderedCommRingEquiv .pres- = M.pres- - makeIsOrderedCommRingEquiv .pres≤ = λ x y → propBiimpl→Equiv + makeIsOrderedCommRingEquivFromMono : IsOrderedCommRingEquiv (str R) e (str S) + makeIsOrderedCommRingEquivFromMono .pres0 = M.pres0 + makeIsOrderedCommRingEquivFromMono .pres1 = M.pres1 + makeIsOrderedCommRingEquivFromMono .pres+ = M.pres+ + makeIsOrderedCommRingEquivFromMono .pres· = M.pres· + makeIsOrderedCommRingEquivFromMono .pres- = M.pres- + makeIsOrderedCommRingEquivFromMono .pres≤ = λ x y → propBiimpl→Equiv (R.is-prop-valued≤ _ _) (S.is-prop-valued≤ _ _) (M.pres≤ x y) (isOrderedCommRingMono→reflect≤ isMono x y) - makeIsOrderedCommRingEquiv .pres< = λ x y → propBiimpl→Equiv + makeIsOrderedCommRingEquivFromMono .pres< = λ x y → propBiimpl→Equiv (R.is-prop-valued< _ _) (S.is-prop-valued< _ _) (M.pres< x y) (M.reflect< x y) + + module _ + (p1 : equivFun e R.1r ≡ S.1r) + (p+ : ∀ x y → equivFun e (x R.+ y) ≡ equivFun e x S.+ equivFun e y) + (p· : ∀ x y → equivFun e (x R.· y) ≡ equivFun e x S.· equivFun e y) + (p< : ∀ x y → x R.< y → equivFun e x S.< equivFun e y) + (p<⁻ : ∀ x y → equivFun e x S.< equivFun e y → x R.< y) + where + + makeIsOrderedCommRingEquiv : IsOrderedCommRingEquiv (str R) e (str S) + makeIsOrderedCommRingEquiv = makeIsOrderedCommRingEquivFromMono + (makeIsOrderedCommRingMono p1 p+ p· p< p<⁻) diff --git a/Cubical/Algebra/OrderedCommRing/Univalence.agda b/Cubical/Algebra/OrderedCommRing/Univalence.agda index 94ced02b7b..ee613ccd6c 100644 --- a/Cubical/Algebra/OrderedCommRing/Univalence.agda +++ b/Cubical/Algebra/OrderedCommRing/Univalence.agda @@ -64,14 +64,13 @@ OrderedCommRingEquivIsoOrderedCommRingIso R S = OCREquivIsoOCRIso fst (fun OCREquivIsoOCRIso e) = equivToIso (fst e) snd (fun OCREquivIsoOCRIso e) = snd (OrderedCommRingEquiv→OrderedCommRingMono e) fst (inv OCREquivIsoOCRIso e) = isoToEquiv (fst e) - snd (inv OCREquivIsoOCRIso e) = makeIsOrderedCommRingEquiv (isoToEquiv (fst e)) (snd e) + snd (inv OCREquivIsoOCRIso e) = makeIsOrderedCommRingEquivFromMono (isoToEquiv (fst e)) (snd e) sec OCREquivIsoOCRIso e = Σ≡Prop (λ f → isPropIsOrderedCommRingMono _ (fun f) _) ( Iso≡Set (OrderedCommRingStr.is-set (snd R)) (OrderedCommRingStr.is-set (snd S)) _ _ (λ x → refl) (λ x → refl)) ret OCREquivIsoOCRIso e = - Σ≡Prop (λ f → isPropIsOrderedCommRingEquiv _ f _) - (equivEq refl) + Σ≡Prop (λ f → isPropIsOrderedCommRingEquiv _ f _) (equivEq refl) isGroupoidOrderedCommRing : isGroupoid (OrderedCommRing ℓ ℓ') isGroupoidOrderedCommRing _ _ = From 1a164965916f79ac4f602d259d6b874be767cd0f Mon Sep 17 00:00:00 2001 From: LorenzoMolena <164308953+LorenzoMolena@users.noreply.github.com> Date: Tue, 14 Apr 2026 15:52:58 +0200 Subject: [PATCH 15/19] Sync with `ocr-update` (#45) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * typo * remove unnecessary imports, make some proofs ~~pointless~~ pointfree * make more proofs pointfree, rename `makeIsOrderedCommRingEquiv` → `makeIsOrderedCommRingEquivFromMono`, add a new `makeIsOrderedCommRingEquiv` that is actually a specialized `make` (i.e. taking as inputs the individual proofs needed to build the OCR equivalence) --- .../Algebra/OrderedCommRing/Morphisms.agda | 34 +++++++++++++------ .../Algebra/OrderedCommRing/Univalence.agda | 5 ++- 2 files changed, 25 insertions(+), 14 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Morphisms.agda b/Cubical/Algebra/OrderedCommRing/Morphisms.agda index 4e74bb721e..ecc2fcfd3e 100644 --- a/Cubical/Algebra/OrderedCommRing/Morphisms.agda +++ b/Cubical/Algebra/OrderedCommRing/Morphisms.agda @@ -286,9 +286,9 @@ snd (OrderedCommRingEquiv→OrderedCommRingMono e) = isOCRMono isOCRMono .isOCRHom .isCRHom .pres+ = E.pres+ isOCRMono .isOCRHom .isCRHom .pres· = E.pres· isOCRMono .isOCRHom .isCRHom .pres- = E.pres- - isOCRMono .isOCRHom .pres≤ = λ x y → equivFun (E.pres≤ x y) - isOCRMono .isOCRHom .reflect< = λ x y → invEq (E.pres< x y) - isOCRMono .pres< = λ x y → equivFun (E.pres< x y) + isOCRMono .isOCRHom .pres≤ = (equivFun ∘_) ∘ E.pres≤ + isOCRMono .isOCRHom .reflect< = (invEq ∘_) ∘ E.pres< + isOCRMono .pres< = (equivFun ∘_) ∘ E.pres< OrderedCommRingEquiv→OrderedCommRingHom : {A : OrderedCommRing ℓ ℓ<≤} → {B : OrderedCommRing ℓ' ℓ<≤'} @@ -346,15 +346,27 @@ module _ {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} ( open IsOrderedCommRingEquiv - makeIsOrderedCommRingEquiv : IsOrderedCommRingEquiv (str R) e (str S) - makeIsOrderedCommRingEquiv .pres0 = M.pres0 - makeIsOrderedCommRingEquiv .pres1 = M.pres1 - makeIsOrderedCommRingEquiv .pres+ = M.pres+ - makeIsOrderedCommRingEquiv .pres· = M.pres· - makeIsOrderedCommRingEquiv .pres- = M.pres- - makeIsOrderedCommRingEquiv .pres≤ = λ x y → propBiimpl→Equiv + makeIsOrderedCommRingEquivFromMono : IsOrderedCommRingEquiv (str R) e (str S) + makeIsOrderedCommRingEquivFromMono .pres0 = M.pres0 + makeIsOrderedCommRingEquivFromMono .pres1 = M.pres1 + makeIsOrderedCommRingEquivFromMono .pres+ = M.pres+ + makeIsOrderedCommRingEquivFromMono .pres· = M.pres· + makeIsOrderedCommRingEquivFromMono .pres- = M.pres- + makeIsOrderedCommRingEquivFromMono .pres≤ = λ x y → propBiimpl→Equiv (R.is-prop-valued≤ _ _) (S.is-prop-valued≤ _ _) (M.pres≤ x y) (isOrderedCommRingMono→reflect≤ isMono x y) - makeIsOrderedCommRingEquiv .pres< = λ x y → propBiimpl→Equiv + makeIsOrderedCommRingEquivFromMono .pres< = λ x y → propBiimpl→Equiv (R.is-prop-valued< _ _) (S.is-prop-valued< _ _) (M.pres< x y) (M.reflect< x y) + + module _ + (p1 : equivFun e R.1r ≡ S.1r) + (p+ : ∀ x y → equivFun e (x R.+ y) ≡ equivFun e x S.+ equivFun e y) + (p· : ∀ x y → equivFun e (x R.· y) ≡ equivFun e x S.· equivFun e y) + (p< : ∀ x y → x R.< y → equivFun e x S.< equivFun e y) + (p<⁻ : ∀ x y → equivFun e x S.< equivFun e y → x R.< y) + where + + makeIsOrderedCommRingEquiv : IsOrderedCommRingEquiv (str R) e (str S) + makeIsOrderedCommRingEquiv = makeIsOrderedCommRingEquivFromMono + (makeIsOrderedCommRingMono p1 p+ p· p< p<⁻) diff --git a/Cubical/Algebra/OrderedCommRing/Univalence.agda b/Cubical/Algebra/OrderedCommRing/Univalence.agda index 94ced02b7b..ee613ccd6c 100644 --- a/Cubical/Algebra/OrderedCommRing/Univalence.agda +++ b/Cubical/Algebra/OrderedCommRing/Univalence.agda @@ -64,14 +64,13 @@ OrderedCommRingEquivIsoOrderedCommRingIso R S = OCREquivIsoOCRIso fst (fun OCREquivIsoOCRIso e) = equivToIso (fst e) snd (fun OCREquivIsoOCRIso e) = snd (OrderedCommRingEquiv→OrderedCommRingMono e) fst (inv OCREquivIsoOCRIso e) = isoToEquiv (fst e) - snd (inv OCREquivIsoOCRIso e) = makeIsOrderedCommRingEquiv (isoToEquiv (fst e)) (snd e) + snd (inv OCREquivIsoOCRIso e) = makeIsOrderedCommRingEquivFromMono (isoToEquiv (fst e)) (snd e) sec OCREquivIsoOCRIso e = Σ≡Prop (λ f → isPropIsOrderedCommRingMono _ (fun f) _) ( Iso≡Set (OrderedCommRingStr.is-set (snd R)) (OrderedCommRingStr.is-set (snd S)) _ _ (λ x → refl) (λ x → refl)) ret OCREquivIsoOCRIso e = - Σ≡Prop (λ f → isPropIsOrderedCommRingEquiv _ f _) - (equivEq refl) + Σ≡Prop (λ f → isPropIsOrderedCommRingEquiv _ f _) (equivEq refl) isGroupoidOrderedCommRing : isGroupoid (OrderedCommRing ℓ ℓ') isGroupoidOrderedCommRing _ _ = From 5f7a8d674cabaca9b8252b3a6fcd6e9ba5e7e916 Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Fri, 17 Apr 2026 20:40:23 +0200 Subject: [PATCH 16/19] avoid reexporting publicly too many properties --- Cubical/Algebra/OrderedCommRing/Properties.agda | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index c8625a7fe8..eb1ea38212 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -425,7 +425,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where isSG .IsSemigroup.is-set = isSetR₊ isSG .IsSemigroup.·Assoc = λ _ _ _ → R₊≡ (+Assoc _ _ _) - open SemigroupStr (snd R₊AdditiveSemigroup) public hiding (_·_) renaming ( + open SemigroupStr (snd R₊AdditiveSemigroup) using () public renaming ( ·Assoc to +₊Assoc) R₊MultiplicativeCommMonoid : CommMonoid _ @@ -439,7 +439,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where (λ _ → R₊≡ (·IdR _)) (λ _ _ → R₊≡ (·Comm _ _)) - open CommMonoidStr (snd R₊MultiplicativeCommMonoid) public hiding (_·_) renaming ( + open CommMonoidStr (snd R₊MultiplicativeCommMonoid) using () public renaming ( ε to 1₊ ; ·Assoc to ·₊Assoc ; ·IdR to ·₊IdR ; ·Comm to ·₊Comm) selfSeparated : ∀ (x y : R) → (∀ (z : R₊) → abs(x - y) < ⟨ z ⟩₊) → x ≡ y @@ -524,8 +524,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where (λ _ → R₀₊≡ (0LeftAnnihilates _)) (λ _ _ → R₀₊≡ (·Comm _ _)) - open CommSemiringStr (snd R₀₊CommSemiring) public hiding (_+_ ; _·_) - renaming ( + open CommSemiringStr (snd R₀₊CommSemiring) using () public renaming ( 0r to 0₀₊ ; 1r to 1₀₊ ; +Assoc to +₀₊Assoc ; +IdL to +₀₊IdL ; +IdR to +₀₊IdR ; +Comm to +₀₊Comm ; ·Assoc to ·₀₊Assoc ; ·IdL to ·₀₊IdL ; ·IdR to ·₀₊IdR ; ·Comm to ·₀₊Comm From cf249e4d0ed9af9d13ed8da5af25bad2d99b8d4e Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Fri, 17 Apr 2026 20:40:23 +0200 Subject: [PATCH 17/19] avoid reexporting publicly too many properties --- Cubical/Algebra/OrderedCommRing/Properties.agda | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Properties.agda b/Cubical/Algebra/OrderedCommRing/Properties.agda index c8625a7fe8..eb1ea38212 100644 --- a/Cubical/Algebra/OrderedCommRing/Properties.agda +++ b/Cubical/Algebra/OrderedCommRing/Properties.agda @@ -425,7 +425,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where isSG .IsSemigroup.is-set = isSetR₊ isSG .IsSemigroup.·Assoc = λ _ _ _ → R₊≡ (+Assoc _ _ _) - open SemigroupStr (snd R₊AdditiveSemigroup) public hiding (_·_) renaming ( + open SemigroupStr (snd R₊AdditiveSemigroup) using () public renaming ( ·Assoc to +₊Assoc) R₊MultiplicativeCommMonoid : CommMonoid _ @@ -439,7 +439,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where (λ _ → R₊≡ (·IdR _)) (λ _ _ → R₊≡ (·Comm _ _)) - open CommMonoidStr (snd R₊MultiplicativeCommMonoid) public hiding (_·_) renaming ( + open CommMonoidStr (snd R₊MultiplicativeCommMonoid) using () public renaming ( ε to 1₊ ; ·Assoc to ·₊Assoc ; ·IdR to ·₊IdR ; ·Comm to ·₊Comm) selfSeparated : ∀ (x y : R) → (∀ (z : R₊) → abs(x - y) < ⟨ z ⟩₊) → x ≡ y @@ -524,8 +524,7 @@ module _ (R' : OrderedCommRing ℓ ℓ') where (λ _ → R₀₊≡ (0LeftAnnihilates _)) (λ _ _ → R₀₊≡ (·Comm _ _)) - open CommSemiringStr (snd R₀₊CommSemiring) public hiding (_+_ ; _·_) - renaming ( + open CommSemiringStr (snd R₀₊CommSemiring) using () public renaming ( 0r to 0₀₊ ; 1r to 1₀₊ ; +Assoc to +₀₊Assoc ; +IdL to +₀₊IdL ; +IdR to +₀₊IdR ; +Comm to +₀₊Comm ; ·Assoc to ·₀₊Assoc ; ·IdL to ·₀₊IdL ; ·IdR to ·₀₊IdR ; ·Comm to ·₀₊Comm From e05d63c7507e8436f788a93793bde654d091fa89 Mon Sep 17 00:00:00 2001 From: Lorenzo Molena Date: Tue, 21 Apr 2026 21:49:38 +0200 Subject: [PATCH 18/19] Revert "Merge branch 'premetric+fast-rationals' into ocr-update" This reverts commit 312f5053de8f472ceffae4642ead5290b8e9b79a, reversing changes made to 207e123164fefb0633306f957eaf989465caf84f. --- .../Algebra/CommRing/Instances/Rationals.agda | 1 + .../Algebra/Field/Instances/Rationals.agda | 33 +- .../OrderedCommRing/Instances/Rationals.agda | 187 ----------- Cubical/Data/Rationals/Base.agda | 2 +- Cubical/Data/Rationals/Order.agda | 311 ++++++++---------- Cubical/Data/Rationals/Properties.agda | 121 +------ .../Order/Loset/Instances/Rationals.agda | 31 -- .../Order/Poset/Instances/Rationals.agda | 11 - .../Order/Proset/Instances/Rationals.agda | 11 - .../Pseudolattice/Instances/Rationals.agda | 19 -- .../Order/Quoset/Instances/Rationals.agda | 11 - .../StrictOrder/Instances/Rationals.agda | 11 - .../Order/Toset/Instances/Rationals.agda | 31 -- Cubical/Relation/Premetric.agda | 3 - Cubical/Relation/Premetric/Base.agda | 73 ---- 15 files changed, 183 insertions(+), 673 deletions(-) delete mode 100644 Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Binary/Order/Loset/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Binary/Order/Poset/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Binary/Order/Proset/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Binary/Order/Pseudolattice/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Binary/Order/Quoset/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Binary/Order/StrictOrder/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Binary/Order/Toset/Instances/Rationals.agda delete mode 100644 Cubical/Relation/Premetric.agda delete mode 100644 Cubical/Relation/Premetric/Base.agda diff --git a/Cubical/Algebra/CommRing/Instances/Rationals.agda b/Cubical/Algebra/CommRing/Instances/Rationals.agda index eeb40346c9..92416ac328 100644 --- a/Cubical/Algebra/CommRing/Instances/Rationals.agda +++ b/Cubical/Algebra/CommRing/Instances/Rationals.agda @@ -20,3 +20,4 @@ open import Cubical.Data.Rationals as ℚ where p : IsCommRing 0 1 _+_ _·_ (-_) p = makeIsCommRing isSetℚ +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistL+ ·Comm + diff --git a/Cubical/Algebra/Field/Instances/Rationals.agda b/Cubical/Algebra/Field/Instances/Rationals.agda index fa3bfadbd4..2209eb5f03 100644 --- a/Cubical/Algebra/Field/Instances/Rationals.agda +++ b/Cubical/Algebra/Field/Instances/Rationals.agda @@ -14,7 +14,7 @@ open import Cubical.Algebra.CommRing.Instances.Rationals open import Cubical.Algebra.Field open import Cubical.Data.Empty as Empty -open import Cubical.Data.Fast.Int as ℤ +open import Cubical.Data.Int as ℤ open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc) open import Cubical.Data.NatPlusOne open import Cubical.Data.Rationals as ℚ @@ -42,9 +42,36 @@ hasInverseℚ = SetQuotients.elimProp q (ℤ.pos zero , b) p = Empty.rec (p (numerator0→0 ((ℤ.pos zero , b)) refl)) q (ℤ.pos (suc n) , (1+ m)) _ = - eq/ _ _ (ℤ.·IdR _ ∙∙ ℤ.·Comm (pos (suc n)) (pos (suc m)) ∙∙ sym (ℤ.·IdL _)) + eq/ ((ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m)) , (1+ m) ·₊₁ (1+ n))) ((1 , 1)) q' + where + q' = (ℤ.pos (suc n) ℤ.· (ℕ₊₁→ℤ (1+ m))) ℤ.· 1 + ≡⟨ ℤ.·IdR _ ⟩ + ℤ.pos (suc n) ℤ.· ℤ.pos (suc m) + ≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩ + ℤ.pos ((suc n) ℕ.· (suc m)) + ≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩ + ℤ.pos ((suc m) ℕ.· (suc n)) + ≡⟨ refl ⟩ + ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n)) + ≡⟨ sym (ℤ.·IdL _) ⟩ + 1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎ q (ℤ.negsuc n , (1+ m)) _ = - eq/ _ _ (ℤ.·IdR _ ∙∙ ℤ.·Comm (pos (suc n)) (pos (suc m)) ∙∙ sym (ℤ.·IdL _)) + eq/ ((ℤ.negsuc n ℤ.· ℤ.negsuc m) , ((1+ m) ·₊₁ (1+ n))) ((1 , 1)) q' + where + q' : (ℤ.negsuc n ℤ.· ℤ.negsuc m , (1+ m) ·₊₁ (1+ n)) ∼ (1 , 1) + q' = (ℤ.negsuc n ℤ.· ℤ.negsuc m) ℤ.· 1 + ≡⟨ ℤ.·IdR _ ⟩ + (ℤ.negsuc n ℤ.· ℤ.negsuc m) + ≡⟨ negsuc·negsuc n m ⟩ + (ℤ.pos (suc n) ℤ.· ℤ.pos (suc m)) + ≡⟨ sym $ ℤ.pos·pos (suc n) (suc m) ⟩ + ℤ.pos ((suc n) ℕ.· (suc m)) + ≡⟨ cong ℤ.pos (ℕ.·-comm (suc n) (suc m)) ⟩ + ℤ.pos ((suc m) ℕ.· (suc n)) + ≡⟨ refl ⟩ + ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n)) + ≡⟨ sym (ℤ.·IdL _) ⟩ + 1 ℤ.· (ℕ₊₁→ℤ ((1+ m) ·₊₁ (1+ n))) ∎ 0≢1-ℚ : ¬ Path ℚ 0 1 0≢1-ℚ p = 0≢1-ℤ (effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ p) diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda b/Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda deleted file mode 100644 index 600f38c22a..0000000000 --- a/Cubical/Algebra/OrderedCommRing/Instances/Rationals.agda +++ /dev/null @@ -1,187 +0,0 @@ -module Cubical.Algebra.OrderedCommRing.Instances.Rationals where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Function -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Equiv - -open import Cubical.Data.Empty as ⊥ - -open import Cubical.HITs.PropositionalTruncation as PT -open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _//_) - -open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_) -open import Cubical.Data.NatPlusOne as ℕ₊₁ -open import Cubical.Data.Fast.Int as ℤ hiding (_+_ ; _-_ ; -_ ; _·_) -import Cubical.Data.Fast.Int.Order as ℤ - -open import Cubical.Data.Rationals as ℚ - renaming (_+_ to _+ℚ_ ; _-_ to _-ℚ_; -_ to -ℚ_ ; _·_ to _·ℚ_) -open import Cubical.Data.Rationals.Order as ℚ - renaming (_<_ to _<ℚ_ ; _≤_ to _≤ℚ_) - -open import Cubical.Algebra.CommRing -open import Cubical.Algebra.CommRing.Instances.Rationals - -open import Cubical.Algebra.OrderedCommRing.Base -open import Cubical.Algebra.OrderedCommRing.Properties - -open import Cubical.Relation.Nullary - -open import Cubical.Relation.Binary.Order.StrictOrder -open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Rationals - -open import Cubical.Relation.Binary.Order.Pseudolattice -open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Rationals - -open CommRingStr -open OrderedCommRingStr -open PseudolatticeStr -open StrictOrderStr - -ℚOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero -fst ℚOrderedCommRing = ℚ -0r (snd ℚOrderedCommRing) = 0 -1r (snd ℚOrderedCommRing) = 1 -_+_ (snd ℚOrderedCommRing) = _+ℚ_ -_·_ (snd ℚOrderedCommRing) = _·ℚ_ --_ (snd ℚOrderedCommRing) = -ℚ_ -_<_ (snd ℚOrderedCommRing) = _<ℚ_ -_≤_ (snd ℚOrderedCommRing) = _≤ℚ_ -isOrderedCommRing (snd ℚOrderedCommRing) = isOrderedCommRingℚ - where - open IsOrderedCommRing - - isOrderedCommRingℚ : IsOrderedCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_ _<ℚ_ _≤ℚ_ - isOrderedCommRingℚ .isCommRing = ℚCommRing .snd .isCommRing - isOrderedCommRingℚ .isPseudolattice = ℚ≤Pseudolattice .snd .is-pseudolattice - isOrderedCommRingℚ .isStrictOrder = ℚ = λ x y → - propBiimpl→Equiv (isProp≤ x y) (isProp¬ (y <ℚ x)) (≤→≯ x y) (≮→≥ y x) - isOrderedCommRingℚ .+MonoR≤ = ≤-+o - isOrderedCommRingℚ .+MonoR< = <-+o - isOrderedCommRingℚ .posSum→pos∨pos = λ x y → ∣_∣₁ ∘ 0<+ x y - isOrderedCommRingℚ .<-≤-trans = isTrans<≤ - isOrderedCommRingℚ .≤-<-trans = isTrans≤< - isOrderedCommRingℚ .·MonoR≤ = ≤-·o - isOrderedCommRingℚ .·MonoR< = <-·o - isOrderedCommRingℚ .0<1 = pos n) -≤→≯ m n m≤n = recompute¬< $ - λ n Date: Tue, 21 Apr 2026 22:05:00 +0200 Subject: [PATCH 19/19] add missing `Is` into the name of an helper function --- Cubical/Algebra/OrderedCommRing/Morphisms.agda | 18 +++++++++--------- .../Algebra/OrderedCommRing/Univalence.agda | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Cubical/Algebra/OrderedCommRing/Morphisms.agda b/Cubical/Algebra/OrderedCommRing/Morphisms.agda index ecc2fcfd3e..09bb5c8684 100644 --- a/Cubical/Algebra/OrderedCommRing/Morphisms.agda +++ b/Cubical/Algebra/OrderedCommRing/Morphisms.agda @@ -346,16 +346,16 @@ module _ {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} ( open IsOrderedCommRingEquiv - makeIsOrderedCommRingEquivFromMono : IsOrderedCommRingEquiv (str R) e (str S) - makeIsOrderedCommRingEquivFromMono .pres0 = M.pres0 - makeIsOrderedCommRingEquivFromMono .pres1 = M.pres1 - makeIsOrderedCommRingEquivFromMono .pres+ = M.pres+ - makeIsOrderedCommRingEquivFromMono .pres· = M.pres· - makeIsOrderedCommRingEquivFromMono .pres- = M.pres- - makeIsOrderedCommRingEquivFromMono .pres≤ = λ x y → propBiimpl→Equiv + makeIsOrderedCommRingEquivFromIsMono : IsOrderedCommRingEquiv (str R) e (str S) + makeIsOrderedCommRingEquivFromIsMono .pres0 = M.pres0 + makeIsOrderedCommRingEquivFromIsMono .pres1 = M.pres1 + makeIsOrderedCommRingEquivFromIsMono .pres+ = M.pres+ + makeIsOrderedCommRingEquivFromIsMono .pres· = M.pres· + makeIsOrderedCommRingEquivFromIsMono .pres- = M.pres- + makeIsOrderedCommRingEquivFromIsMono .pres≤ = λ x y → propBiimpl→Equiv (R.is-prop-valued≤ _ _) (S.is-prop-valued≤ _ _) (M.pres≤ x y) (isOrderedCommRingMono→reflect≤ isMono x y) - makeIsOrderedCommRingEquivFromMono .pres< = λ x y → propBiimpl→Equiv + makeIsOrderedCommRingEquivFromIsMono .pres< = λ x y → propBiimpl→Equiv (R.is-prop-valued< _ _) (S.is-prop-valued< _ _) (M.pres< x y) (M.reflect< x y) @@ -368,5 +368,5 @@ module _ {R : OrderedCommRing ℓ ℓ<≤} {S : OrderedCommRing ℓ' ℓ<≤'} ( where makeIsOrderedCommRingEquiv : IsOrderedCommRingEquiv (str R) e (str S) - makeIsOrderedCommRingEquiv = makeIsOrderedCommRingEquivFromMono + makeIsOrderedCommRingEquiv = makeIsOrderedCommRingEquivFromIsMono (makeIsOrderedCommRingMono p1 p+ p· p< p<⁻) diff --git a/Cubical/Algebra/OrderedCommRing/Univalence.agda b/Cubical/Algebra/OrderedCommRing/Univalence.agda index ee613ccd6c..a34fe37db5 100644 --- a/Cubical/Algebra/OrderedCommRing/Univalence.agda +++ b/Cubical/Algebra/OrderedCommRing/Univalence.agda @@ -64,7 +64,7 @@ OrderedCommRingEquivIsoOrderedCommRingIso R S = OCREquivIsoOCRIso fst (fun OCREquivIsoOCRIso e) = equivToIso (fst e) snd (fun OCREquivIsoOCRIso e) = snd (OrderedCommRingEquiv→OrderedCommRingMono e) fst (inv OCREquivIsoOCRIso e) = isoToEquiv (fst e) - snd (inv OCREquivIsoOCRIso e) = makeIsOrderedCommRingEquivFromMono (isoToEquiv (fst e)) (snd e) + snd (inv OCREquivIsoOCRIso e) = makeIsOrderedCommRingEquivFromIsMono (isoToEquiv (fst e)) (snd e) sec OCREquivIsoOCRIso e = Σ≡Prop (λ f → isPropIsOrderedCommRingMono _ (fun f) _) ( Iso≡Set (OrderedCommRingStr.is-set (snd R)) (OrderedCommRingStr.is-set (snd S))