simplify isSet<SomeAlgebraicStructure> (#1033)

* export is-set only once from AlgebraStr

* harmonize IsOrderedCommMonoid, hide second is-set

* harmonize all isSet<Something> in Algebra

* two small fixes

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)

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_)
 

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}

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)

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))

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) ]

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

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}

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)

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)

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_)
 

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)

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)