From 21ddf92608a4538bcdef02d27de8bd373c5f7cfb Mon Sep 17 00:00:00 2001 From: Matthias Hutzler Date: Fri, 25 Aug 2023 09:08:46 +0200 Subject: [PATCH] simplify isSet (#1033) * export is-set only once from AlgebraStr * harmonize IsOrderedCommMonoid, hide second is-set * harmonize all isSet in Algebra * two small fixes --- Cubical/Algebra/AbGroup/Base.agda | 2 +- Cubical/Algebra/Algebra/Base.agda | 7 +++++-- Cubical/Algebra/CommAlgebra/Base.agda | 4 +++- Cubical/Algebra/CommMonoid/Base.agda | 14 +++----------- Cubical/Algebra/CommMonoid/Properties.agda | 2 +- Cubical/Algebra/CommRing/Base.agda | 4 +++- Cubical/Algebra/DistLattice/Base.agda | 4 +++- Cubical/Algebra/Field/Base.agda | 4 +++- Cubical/Algebra/Group/Base.agda | 4 +++- Cubical/Algebra/Lattice/Base.agda | 4 +++- Cubical/Algebra/Module/Base.agda | 4 +++- Cubical/Algebra/OrderedCommMonoid/Base.agda | 14 +++++++++----- Cubical/Algebra/Ring/Base.agda | 4 +++- 13 files changed, 43 insertions(+), 28 deletions(-) diff --git a/Cubical/Algebra/AbGroup/Base.agda b/Cubical/Algebra/AbGroup/Base.agda index ce03b130e2..718f8138e5 100644 --- a/Cubical/Algebra/AbGroup/Base.agda +++ b/Cubical/Algebra/AbGroup/Base.agda @@ -139,7 +139,7 @@ module _ ((G , abgroupstr _ _ _ GisGroup) : AbGroup ℓ) where AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.·Comm = IsAbGroup.+Comm GisGroup isSetAbGroup : (A : AbGroup ℓ) → isSet ⟨ A ⟩ -isSetAbGroup A = isSetGroup (AbGroup→Group A) +isSetAbGroup A = is-set (str A) AbGroupHom : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ') AbGroupHom G H = GroupHom (AbGroup→Group G) (AbGroup→Group H) diff --git a/Cubical/Algebra/Algebra/Base.agda b/Cubical/Algebra/Algebra/Base.agda index d4af8c8fb8..372feb7680 100644 --- a/Cubical/Algebra/Algebra/Base.agda +++ b/Cubical/Algebra/Algebra/Base.agda @@ -52,7 +52,8 @@ record IsAlgebra (R : Ring ℓ) {A : Type ℓ'} isRing : IsRing _ _ _ _ _ isRing = isring (IsLeftModule.+IsAbGroup +IsLeftModule) ·IsMonoid ·DistR+ ·DistL+ - open IsRing isRing public hiding (_-_; +Assoc; +IdL; +InvL; +IdR; +InvR; +Comm ; ·DistR+ ; ·DistL+) + open IsRing isRing public + hiding (_-_; +Assoc; +IdL; +InvL; +IdR; +InvR; +Comm; ·DistR+; ·DistL+; is-set) unquoteDecl IsAlgebraIsoΣ = declareRecordIsoΣ IsAlgebraIsoΣ (quote IsAlgebra) @@ -111,7 +112,9 @@ module commonExtractors {R : Ring ℓ} where Algebra→MultMonoid A = Ring→MultMonoid (Algebra→Ring A) isSetAlgebra : (A : Algebra R ℓ') → isSet ⟨ A ⟩ - isSetAlgebra A = isSetAbGroup (Algebra→AbGroup A) + isSetAlgebra A = is-set + where + open AlgebraStr (str A) open RingStr (snd R) using (1r; ·DistL+) renaming (_+_ to _+r_; _·_ to _·s_) diff --git a/Cubical/Algebra/CommAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/Base.agda index 21f22c90af..a0fff564c8 100644 --- a/Cubical/Algebra/CommAlgebra/Base.agda +++ b/Cubical/Algebra/CommAlgebra/Base.agda @@ -78,7 +78,9 @@ module _ {R : CommRing ℓ} where _ , commringstr _ _ _ _ _ (iscommring (IsAlgebra.isRing isAlgebra) ·-comm) isSetCommAlgebra : (A : CommAlgebra R ℓ') → isSet ⟨ A ⟩ - isSetCommAlgebra A = isSetAlgebra (CommAlgebra→Algebra A) + isSetCommAlgebra A = is-set + where + open CommAlgebraStr (str A) module _ {A : Type ℓ'} {0a 1a : A} diff --git a/Cubical/Algebra/CommMonoid/Base.agda b/Cubical/Algebra/CommMonoid/Base.agda index 9eea807746..9f643a768a 100644 --- a/Cubical/Algebra/CommMonoid/Base.agda +++ b/Cubical/Algebra/CommMonoid/Base.agda @@ -81,18 +81,10 @@ CommMonoidStr→MonoidStr (commmonoidstr _ _ H) = monoidstr _ _ (IsCommMonoid.is CommMonoid→Monoid : CommMonoid ℓ → Monoid ℓ CommMonoid→Monoid (_ , commmonoidstr _ _ M) = _ , monoidstr _ _ (IsCommMonoid.isMonoid M) -isSetFromIsCommMonoid : - {M : Type ℓ} {ε : M} {_·_ : M → M → M} - (isCommMonoid : IsCommMonoid ε _·_) - → isSet M -isSetFromIsCommMonoid isCommMonoid = - let open IsCommMonoid isCommMonoid - in is-set - isSetCommMonoid : (M : CommMonoid ℓ) → isSet ⟨ M ⟩ -isSetCommMonoid M = - let open CommMonoidStr (snd M) - in isSetFromIsCommMonoid isCommMonoid +isSetCommMonoid M = is-set + where + open CommMonoidStr (str M) CommMonoidHom : (L : CommMonoid ℓ) (M : CommMonoid ℓ') → Type (ℓ-max ℓ ℓ') CommMonoidHom L M = MonoidHom (CommMonoid→Monoid L) (CommMonoid→Monoid M) diff --git a/Cubical/Algebra/CommMonoid/Properties.agda b/Cubical/Algebra/CommMonoid/Properties.agda index 40ee5bc4ef..4926c3dc0b 100644 --- a/Cubical/Algebra/CommMonoid/Properties.agda +++ b/Cubical/Algebra/CommMonoid/Properties.agda @@ -33,7 +33,7 @@ module _ (x · y) , ·Closed x y xContained yContained IsCommMonoid.isMonoid (CommMonoidStr.isCommMonoid (snd makeSubCommMonoid)) = makeIsMonoid - (isOfHLevelΣ 2 (isSetFromIsCommMonoid isCommMonoid) λ _ → isProp→isSet (snd (P _))) + (isOfHLevelΣ 2 is-set λ _ → isProp→isSet (snd (P _))) (λ x y z → Σ≡Prop (λ _ → snd (P _)) (·Assoc (fst x) (fst y) (fst z))) (λ x → Σ≡Prop (λ _ → snd (P _)) (·IdR (fst x))) λ x → Σ≡Prop (λ _ → snd (P _)) (·IdL (fst x)) diff --git a/Cubical/Algebra/CommRing/Base.agda b/Cubical/Algebra/CommRing/Base.agda index d424a465d9..6a481ca443 100644 --- a/Cubical/Algebra/CommRing/Base.agda +++ b/Cubical/Algebra/CommRing/Base.agda @@ -156,7 +156,9 @@ uaCommRing : {A B : CommRing ℓ} → CommRingEquiv A B → A ≡ B uaCommRing {A = A} {B = B} = equivFun (CommRingPath A B) isSetCommRing : ((R , str) : CommRing ℓ) → isSet R -isSetCommRing (R , str) = str .CommRingStr.is-set +isSetCommRing R = is-set + where + open CommRingStr (str R) CommRingIso : (R : CommRing ℓ) (S : CommRing ℓ') → Type (ℓ-max ℓ ℓ') CommRingIso R S = Σ[ e ∈ Iso (R .fst) (S .fst) ] diff --git a/Cubical/Algebra/DistLattice/Base.agda b/Cubical/Algebra/DistLattice/Base.agda index a0bfba41a9..37c1b5a5f7 100644 --- a/Cubical/Algebra/DistLattice/Base.agda +++ b/Cubical/Algebra/DistLattice/Base.agda @@ -75,7 +75,9 @@ DistLattice : ∀ ℓ → Type (ℓ-suc ℓ) DistLattice ℓ = TypeWithStr ℓ DistLatticeStr isSetDistLattice : (L : DistLattice ℓ) → isSet ⟨ L ⟩ -isSetDistLattice L = L .snd .DistLatticeStr.is-set +isSetDistLattice L = is-set + where + open DistLatticeStr (str L) -- when proving the axioms for a distributive lattice -- we use the fact that from distributivity and absorption diff --git a/Cubical/Algebra/Field/Base.agda b/Cubical/Algebra/Field/Base.agda index 862721873d..c2406af2f3 100644 --- a/Cubical/Algebra/Field/Base.agda +++ b/Cubical/Algebra/Field/Base.agda @@ -75,7 +75,9 @@ Field : ∀ ℓ → Type (ℓ-suc ℓ) Field ℓ = TypeWithStr ℓ FieldStr isSetField : (R : Field ℓ) → isSet ⟨ R ⟩ -isSetField R = R .snd .FieldStr.isField .IsField.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set +isSetField R = is-set + where + open FieldStr (str R) makeIsField : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R} diff --git a/Cubical/Algebra/Group/Base.agda b/Cubical/Algebra/Group/Base.agda index b209bc5d14..1b2a6cac5f 100644 --- a/Cubical/Algebra/Group/Base.agda +++ b/Cubical/Algebra/Group/Base.agda @@ -56,7 +56,9 @@ group : (G : Type ℓ) (1g : G) (_·_ : G → G → G) (inv : G → G) (h : IsGr group G 1g _·_ inv h = G , groupstr 1g _·_ inv h isSetGroup : (G : Group ℓ) → isSet ⟨ G ⟩ -isSetGroup G = GroupStr.isGroup (snd G) .IsGroup.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set +isSetGroup G = is-set + where + open GroupStr (str G) makeIsGroup : {G : Type ℓ} {e : G} {_·_ : G → G → G} { inv : G → G} (is-setG : isSet G) diff --git a/Cubical/Algebra/Lattice/Base.agda b/Cubical/Algebra/Lattice/Base.agda index b6a486669d..7782c8b5df 100644 --- a/Cubical/Algebra/Lattice/Base.agda +++ b/Cubical/Algebra/Lattice/Base.agda @@ -94,7 +94,9 @@ Lattice : ∀ ℓ → Type (ℓ-suc ℓ) Lattice ℓ = TypeWithStr ℓ LatticeStr isSetLattice : (L : Lattice ℓ) → isSet ⟨ L ⟩ -isSetLattice L = L .snd .LatticeStr.is-set +isSetLattice L = is-set + where + open LatticeStr (str L) makeIsLattice : {L : Type ℓ} {0l 1l : L} {_∨l_ _∧l_ : L → L → L} (is-setL : isSet L) diff --git a/Cubical/Algebra/Module/Base.agda b/Cubical/Algebra/Module/Base.agda index 4c3a90e0c0..46a0c27e70 100644 --- a/Cubical/Algebra/Module/Base.agda +++ b/Cubical/Algebra/Module/Base.agda @@ -84,7 +84,9 @@ module _ {R : Ring ℓ} where LeftModule→Group = AbGroup→Group LeftModule→AbGroup isSetLeftModule : (M : LeftModule R ℓ') → isSet ⟨ M ⟩ - isSetLeftModule M = isSetAbGroup (LeftModule→AbGroup M) + isSetLeftModule M = is-set + where + open LeftModuleStr (str M) open RingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_) diff --git a/Cubical/Algebra/OrderedCommMonoid/Base.agda b/Cubical/Algebra/OrderedCommMonoid/Base.agda index 538d01612b..39856573d7 100644 --- a/Cubical/Algebra/OrderedCommMonoid/Base.agda +++ b/Cubical/Algebra/OrderedCommMonoid/Base.agda @@ -6,7 +6,7 @@ module Cubical.Algebra.OrderedCommMonoid.Base where open import Cubical.Foundations.Prelude open import Cubical.Foundations.SIP using (TypeWithStr) -open import Cubical.Foundations.Structure using (⟨_⟩) +open import Cubical.Foundations.Structure using (⟨_⟩; str) open import Cubical.Algebra.CommMonoid.Base @@ -26,6 +26,10 @@ record IsOrderedCommMonoid MonotoneR : {x y z : M} → x ≤ y → (x · z) ≤ (y · z) -- both versions, just for convenience MonotoneL : {x y z : M} → x ≤ y → (z · x) ≤ (z · y) + open IsPoset isPoset public + open IsCommMonoid isCommMonoid public + hiding (is-set) + record OrderedCommMonoidStr (ℓ' : Level) (M : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where field _≤_ : M → M → Type ℓ' @@ -34,8 +38,6 @@ record OrderedCommMonoidStr (ℓ' : Level) (M : Type ℓ) : Type (ℓ-suc (ℓ-m isOrderedCommMonoid : IsOrderedCommMonoid _·_ ε _≤_ open IsOrderedCommMonoid isOrderedCommMonoid public - open IsPoset isPoset public - open IsCommMonoid isCommMonoid public infixl 4 _≤_ @@ -78,7 +80,7 @@ module _ IsOrderedCommMonoidFromIsCommMonoid : IsOrderedCommMonoid _·_ 1m _≤_ CM.isPoset IsOrderedCommMonoidFromIsCommMonoid = - isposet (isSetFromIsCommMonoid isCommMonoid) isProp≤ isRefl isTrans isAntisym + isposet (IsCommMonoid.is-set isCommMonoid) isProp≤ isRefl isTrans isAntisym CM.isCommMonoid IsOrderedCommMonoidFromIsCommMonoid = isCommMonoid CM.MonotoneR IsOrderedCommMonoidFromIsCommMonoid = rmonotone _ _ _ CM.MonotoneL IsOrderedCommMonoidFromIsCommMonoid = lmonotone _ _ _ @@ -90,4 +92,6 @@ OrderedCommMonoid→CommMonoid M .snd = in commmonoidstr _ _ isCommMonoid isSetOrderedCommMonoid : (M : OrderedCommMonoid ℓ ℓ') → isSet ⟨ M ⟩ -isSetOrderedCommMonoid M = isSetCommMonoid (OrderedCommMonoid→CommMonoid M) +isSetOrderedCommMonoid M = is-set + where + open OrderedCommMonoidStr (str M) diff --git a/Cubical/Algebra/Ring/Base.agda b/Cubical/Algebra/Ring/Base.agda index f998348d26..d3db28be08 100644 --- a/Cubical/Algebra/Ring/Base.agda +++ b/Cubical/Algebra/Ring/Base.agda @@ -82,7 +82,9 @@ Ring : ∀ ℓ → Type (ℓ-suc ℓ) Ring ℓ = TypeWithStr ℓ RingStr isSetRing : (R : Ring ℓ) → isSet ⟨ R ⟩ -isSetRing R = R .snd .RingStr.isRing .IsRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set +isSetRing R = is-set + where + open RingStr (str R) module _ {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R} (is-setR : isSet R)