diff --git a/Cubical/Algebra/AbGroup/Base.agda b/Cubical/Algebra/AbGroup/Base.agda
index 718f8138e5..eb86373396 100644
--- a/Cubical/Algebra/AbGroup/Base.agda
+++ b/Cubical/Algebra/AbGroup/Base.agda
@@ -138,9 +138,6 @@ module _ ((G , abgroupstr _ _ _ GisGroup) : AbGroup ℓ) where
   AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.isMonoid = IsAbGroup.isMonoid GisGroup
   AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.·Comm = IsAbGroup.+Comm GisGroup
 
-isSetAbGroup : (A : AbGroup ℓ) → isSet ⟨ 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 372feb7680..97afcced0f 100644
--- a/Cubical/Algebra/Algebra/Base.agda
+++ b/Cubical/Algebra/Algebra/Base.agda
@@ -111,11 +111,6 @@ module commonExtractors {R : Ring ℓ} where
   Algebra→MultMonoid : (A : Algebra R ℓ') → Monoid ℓ'
   Algebra→MultMonoid A = Ring→MultMonoid (Algebra→Ring A)
 
-  isSetAlgebra : (A : Algebra R ℓ') → isSet ⟨ A ⟩
-  isSetAlgebra A = is-set
-    where
-    open AlgebraStr (str A)
-
   open RingStr (snd R) using (1r; ·DistL+) renaming (_+_ to _+r_; _·_ to _·s_)
 
   module _ {A : Type ℓ'} {0a 1a : A}
@@ -214,23 +209,30 @@ isPropIsAlgebraHom : (R : Ring ℓ) {A : Type ℓ'} {B : Type ℓ''}
                      (AS : AlgebraStr R A) (f : A → B) (BS : AlgebraStr R B)
                    → isProp (IsAlgebraHom AS f BS)
 isPropIsAlgebraHom R AS f BS = isOfHLevelRetractFromIso 1 IsAlgebraHomIsoΣ
-                               (isProp×5 (isSetAlgebra (_ , BS) _ _)
-                                         (isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ λ _ → isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _))
+                               (isProp×5 (is-set _ _)
+                                         (is-set _ _)
+                                         (isPropΠ2 λ _ _ → is-set _ _)
+                                         (isPropΠ2 λ _ _ → is-set _ _)
+                                         (isPropΠ λ _ → is-set _ _)
+                                         (isPropΠ2 λ _ _ → is-set _ _))
+  where
+  open AlgebraStr BS
 
 isSetAlgebraHom : (M : Algebra R ℓ') (N : Algebra R ℓ'')
                 → isSet (AlgebraHom M N)
-isSetAlgebraHom _ N = isSetΣ (isSetΠ (λ _ → isSetAlgebra N))
+isSetAlgebraHom _ N = isSetΣ (isSetΠ (λ _ → is-set))
                         λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)
+  where
+  open AlgebraStr (str N)
 
 
 isSetAlgebraEquiv : (M : Algebra R ℓ') (N : Algebra R ℓ'')
                   → isSet (AlgebraEquiv M N)
-isSetAlgebraEquiv M N = isSetΣ (isOfHLevel≃ 2 (isSetAlgebra M) (isSetAlgebra N))
+isSetAlgebraEquiv M N = isSetΣ (isOfHLevel≃ 2 M.is-set N.is-set)
                           λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)
+  where
+  module M = AlgebraStr (str M)
+  module N = AlgebraStr (str N)
 
 AlgebraHom≡ : {φ ψ : AlgebraHom A B} → fst φ ≡ fst ψ → φ ≡ ψ
 AlgebraHom≡ = Σ≡Prop λ f → isPropIsAlgebraHom _ _ f _
diff --git a/Cubical/Algebra/Algebra/Subalgebra.agda b/Cubical/Algebra/Algebra/Subalgebra.agda
index c2d56d04d6..ac30b99fa0 100644
--- a/Cubical/Algebra/Algebra/Subalgebra.agda
+++ b/Cubical/Algebra/Algebra/Subalgebra.agda
@@ -68,7 +68,7 @@ module _ ((S , isSubalgebra) : Subalgebra) where
   Subalgebra→Algebra .snd .algStr._⋆_ r (a , a∈) = r ⋆ a , ⋆-closed r a∈
   Subalgebra→Algebra .snd .algStr.isAlgebra =
     let
-      isSet-A' = isSetΣSndProp (isSetAlgebra A) (∈-isProp S)
+      isSet-A' = isSetΣSndProp is-set (∈-isProp S)
       +Assoc' = λ x y z → Subalgebra→Algebra≡ (+Assoc (fst x) (fst y) (fst z))
       +IdR' = λ x → Subalgebra→Algebra≡ (+IdR (fst x))
       +InvR' = λ x → Subalgebra→Algebra≡ (+InvR (fst x))
diff --git a/Cubical/Algebra/CommAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/Base.agda
index a0fff564c8..4022db273f 100644
--- a/Cubical/Algebra/CommAlgebra/Base.agda
+++ b/Cubical/Algebra/CommAlgebra/Base.agda
@@ -77,11 +77,6 @@ module _ {R : CommRing ℓ} where
   CommAlgebra→CommRing (_ , commalgebrastr  _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
     _ , commringstr _ _ _ _ _ (iscommring (IsAlgebra.isRing isAlgebra) ·-comm)
 
-  isSetCommAlgebra : (A : CommAlgebra R ℓ') → isSet ⟨ A ⟩
-  isSetCommAlgebra A = is-set
-    where
-    open CommAlgebraStr (str A)
-
   module _
       {A : Type ℓ'} {0a 1a : A}
       {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}
diff --git a/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda
index 2fa2e33ba3..229c8cb20a 100644
--- a/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda
+++ b/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda
@@ -169,8 +169,10 @@ module _ {R : CommRing ℓ} where
         universal =
           (inducedHom , inducedHomOnGenerators)
           , λ {(f , mapsValues)
-              → Σ≡Prop (λ _ → isPropΠ (λ _ → isSetCommAlgebra A _ _))
+              → Σ≡Prop (λ _ → isPropΠ (λ _ → is-set _ _))
                        (unique f mapsValues)}
+          where
+          open CommAlgebraStr (str A)
 
       {- ∀ A : Comm-R-Algebra,
          ∀ J : Finitely-generated-Ideal,
@@ -215,10 +217,12 @@ module _ {R : CommRing ℓ} where
       Iso.rightInv (FPHomIso {A}) =
         λ b → Σ≡Prop
                 (λ x → isPropΠ
-                  (λ i → isSetCommAlgebra A
+                  (λ i → is-set
                           (evPoly A (relation i) x)
                           (0a (snd A))))
                 (funExt (inducedHomOnGenerators A (fst b) (snd b)))
+        where
+        open CommAlgebraStr (str A)
       Iso.leftInv (FPHomIso {A}) =
         λ a → Σ≡Prop (λ f → isPropIsCommAlgebraHom {ℓ} {R} {ℓ} {ℓ} {FPAlgebra} {A} f)
                  λ i → fst (unique A
diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
index 40b434650d..a7dea81c7c 100644
--- a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
+++ b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
@@ -200,7 +200,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
                (s ⋆ 1a) · (t ⋆ 1a) ∎
       in eq i
     inducedMap (C.0-trunc P Q p q i j) =
-      isSetAlgebra (CommAlgebra→Algebra A) (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j
+      is-set (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j
 
     module _ where
       open IsAlgebraHom
diff --git a/Cubical/Algebra/CommAlgebra/Instances/Initial.agda b/Cubical/Algebra/CommAlgebra/Instances/Initial.agda
index 40e91e1c41..26c8b6bdd6 100644
--- a/Cubical/Algebra/CommAlgebra/Instances/Initial.agda
+++ b/Cubical/Algebra/CommAlgebra/Instances/Initial.agda
@@ -35,7 +35,7 @@ module _ (R : CommRing ℓ) where
     initialCAlg .snd .CommAlgebraStr.-_ = _
     initialCAlg .snd .CommAlgebraStr._⋆_ r x = r · x
     initialCAlg .snd .CommAlgebraStr.isCommAlgebra =
-      makeIsCommAlgebra (isSetRing (CommRing→Ring R))
+      makeIsCommAlgebra is-set
                          +Assoc +IdR +InvR +Comm
                          ·Assoc ·IdL
                          ·DistL+ ·Comm
diff --git a/Cubical/Algebra/CommAlgebra/Instances/Pointwise.agda b/Cubical/Algebra/CommAlgebra/Instances/Pointwise.agda
index 408cba54e8..9ce845e935 100644
--- a/Cubical/Algebra/CommAlgebra/Instances/Pointwise.agda
+++ b/Cubical/Algebra/CommAlgebra/Instances/Pointwise.agda
@@ -17,7 +17,7 @@ module _ {R : CommRing ℓ} (X : Type ℓ'') (A : CommAlgebra R ℓ') where
   pointwiseAlgebra : CommAlgebra R _
   pointwiseAlgebra =
     let open CommAlgebraStr (snd A)
-        isSetX→A = isOfHLevelΠ 2 (λ (x : X) → isSetCommRing (CommAlgebra→CommRing A))
+        isSetX→A = isOfHLevelΠ 2 (λ (x : X) → is-set)
     in commAlgebraFromCommRing
          (pointwiseRing X (CommAlgebra→CommRing A))
          (λ r f → (λ x → r ⋆ (f x)))
diff --git a/Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda b/Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda
index 9b62b35a94..1f488ddacf 100644
--- a/Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda
+++ b/Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda
@@ -223,7 +223,7 @@ module _
         -- The original function we get with the UP respects ⋆.
         original-pres⋆ : type-pres⋆ RLoc.S⁻¹RAsCommRing _⋆_ (original-univ .fst .fst)
         original-pres⋆ r = SQ.elimProp
-          (λ _ _ _ → isSetCommAlgebra B _ _ _ _)
+          (λ _ _ _ → is-set _ _ _ _)
           (λ (a , s , s∈S') → cong (_· _) (ψ .snd .IsAlgebraHom.pres⋆ r a)
                             ∙ ⋆AssocL _ _ _)
 
@@ -252,7 +252,7 @@ module _
                             (fst φ) ∘ RUniv._/1 ≡ (fst ψ))
                  → (χₐ , χₐcomm) ≡ el
         χₐunique (φ' , φ'comm) =
-          Σ≡Prop ((λ _ → isSetΠ (λ _ → isSetCommAlgebra B) _ _)) $ AlgebraHom≡ $
+          Σ≡Prop ((λ _ → isSetΠ (λ _ → is-set) _ _)) $ AlgebraHom≡ $
           cong (fst ∘ fst) -- Get underlying bare function.
                (univ .snd (CommAlgebraHom→RingHom {A = S⁻¹AAsCommAlgebra} {B = B}
                                                   φ' , φ'comm))
diff --git a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
index 51e8786e73..75bb4829e8 100644
--- a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
+++ b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
@@ -93,7 +93,9 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
   IsAlgebraHom.pres⋆ (snd quotientHom) _ _ = refl
 
 module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
-  open CommRingStr {{...}} hiding (_-_; -_; ·IdL; ·DistR+) renaming (_·_ to _·R_; _+_ to _+R_)
+  open CommRingStr {{...}}
+    hiding (_-_; -_; ·IdL; ·DistR+; is-set)
+    renaming (_·_ to _·R_; _+_ to _+R_)
   open CommAlgebraStr ⦃...⦄
 
   instance
@@ -102,39 +104,35 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
     _ : CommAlgebraStr R ⟨ A ⟩
     _ = snd A
 
-  private
-    LRing : Ring ℓ
-    LRing = CommAlgebra→Ring (A / I)
-    RRing : Ring ℓ
-    RRing = (CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I)
-
   -- sanity check / maybe a helper function some day
+  -- (These two rings are not definitionally equal, but only because of proofs, not data.)
   CommForget/ : RingEquiv (CommAlgebra→Ring (A / I)) ((CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I))
-  fst CommForget/ =
-    isoToEquiv
-      (iso
-        (rec (isSetRing LRing) (λ a → [ a ]) λ a b a-b∈I → eq/ a b a-b∈I)
-        (rec (isSetRing RRing) (λ a → [ a ]) (λ a b a-b∈I → eq/ a b a-b∈I))
-        (elimProp (λ _ → isSetRing LRing _ _) λ _ → refl)
-        (elimProp (λ _ → isSetRing RRing _ _) (λ _ → refl)))
+  fst CommForget/ = idEquiv _
   IsRingHom.pres0 (snd CommForget/) = refl
   IsRingHom.pres1 (snd CommForget/) = refl
-  IsRingHom.pres+ (snd CommForget/) = elimProp2 (λ _ _ → isSetRing RRing _ _) (λ _ _ → refl)
-  IsRingHom.pres· (snd CommForget/) = elimProp2 (λ _ _ → isSetRing RRing _ _) (λ _ _ → refl)
-  IsRingHom.pres- (snd CommForget/) = elimProp (λ _ → isSetRing RRing _ _) (λ _ → refl)
-
-  open IsAlgebraHom
-  inducedHom : (B : CommAlgebra R ℓ) (ϕ : CommAlgebraHom A B)
-               → (fst I) ⊆ (fst (kernel A B ϕ))
-               → CommAlgebraHom (A / I) B
-  fst (inducedHom B ϕ I⊆kernel) =
-    let open RingTheory (CommRing→Ring (CommAlgebra→CommRing B))
-        instance
-          _ : CommAlgebraStr R _
-          _ = snd B
-          _ : CommRingStr _
-          _ = snd (CommAlgebra→CommRing B)
-    in rec (isSetCommAlgebra B) (λ x → fst ϕ x)
+  IsRingHom.pres+ (snd CommForget/) = λ _ _ → refl
+  IsRingHom.pres· (snd CommForget/) = λ _ _ → refl
+  IsRingHom.pres- (snd CommForget/) = λ _ → refl
+
+  module _
+    (B : CommAlgebra R ℓ)
+    (ϕ : CommAlgebraHom A B)
+    (I⊆kernel : (fst I) ⊆ (fst (kernel A B ϕ)))
+    where abstract
+
+    open IsAlgebraHom
+    open RingTheory (CommRing→Ring (CommAlgebra→CommRing B))
+
+    private
+      instance
+        _ : CommAlgebraStr R ⟨ B ⟩
+        _ = snd B
+        _ : CommRingStr ⟨ B ⟩
+        _ = snd (CommAlgebra→CommRing B)
+
+    inducedHom : CommAlgebraHom (A / I) B
+    fst inducedHom =
+      rec is-set (λ x → fst ϕ x)
         λ a b a-b∈I →
           equalByDifference
             (fst ϕ a) (fst ϕ b)
@@ -142,26 +140,28 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
              (fst ϕ a) + (fst ϕ (- b)) ≡⟨ sym (IsAlgebraHom.pres+ (snd ϕ) _ _) ⟩
              fst ϕ (a - b)             ≡⟨ I⊆kernel (a - b) a-b∈I ⟩
              0r ∎)
-  pres0 (snd (inducedHom B ϕ kernel⊆I)) = pres0 (snd ϕ)
-  pres1 (snd (inducedHom B ϕ kernel⊆I)) = pres1 (snd ϕ)
-  pres+ (snd (inducedHom B ϕ kernel⊆I)) = elimProp2 (λ _ _ → isSetCommAlgebra B _ _) (pres+ (snd ϕ))
-  pres· (snd (inducedHom B ϕ kernel⊆I)) = elimProp2 (λ _ _ → isSetCommAlgebra B _ _) (pres· (snd ϕ))
-  pres- (snd (inducedHom B ϕ kernel⊆I)) = elimProp (λ _ → isSetCommAlgebra B _ _) (pres- (snd ϕ))
-  pres⋆ (snd (inducedHom B ϕ kernel⊆I)) = λ r → elimProp (λ _ → isSetCommAlgebra B _ _) (pres⋆ (snd ϕ) r)
-
-  inducedHom∘quotientHom : (B : CommAlgebra R ℓ) (ϕ : CommAlgebraHom A B)
-               → (I⊆kerϕ : fst I ⊆ fst (kernel A B ϕ))
-               → inducedHom B ϕ I⊆kerϕ ∘a quotientHom A I ≡ ϕ
-  inducedHom∘quotientHom B ϕ I⊆kerϕ = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = B}) (funExt (λ a → refl))
+    pres0 (snd inducedHom) = pres0 (snd ϕ)
+    pres1 (snd inducedHom) = pres1 (snd ϕ)
+    pres+ (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres+ (snd ϕ))
+    pres· (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres· (snd ϕ))
+    pres- (snd inducedHom) = elimProp (λ _ → is-set _ _) (pres- (snd ϕ))
+    pres⋆ (snd inducedHom) = λ r → elimProp (λ _ → is-set _ _) (pres⋆ (snd ϕ) r)
+
+    inducedHom∘quotientHom : inducedHom ∘a quotientHom A I ≡ ϕ
+    inducedHom∘quotientHom = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = B}) (funExt (λ a → refl))
 
   injectivePrecomp : (B : CommAlgebra R ℓ) (f g : CommAlgebraHom (A / I) B)
                      → f ∘a (quotientHom A I) ≡ g ∘a (quotientHom A I)
                      → f ≡ g
   injectivePrecomp B f g p =
     Σ≡Prop
-      (λ h → isPropIsAlgebraHom (CommRing→Ring R) (snd (CommAlgebra→Algebra (A / I))) h (snd (CommAlgebra→Algebra B)))
-      (descendMapPath (fst f) (fst g) (isSetCommAlgebra B)
+      (λ h → isPropIsCommAlgebraHom {M = A / I} {N = B} h)
+      (descendMapPath (fst f) (fst g) is-set
                       λ x → λ i → fst (p i) x)
+    where
+    instance
+      _ : CommAlgebraStr R ⟨ B ⟩
+      _ = str B
 
 
 {- trivial quotient -}
@@ -181,7 +181,7 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where abstract
   fst zeroIdealQuotient =
     let open RingTheory (CommRing→Ring (CommAlgebra→CommRing A))
     in isoToEquiv (iso (fst (quotientHom A (0Ideal A)))
-                    (rec (isSetCommAlgebra A) (λ x → x) λ x y x-y≡0 → equalByDifference x y x-y≡0)
+                    (rec is-set (λ x → x) λ x y x-y≡0 → equalByDifference x y x-y≡0)
                     (elimProp (λ _ → squash/ _ _) λ _ → refl)
                     λ _ → refl)
   snd zeroIdealQuotient = snd (quotientHom A (0Ideal A))
diff --git a/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda b/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda
index cc307b6397..7851f2fb4f 100644
--- a/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda
+++ b/Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda
@@ -226,7 +226,7 @@ module _ (R : CommRing ℓ) where
     fst (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedHom x
     snd (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedMapGenerator x
     snd (equiv-proof (snd indcuedHomEquivalence) x) (g , gX≡x) =
-      Σ≡Prop (λ _ → isSetAlgebra A _ _) (sym (inducedHomUnique x g gX≡x))
+      Σ≡Prop (λ _ → is-set _ _) (sym (inducedHomUnique x g gX≡x))
 
     equalByUMP : (f g : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A)
                  → fst f X ≡ fst g X
diff --git a/Cubical/Algebra/CommMonoid/Base.agda b/Cubical/Algebra/CommMonoid/Base.agda
index 9f643a768a..3c7439c2a3 100644
--- a/Cubical/Algebra/CommMonoid/Base.agda
+++ b/Cubical/Algebra/CommMonoid/Base.agda
@@ -81,11 +81,6 @@ CommMonoidStr→MonoidStr (commmonoidstr _ _ H) = monoidstr _ _ (IsCommMonoid.is
 CommMonoid→Monoid : CommMonoid ℓ → Monoid ℓ
 CommMonoid→Monoid (_ , commmonoidstr  _ _ M) = _ , monoidstr _ _ (IsCommMonoid.isMonoid M)
 
-isSetCommMonoid : (M : CommMonoid ℓ) → isSet ⟨ M ⟩
-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/GrothendieckGroup.agda b/Cubical/Algebra/CommMonoid/GrothendieckGroup.agda
index f1addba0e2..56976dfcac 100644
--- a/Cubical/Algebra/CommMonoid/GrothendieckGroup.agda
+++ b/Cubical/Algebra/CommMonoid/GrothendieckGroup.agda
@@ -155,7 +155,7 @@ The "groupification" of a monoid comes with a universal morphism and a universal
       f = fst φ
 
     inducedHom : AbGroupHom (Groupification M) A
-    fst inducedHom = elim (λ x → isSetAbGroup A) g proof
+    fst inducedHom = elim (λ x → is-set) g proof
         where
         g = λ (a , b) → f a - f b
         proof : (u v : ⟨ M² M ⟩) (r : R M u v) → g u ≡ g v
@@ -187,7 +187,7 @@ The "groupification" of a monoid comes with a universal morphism and a universal
               f c - f d
                 ∎
 
-    pres· (snd inducedHom) = elimProp2 (λ _ _ → isSetAbGroup A _ _) proof
+    pres· (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) proof
       where
         rExp : ∀ {x y z} → x ≡ y → x + z ≡ y + z
         rExp r = cong₂ _+_ r refl
@@ -205,7 +205,7 @@ The "groupification" of a monoid comes with a universal morphism and a universal
             lemma = rExp (sym (·Assoc _ _ _) ∙ lExp (·Comm _ _) ∙ ·Assoc _ _ _) ∙ sym (·Assoc _ _ _)
 
     pres1 (snd inducedHom)   = +InvR _
-    presinv (snd inducedHom) = elimProp (λ _ → isSetAbGroup A _ _)
+    presinv (snd inducedHom) = elimProp (λ _ → is-set _ _)
                                         (λ _ → sym (invDistr _ _ ∙ cong₂ _-_ (invInv _) refl))
 
     solution : (m : ⟨ M ⟩) → (fst inducedHom) (i m) ≡ f m
diff --git a/Cubical/Algebra/CommRing/Base.agda b/Cubical/Algebra/CommRing/Base.agda
index 6a481ca443..36f44a8001 100644
--- a/Cubical/Algebra/CommRing/Base.agda
+++ b/Cubical/Algebra/CommRing/Base.agda
@@ -155,11 +155,6 @@ CommRingPath = ∫ 𝒮ᴰ-CommRing .UARel.ua
 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 = is-set
-  where
-  open CommRingStr (str R)
-
 CommRingIso : (R : CommRing ℓ) (S : CommRing ℓ') → Type (ℓ-max ℓ ℓ')
 CommRingIso R S = Σ[ e ∈ Iso (R .fst) (S .fst) ]
                      IsRingHom (CommRingStr→RingStr (R .snd)) (e .fun) (CommRingStr→RingStr (S .snd))
diff --git a/Cubical/Algebra/CommRing/Instances/Pointwise.agda b/Cubical/Algebra/CommRing/Instances/Pointwise.agda
index e2e0d237e1..47ee23a8e9 100644
--- a/Cubical/Algebra/CommRing/Instances/Pointwise.agda
+++ b/Cubical/Algebra/CommRing/Instances/Pointwise.agda
@@ -15,7 +15,7 @@ pointwiseRing X R = (X → fst R) , str
     where
       open CommRingStr (snd R)
 
-      isSetX→R = isOfHLevelΠ 2 (λ _ → isSetCommRing R)
+      isSetX→R = isOfHLevelΠ 2 (λ _ → is-set)
 
       str : CommRingStr (X → fst R)
       CommRingStr.0r str = λ _ → 0r
diff --git a/Cubical/Algebra/CommRing/Quotient/Base.agda b/Cubical/Algebra/CommRing/Quotient/Base.agda
index 9a37f2ab66..960717c018 100644
--- a/Cubical/Algebra/CommRing/Quotient/Base.agda
+++ b/Cubical/Algebra/CommRing/Quotient/Base.agda
@@ -50,12 +50,12 @@ module Quotient-FGideal-CommRing-Ring
   (gnull : (k : Fin n) → g $r v k ≡ RingStr.0r (snd B))
   where
 
-  open RingStr (snd B) using (0r)
+  open RingStr (snd B) using (0r; is-set)
 
   zeroOnGeneratedIdeal : (x : ⟨ A ⟩) → x ∈ fst (generatedIdeal A v) → g $r x ≡ 0r
   zeroOnGeneratedIdeal x x∈FGIdeal =
     PT.elim
-      (λ _ → isSetRing B (g $r x) 0r)
+      (λ _ → is-set (g $r x) 0r)
       (λ {(α , isLC) → subst _ (sym isLC) (cancelLinearCombination A B g _ α v gnull)})
       x∈FGIdeal
 
diff --git a/Cubical/Algebra/CommRing/Quotient/IdealSum.agda b/Cubical/Algebra/CommRing/Quotient/IdealSum.agda
index 7948ff96b1..6906c1167e 100644
--- a/Cubical/Algebra/CommRing/Quotient/IdealSum.agda
+++ b/Cubical/Algebra/CommRing/Quotient/IdealSum.agda
@@ -105,7 +105,7 @@ module Construction {R : CommRing ℓ} (I J : IdealsIn R) where
 
   kernel-0 : (x : ⟨ R / (I +i J) ⟩) → fst ψ x ≡ 0r → x ≡ 0r
   kernel-0 x ψx≡0 =
-    PT.rec (isSetCommRing (R / (I +i J)) x 0r)
+    PT.rec (is-set x 0r)
            (λ (x' , π+x'≡x) →
              let πx'≡0 : fst π x' ≡ 0r
                  πx'≡0 = fst π x'          ≡⟨⟩
@@ -142,7 +142,7 @@ module Construction {R : CommRing ℓ} (I J : IdealsIn R) where
   embedding : isEmbedding {A = ⟨ R / (I +i J) ⟩} {B = ⟨ (R / I) / π₁J ⟩} (fst ϕ)
   embedding =
     injEmbedding
-          (isSetCommRing ((R / I) / π₁J))
+          is-set
           ϕ-injective
 
 
diff --git a/Cubical/Algebra/DistLattice/Base.agda b/Cubical/Algebra/DistLattice/Base.agda
index 37c1b5a5f7..cadd500bb6 100644
--- a/Cubical/Algebra/DistLattice/Base.agda
+++ b/Cubical/Algebra/DistLattice/Base.agda
@@ -74,11 +74,6 @@ record DistLatticeStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
 DistLattice : ∀ ℓ → Type (ℓ-suc ℓ)
 DistLattice ℓ = TypeWithStr ℓ DistLatticeStr
 
-isSetDistLattice : (L : DistLattice ℓ) → isSet ⟨ L ⟩
-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
 -- of ∧l over ∨l we can derive distributivity and absorption
@@ -245,17 +240,15 @@ isPropIsDistLattice 0l 1l _∨l_ _∧l_ (isdistlattice LL LD1 LD2) (isdistlattic
   λ i → isdistlattice (isPropIsLattice _ _ _ _ LL ML i) (isPropDist1 LD1 MD1 i)
                                                         (isPropDist2 LD2 MD2 i)
   where
-  isSetL : isSet _
-  isSetL = LL .IsLattice.joinSemilattice .IsSemilattice.isCommMonoid .IsCommMonoid.isMonoid
-              .IsMonoid.isSemigroup .IsSemigroup.is-set
+  open IsLattice LL using (is-set)
 
   isPropDist1 : isProp ((x y z : _) → (x ∨l (y ∧l z) ≡ (x ∨l y) ∧l (x ∨l z))
                                     × ((y ∧l z) ∨l x ≡ (y ∨l x) ∧l (z ∨l x)))
-  isPropDist1 = isPropΠ3 (λ _ _ _ → isProp× (isSetL _ _) (isSetL _ _))
+  isPropDist1 = isPropΠ3 (λ _ _ _ → isProp× (is-set _ _) (is-set _ _))
 
   isPropDist2 : isProp ((x y z : _) → (x ∧l (y ∨l z) ≡ (x ∧l y) ∨l (x ∧l z))
                                     × ((y ∨l z) ∧l x ≡ (y ∧l x) ∨l (z ∧l x)))
-  isPropDist2 = isPropΠ3 (λ _ _ _ → isProp× (isSetL _ _) (isSetL _ _))
+  isPropDist2 = isPropΠ3 (λ _ _ _ → isProp× (is-set _ _) (is-set _ _))
 
 𝒮ᴰ-DistLattice : DUARel (𝒮-Univ ℓ) DistLatticeStr ℓ
 𝒮ᴰ-DistLattice =
diff --git a/Cubical/Algebra/DistLattice/Basis.agda b/Cubical/Algebra/DistLattice/Basis.agda
index d150d23458..383e7e251c 100644
--- a/Cubical/Algebra/DistLattice/Basis.agda
+++ b/Cubical/Algebra/DistLattice/Basis.agda
@@ -64,14 +64,14 @@ module _ (L' : DistLattice ℓ) where
    ⋁Basis : ∀ (x : L) → ∃[ n ∈ ℕ ] Σ[ α ∈ FinVec L n ] (∀ i → α i ∈ S) × (⋁ α ≡ x)
 
  open IsBasis
- open SemilatticeStr
+ open SemilatticeStr hiding (is-set)
  Basis→MeetSemilattice : (S : ℙ L) → IsBasis S → Semilattice ℓ
  fst (Basis→MeetSemilattice S isBasisS) = Σ[ l ∈ L ] (l ∈ S)
  ε (snd (Basis→MeetSemilattice S isBasisS)) = 1l , isBasisS .contains1
  _·_ (snd (Basis→MeetSemilattice S isBasisS)) x y = fst x ∧l fst y
                                                   , isBasisS .∧lClosed _ _ (snd x) (snd y)
  isSemilattice (snd (Basis→MeetSemilattice S isBasisS)) = makeIsSemilattice
-   (isSetΣ (isSetDistLattice L') λ _ → isProp→isSet (S _ .snd))
+   (isSetΣ is-set λ _ → isProp→isSet (S _ .snd))
      (λ _ _ _ → Σ≡Prop (λ _ → S _ .snd) (∧lAssoc _ _ _))
        (λ _ → Σ≡Prop (λ _ → S _ .snd) (∧lRid _))
            (λ _ _ → Σ≡Prop (λ _ → S _ .snd) (∧lComm _ _))
diff --git a/Cubical/Algebra/Field/Base.agda b/Cubical/Algebra/Field/Base.agda
index c2406af2f3..445238dd6b 100644
--- a/Cubical/Algebra/Field/Base.agda
+++ b/Cubical/Algebra/Field/Base.agda
@@ -74,11 +74,6 @@ record FieldStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
 Field : ∀ ℓ → Type (ℓ-suc ℓ)
 Field ℓ = TypeWithStr ℓ FieldStr
 
-isSetField : (R : Field ℓ) → isSet ⟨ R ⟩
-isSetField R = is-set
-  where
-  open FieldStr (str R)
-
 
 makeIsField : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
                  {_[_]⁻¹ : (x : R) → ¬ (x ≡ 0r) → R}
@@ -181,9 +176,6 @@ isPropIsField {R = R} 0r 1r _+_ _·_ -_ H@(isfield RR RC RD) (isfield SR SC SD)
   λ i → isfield (isPropIsCommRing _ _ _ _ _ RR SR i)
                    (isPropInv RC SC i) (isProp¬ _ RD SD i)
   where
-  isSetR : isSet _
-  isSetR =  RR .IsCommRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set
-
   isPropInv : isProp ((x : _) → ¬ x ≡ 0r → Σ[ y ∈ R ] x · y ≡ 1r)
   isPropInv = isPropΠ2 (λ x _ → Units.inverseUniqueness (Field→CommRing (_ , fieldstr _ _ _ _ _ H)) x)
 
diff --git a/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda b/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda
index 8c56c34edf..80a760f241 100644
--- a/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda
+++ b/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda
@@ -14,6 +14,7 @@ module Cubical.Algebra.Group.Abelianization.AbelianizationAsCoeq where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
 
 open import Cubical.Data.Sigma
 
@@ -213,7 +214,7 @@ module UniversalPropertyCoeq (G : Group ℓ) where
             f' = fst f
             g : Abelianization → fst H
             g = rec
-                  (isSetAbGroup H)
+                  is-set
                   (λ x → (f') x)
                   (λ (a , b , c) →
                     f' (a · b · c)           ≡⟨ (snd f).pres· a (b · c) ⟩
@@ -227,12 +228,12 @@ module UniversalPropertyCoeq (G : Group ℓ) where
             gIsHom : IsGroupHom (snd (AbGroup→Group asAbelianGroup)) g (snd (AbGroup→Group H))
             pres· gIsHom =
               elimProp2
-                (λ x y → isSetAbGroup H _ _)
+                (λ x y → is-set _ _)
                 ((snd f).pres·)
             pres1 gIsHom = (snd f).pres1
             presinv gIsHom =
               elimProp
-                (λ x → isSetAbGroup H _ _)
+                (λ x → is-set _ _)
                 ((snd f).presinv)
 
     commutativity : (H : AbGroup ℓ)
@@ -255,13 +256,14 @@ module UniversalPropertyCoeq (G : Group ℓ) where
         Σ≡Prop
           (λ _ → isPropIsGroupHom _ _)
           (λ i x →  q x i)
-      where q : (x : Abelianization)
-                →  fst g x ≡ fst (inducedHom H f) x
-            q = elimProp
-                  (λ _ → isSetAbGroup H _ _)
-                  (λ x → fst g (incAb x) ≡⟨ cong (λ f → f x) (cong fst p) ⟩
-                        (fst f) x       ≡⟨ refl ⟩
-                        fst (inducedHom H f) (incAb x)∎)
+      where
+      module H = AbGroupStr (str H)
+      q : (x : Abelianization) →  fst g x ≡ fst (inducedHom H f) x
+      q = elimProp
+            (λ _ → H.is-set _ _)
+            (λ x → fst g (incAb x) ≡⟨ cong (λ f → f x) (cong fst p) ⟩
+                  (fst f) x       ≡⟨ refl ⟩
+                  fst (inducedHom H f) (incAb x)∎)
 
 module IsoCoeqHIT (G : Group ℓ) where
   open GroupStr {{...}}
@@ -415,8 +417,8 @@ module IsoCoeqHIT (G : Group ℓ) where
       p : h .fst ≡ isomorphism .fst
       p =
         Iso≡Set
-          (isSetAbGroup asAbelianGroup)
-          (isSetAbGroup (HITasAbelianGroup G))
+          (AbGroupStr.is-set (str asAbelianGroup))
+          (AbGroupStr.is-set (str (HITasAbelianGroup G)))
           (h .fst)
           (isomorphism .fst)
           (λ x → cong
diff --git a/Cubical/Algebra/Group/Abelianization/Properties.agda b/Cubical/Algebra/Group/Abelianization/Properties.agda
index 45ff502d27..75f17b5e50 100644
--- a/Cubical/Algebra/Group/Abelianization/Properties.agda
+++ b/Cubical/Algebra/Group/Abelianization/Properties.agda
@@ -12,6 +12,7 @@ module Cubical.Algebra.Group.Abelianization.Properties where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
 
 open import Cubical.Data.Sigma
 
@@ -245,7 +246,7 @@ module UniversalProperty (G : Group ℓ) where
             f' = fst f
             g : Abelianization G → fst H
             g = (rec G)
-                  (isSetAbGroup H)
+                  is-set
                   (λ x → (f') x)
                   (λ a b c → f' (a · b · c)           ≡⟨ (snd f).pres· a (b · c) ⟩
                              (f' a) · (f' (b · c))    ≡⟨ cong
@@ -262,12 +263,12 @@ module UniversalProperty (G : Group ℓ) where
             gIsHom : IsGroupHom (snd (AbGroup→Group asAbelianGroup)) g (snd (AbGroup→Group H))
             pres· gIsHom =
               (elimProp2 G)
-                (λ x y → isSetAbGroup H _ _)
+                (λ x y → is-set _ _)
                 ((snd f).pres·)
             pres1 gIsHom = (snd f).pres1
             presinv gIsHom =
               (elimProp G)
-                (λ x → isSetAbGroup H _ _)
+                (λ x → is-set _ _)
                 ((snd f).presinv)
 
     commutativity : (H : AbGroup ℓ)
@@ -290,10 +291,11 @@ module UniversalProperty (G : Group ℓ) where
         Σ≡Prop
           (λ _ → isPropIsGroupHom _ _)
           (λ i x →  q x i)
-      where q : (x : Abelianization G)
-                →  fst g x ≡ fst (inducedHom H f) x
-            q = (elimProp G)
-                  (λ _ → isSetAbGroup H _ _)
-                  (λ x → fst g (η x) ≡⟨ cong (λ f → f x) (cong fst p) ⟩
-                         (fst f) x   ≡⟨ refl ⟩
-                         fst (inducedHom H f) (η x)∎)
+      where
+      module H = AbGroupStr (str H)
+      q : (x : Abelianization G) → fst g x ≡ fst (inducedHom H f) x
+      q = (elimProp G)
+            (λ _ → H.is-set _ _)
+            (λ x → fst g (η x) ≡⟨ cong (λ f → f x) (cong fst p) ⟩
+                   (fst f) x   ≡⟨ refl ⟩
+                   fst (inducedHom H f) (η x)∎)
diff --git a/Cubical/Algebra/Group/Base.agda b/Cubical/Algebra/Group/Base.agda
index 1b2a6cac5f..2bde95181d 100644
--- a/Cubical/Algebra/Group/Base.agda
+++ b/Cubical/Algebra/Group/Base.agda
@@ -55,11 +55,6 @@ Group₀ = Group ℓ-zero
 group : (G : Type ℓ) (1g : G) (_·_ : G → G → G) (inv : G → G) (h : IsGroup 1g _·_ inv) → Group ℓ
 group G 1g _·_ inv h = G , groupstr 1g _·_ inv h
 
-isSetGroup : (G : Group ℓ) → isSet ⟨ G ⟩
-isSetGroup G = is-set
-  where
-  open GroupStr (str G)
-
 makeIsGroup : {G : Type ℓ} {e : G} {_·_ : G → G → G} { inv : G → G}
               (is-setG : isSet G)
               (·Assoc : (x y z : G) → x · (y · z) ≡ (x · y) · z)
diff --git a/Cubical/Algebra/Lattice/Base.agda b/Cubical/Algebra/Lattice/Base.agda
index 7782c8b5df..55889dfa6e 100644
--- a/Cubical/Algebra/Lattice/Base.agda
+++ b/Cubical/Algebra/Lattice/Base.agda
@@ -93,11 +93,6 @@ record LatticeStr (A : Type ℓ)  : Type (ℓ-suc ℓ) where
 Lattice : ∀ ℓ → Type (ℓ-suc ℓ)
 Lattice ℓ = TypeWithStr ℓ LatticeStr
 
-isSetLattice : (L : Lattice ℓ) → isSet ⟨ L ⟩
-isSetLattice L = is-set
-  where
-  open LatticeStr (str L)
-
 makeIsLattice : {L : Type ℓ} {0l 1l : L} {_∨l_ _∧l_ : L → L → L}
              (is-setL : isSet L)
              (∨l-assoc : (x y z : L) → x ∨l (y ∨l z) ≡ (x ∨l y) ∨l z)
@@ -183,20 +178,20 @@ isPropIsLattice 0l 1l _∨l_ _∧l_ (islattice LJ LM LA) (islattice MJ MM MA) =
                   (isPropIsSemilattice _ _ LM MM i)
                   (isPropAbsorb LA MA i)
   where
-  isSetL : isSet _
-  isSetL = LJ .IsSemilattice.isCommMonoid .IsCommMonoid.isMonoid
-              .IsMonoid.isSemigroup .IsSemigroup.is-set
+  open IsSemilattice LJ using (is-set)
 
   isPropAbsorb : isProp ((x y : _) → (x ∨l (x ∧l y) ≡ x) × (x ∧l (x ∨l y) ≡ x))
-  isPropAbsorb = isPropΠ2 λ _ _ → isProp× (isSetL _ _) (isSetL _ _)
+  isPropAbsorb = isPropΠ2 λ _ _ → isProp× (is-set _ _) (is-set _ _)
 
 isPropIsLatticeHom : {A : Type ℓ} {B : Type ℓ'} (R : LatticeStr A) (f : A → B) (S : LatticeStr B)
                    → isProp (IsLatticeHom R f S)
 isPropIsLatticeHom R f S = isOfHLevelRetractFromIso 1 IsLatticeHomIsoΣ
-                           (isProp×3 (isSetLattice (_ , S) _ _)
-                                     (isSetLattice (_ , S) _ _)
-                                     (isPropΠ2 λ _ _ → isSetLattice (_ , S) _ _)
-                                     (isPropΠ2 λ _ _ → isSetLattice (_ , S) _ _))
+                           (isProp×3 (is-set _ _)
+                                     (is-set _ _)
+                                     (isPropΠ2 λ _ _ → is-set _ _)
+                                     (isPropΠ2 λ _ _ → is-set _ _))
+  where
+  open LatticeStr S
 
 
 𝒮ᴰ-Lattice : DUARel (𝒮-Univ ℓ) LatticeStr ℓ
diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda
index 35c3e04559..3bc28d5fae 100644
--- a/Cubical/Algebra/Lattice/Properties.agda
+++ b/Cubical/Algebra/Lattice/Properties.agda
@@ -68,7 +68,7 @@ module Order (L' : Lattice ℓ) where
                     y ∎
 
  ≤Equiv : ∀ (x y : L) → (x ≤j y) ≃ (x ≤m y)
- ≤Equiv x y = propBiimpl→Equiv (isSetLattice L' _ _) (isSetLattice L' _ _) (≤j→≤m x y) (≤m→≤j x y)
+ ≤Equiv x y = propBiimpl→Equiv (is-set _ _) (is-set _ _) (≤j→≤m x y) (≤m→≤j x y)
 
  IndPosetPath : JoinPoset ≡ MeetPoset
  IndPosetPath = PosetPath _ _ .fst ((idEquiv _) , isposetequiv ≤Equiv )
diff --git a/Cubical/Algebra/Module/Base.agda b/Cubical/Algebra/Module/Base.agda
index 46a0c27e70..f88a0e5840 100644
--- a/Cubical/Algebra/Module/Base.agda
+++ b/Cubical/Algebra/Module/Base.agda
@@ -83,11 +83,6 @@ module _ {R : Ring ℓ} where
     LeftModule→Group : Group ℓ'
     LeftModule→Group = AbGroup→Group LeftModule→AbGroup
 
-  isSetLeftModule : (M : LeftModule R ℓ') → isSet ⟨ M ⟩
-  isSetLeftModule M = is-set
-    where
-    open LeftModuleStr (str M)
-
   open RingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_)
 
   module _  {M : Type ℓ'} {0m : M}
diff --git a/Cubical/Algebra/Module/Submodule.agda b/Cubical/Algebra/Module/Submodule.agda
index 1389f1f0ce..90f301e21c 100644
--- a/Cubical/Algebra/Module/Submodule.agda
+++ b/Cubical/Algebra/Module/Submodule.agda
@@ -40,7 +40,7 @@ module _ (R : Ring ℓ) (M : LeftModule R ℓ') where
   open isSubmodule
 
   zeroSubmodule : Submodule
-  fst zeroSubmodule x = (x ≡ 0m) , isSetLeftModule M x 0m
+  fst zeroSubmodule x = (x ≡ 0m) , is-set x 0m
   +-closed  (snd zeroSubmodule) x≡0 y≡0 = (λ i → x≡0 i + y≡0 i) ∙ +IdL 0m
   0r-closed (snd zeroSubmodule)         = refl
   ⋆-closed  (snd zeroSubmodule) r x≡0   = (λ i → r ⋆ x≡0 i) ∙ ⋆AnnihilR r
diff --git a/Cubical/Algebra/OrderedCommMonoid/Base.agda b/Cubical/Algebra/OrderedCommMonoid/Base.agda
index 39856573d7..22aaf7cc15 100644
--- a/Cubical/Algebra/OrderedCommMonoid/Base.agda
+++ b/Cubical/Algebra/OrderedCommMonoid/Base.agda
@@ -90,8 +90,3 @@ OrderedCommMonoid→CommMonoid M .fst = M .fst
 OrderedCommMonoid→CommMonoid M .snd =
   let open OrderedCommMonoidStr (M .snd)
   in commmonoidstr _ _ isCommMonoid
-
-isSetOrderedCommMonoid : (M : OrderedCommMonoid ℓ ℓ') → isSet ⟨ M ⟩
-isSetOrderedCommMonoid M = is-set
-  where
-  open OrderedCommMonoidStr (str M)
diff --git a/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda b/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda
index f270ed0785..df93645aca 100644
--- a/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda
+++ b/Cubical/Algebra/OrderedCommMonoid/PropCompletion.agda
@@ -261,5 +261,7 @@ isSetBoundedPropCompletion :
      (M : OrderedCommMonoid ℓ ℓ)
    → isSet (⟨ BoundedPropCompletion M ⟩)
 isSetBoundedPropCompletion M =
-  isSetΣSndProp (isSetOrderedCommMonoid (PropCompletion M))
+  isSetΣSndProp is-set
                 λ x → PropCompletion.isPropIsBounded _ M x
+  where
+  open OrderedCommMonoidStr (str (PropCompletion M))
diff --git a/Cubical/Algebra/Polynomials/UnivariateList/Base.agda b/Cubical/Algebra/Polynomials/UnivariateList/Base.agda
index 62f93719a4..3a088302d8 100644
--- a/Cubical/Algebra/Polynomials/UnivariateList/Base.agda
+++ b/Cubical/Algebra/Polynomials/UnivariateList/Base.agda
@@ -118,7 +118,7 @@ module PolyMod (R' : CommRing ℓ) where
 
 
   isSetPolyFun : isSet PolyFun
-  isSetPolyFun = isSetΣSndProp (isSetΠ (λ x → isSetCommRing R')) λ f x y → squash₁ x y
+  isSetPolyFun = isSetΣSndProp (isSetΠ (λ x → is-set)) λ f x y → squash₁ x y
 
 
   --construction of the function that represents the polynomial
diff --git a/Cubical/Algebra/Ring/Base.agda b/Cubical/Algebra/Ring/Base.agda
index d3db28be08..91ce9d7099 100644
--- a/Cubical/Algebra/Ring/Base.agda
+++ b/Cubical/Algebra/Ring/Base.agda
@@ -81,11 +81,6 @@ record RingStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
 Ring : ∀ ℓ → Type (ℓ-suc ℓ)
 Ring ℓ = TypeWithStr ℓ RingStr
 
-isSetRing : (R : Ring ℓ) → isSet ⟨ R ⟩
-isSetRing R = is-set
-  where
-  open RingStr (str R)
-
 module _ {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
                (is-setR : isSet R)
                (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
@@ -183,18 +178,25 @@ isPropIsRing 0r 1r _+_ _·_ -_ =
 isPropIsRingHom : {A : Type ℓ} {B : Type ℓ'} (R : RingStr A) (f : A → B) (S : RingStr B)
   → isProp (IsRingHom R f S)
 isPropIsRingHom R f S = isOfHLevelRetractFromIso 1 IsRingHomIsoΣ
-                        (isProp×4 (isSetRing (_ , S) _ _)
-                                  (isSetRing (_ , S) _ _)
-                                  (isPropΠ2 λ _ _ → isSetRing (_ , S) _ _)
-                                  (isPropΠ2 λ _ _ → isSetRing (_ , S) _ _)
-                                  (isPropΠ λ _ → isSetRing (_ , S) _ _))
+                        (isProp×4 (is-set _ _)
+                                  (is-set _ _)
+                                  (isPropΠ2 λ _ _ → is-set _ _)
+                                  (isPropΠ2 λ _ _ → is-set _ _)
+                                  (isPropΠ λ _ → is-set _ _))
+  where
+  open RingStr S using (is-set)
 
 isSetRingHom : (R : Ring ℓ) (S : Ring ℓ') → isSet (RingHom R S)
-isSetRingHom R S = isSetΣSndProp (isSetΠ (λ _ → isSetRing S)) (λ f → isPropIsRingHom (snd R) f (snd S))
+isSetRingHom R S = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f → isPropIsRingHom (snd R) f (snd S))
+  where
+  open RingStr (str S) using (is-set)
 
 isSetRingEquiv : (A : Ring ℓ) (B : Ring ℓ') → isSet (RingEquiv A B)
-isSetRingEquiv A B = isSetΣSndProp (isOfHLevel≃ 2 (isSetRing A) (isSetRing B))
+isSetRingEquiv A B = isSetΣSndProp (isOfHLevel≃ 2 A.is-set B.is-set)
                                    (λ e → isPropIsRingHom (snd A) (fst e) (snd B))
+  where
+  module A = RingStr (str A)
+  module B = RingStr (str B)
 
 RingHomPathP : (R : Ring ℓ) (S T : Ring ℓ') (p : S ≡ T) (φ : RingHom R S) (ψ : RingHom R T)
              → PathP (λ i → R .fst → p i .fst) (φ .fst) (ψ .fst)
diff --git a/Cubical/Algebra/Ring/Ideal/Base.agda b/Cubical/Algebra/Ring/Ideal/Base.agda
index ccf6a63832..0bf8f0a6f8 100644
--- a/Cubical/Algebra/Ring/Ideal/Base.agda
+++ b/Cubical/Algebra/Ring/Ideal/Base.agda
@@ -63,7 +63,7 @@ module _ (R' : Ring ℓ) where
 
   {- Examples of ideals -}
   zeroSubset : ℙ R
-  zeroSubset x = (x ≡ 0r) , isSetRing R' _ _
+  zeroSubset x = (x ≡ 0r) , is-set _ _
 
   open RingTheory R'
   open isIdeal
diff --git a/Cubical/Algebra/Ring/Kernel.agda b/Cubical/Algebra/Ring/Kernel.agda
index e82a4bd54f..eee454ac8f 100644
--- a/Cubical/Algebra/Ring/Kernel.agda
+++ b/Cubical/Algebra/Ring/Kernel.agda
@@ -29,7 +29,7 @@ module _ {R S : Ring ℓ} (f′ : RingHom R S) where
     f = fst f′
 
   kernel : fst R → hProp ℓ
-  kernel x = (f x ≡ 0r) , isSetRing S _ _
+  kernel x = (f x ≡ 0r) , is-set _ _
 
   kernelIsIdeal : isIdeal R kernel
   +-closed kernelIsIdeal =
diff --git a/Cubical/Algebra/Ring/Quotient.agda b/Cubical/Algebra/Ring/Quotient.agda
index 70141c6edb..b9dcd69143 100644
--- a/Cubical/Algebra/Ring/Quotient.agda
+++ b/Cubical/Algebra/Ring/Quotient.agda
@@ -234,7 +234,7 @@ module UniversalProperty (R : Ring ℓ) (I : IdealsIn R) where
     inducedHom : ((x : ⟨ R ⟩) → x ∈ Iₛ → φ $r x ≡ 0r) → RingHom (R / I) S
     fst (inducedHom Iₛ⊆kernel) =
       elim
-        (λ _ → isSetRing S)
+        (λ _ → is-set)
         f
         λ r₁ r₂ r₁-r₂∈I → equalByDifference (f r₁) (f r₂)
           (f r₁ - f r₂     ≡⟨ cong (λ u → f r₁ + u) (sym (φ.pres- _)) ⟩
@@ -244,11 +244,11 @@ module UniversalProperty (R : Ring ℓ) (I : IdealsIn R) where
     pres0 (snd (inducedHom Iₛ⊆kernel)) = φ.pres0
     pres1 (snd (inducedHom Iₛ⊆kernel)) = φ.pres1
     pres+ (snd (inducedHom Iₛ⊆kernel)) =
-      elimProp2 (λ _ _ → isSetRing S _ _) φ.pres+
+      elimProp2 (λ _ _ → is-set _ _) φ.pres+
     pres· (snd (inducedHom Iₛ⊆kernel)) =
-      elimProp2 (λ _ _ → isSetRing S _ _) φ.pres·
+      elimProp2 (λ _ _ → is-set _ _) φ.pres·
     pres- (snd (inducedHom Iₛ⊆kernel)) =
-      elimProp (λ _ → isSetRing S _ _) φ.pres-
+      elimProp (λ _ → is-set _ _) φ.pres-
 
     solution : (p : ((x : ⟨ R ⟩) → x ∈ Iₛ → φ $r x ≡ 0r))
                → (x : ⟨ R ⟩) → inducedHom p $r [ x ] ≡ φ $r x
diff --git a/Cubical/Algebra/Semilattice/Base.agda b/Cubical/Algebra/Semilattice/Base.agda
index 22315122ea..dd06511816 100644
--- a/Cubical/Algebra/Semilattice/Base.agda
+++ b/Cubical/Algebra/Semilattice/Base.agda
@@ -124,11 +124,10 @@ isPropIsSemilattice : {L : Type ℓ} (ε : L) (_·_ : L → L → L)
 isPropIsSemilattice ε _·_ (issemilattice LL LC) (issemilattice SL SC) =
   λ i → issemilattice (isPropIsCommMonoid _ _ LL SL i) (isPropIdem LC SC i)
   where
-  isSetL : isSet _
-  isSetL = LL .IsCommMonoid.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set
+  open IsCommMonoid LL using (is-set)
 
   isPropIdem : isProp ((x : _) → x · x ≡ x)
-  isPropIdem = isPropΠ λ _ → isSetL _ _
+  isPropIdem = isPropΠ λ _ → is-set _ _
 
 𝒮ᴰ-Semilattice : DUARel (𝒮-Univ ℓ) SemilatticeStr ℓ
 𝒮ᴰ-Semilattice =
diff --git a/Cubical/Categories/DistLatticeSheaf/Extension.agda b/Cubical/Categories/DistLatticeSheaf/Extension.agda
index c37bb6053e..600e1188f2 100644
--- a/Cubical/Categories/DistLatticeSheaf/Extension.agda
+++ b/Cubical/Categories/DistLatticeSheaf/Extension.agda
@@ -94,7 +94,7 @@ module PreSheafExtension (L : DistLattice ℓ) (C : Category ℓ' ℓ'')
   open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L))
   open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice L))
       using (∧≤RCancel ; ∧≤LCancel ; ≤-∧Pres ; ≤-∧RPres ; ≤-∧LPres)
-  open PosetStr (IndPoset .snd) hiding (_≤_)
+  open PosetStr (IndPoset .snd) hiding (_≤_; is-set)
   open IsBasis ⦃...⦄
   open EquivalenceOfDefs L C (DLRan F)
   open condCone
@@ -423,7 +423,7 @@ module PreSheafExtension (L : DistLattice ℓ) (C : Category ℓ' ℓ'')
           Σpathhelperpath = isSetL' _ _ _ _
            where
            isSetL' : isSet (ob DLSubCat)
-           isSetL' = isSetΣSndProp (isSetDistLattice L) λ x → L' x .snd
+           isSetL' = isSetΣSndProp is-set λ x → L' x .snd
 
           helperPathP : PathP (λ j → C [ c , F .F-ob (Σpathhelper (~ j)) ])
                               (uniqβConeMor c cc (α i) (α∈L' i) (ind≤⋁ α i) .fst .fst)
diff --git a/Cubical/HITs/FreeGroup/Properties.agda b/Cubical/HITs/FreeGroup/Properties.agda
index d3bdc748c8..d108d78a4a 100644
--- a/Cubical/HITs/FreeGroup/Properties.agda
+++ b/Cubical/HITs/FreeGroup/Properties.agda
@@ -152,10 +152,11 @@ elimProp {B = B} Bprop η-ind ·-ind ε-ind inv-ind = induction where
 freeGroupHom≡ : {Group : Group ℓ'}{f g : GroupHom (freeGroupGroup A) Group}
                → (∀ a → (fst f) (η a) ≡ (fst g) (η a)) → f ≡ g
 freeGroupHom≡ {Group = G , (groupstr 1g _·g_ invg isGrp)} {f} {g} eqOnA = GroupHom≡ (funExt pointwise) where
+  open IsGroup isGrp using (is-set)
   B : ∀ x → Type _
   B x = (fst f) x ≡ (fst g) x
   Bprop : ∀ x → isProp (B x)
-  Bprop x = (isSetGroup (G , groupstr 1g _·g_ invg isGrp)) ((fst f) x) ((fst g) x)
+  Bprop x = is-set ((fst f) x) ((fst g) x)
   η-ind : ∀ a → B (η a)
   η-ind = eqOnA
   ·-ind : ∀ g1 g2 → B g1 → B g2 → B (g1 · g2)