diff --git a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
index 1eca7378bc..38f7632ab3 100644
--- a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
+++ b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
@@ -31,24 +31,24 @@ private
     ℓ : Level
 
 {-
-  The definition of the quotient algebra (_/_ below) is marked abstract to avoid
+  The definition of the quotient algebra (_/_ below) is marked opaque to avoid
   long type checking times. All other definitions that need to "look into" this
-  abstract definition must be in the same abstract scope. Note that anonymous
-  modules share an abstract scope but named modules do not.
+  opaque definition must be in an opaque block that unfolds the definition of _/_.
 -}
 
-module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
+module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
   open CommRingStr {{...}} hiding (_-_; -_; ·IdL ; ·DistR+) renaming (_·_ to _·R_; _+_ to _+R_)
   open CommAlgebraStr {{...}}
   open RingTheory (CommRing→Ring (CommAlgebra→CommRing A)) using (-DistR·)
   instance
-    _ : CommRingStr ⟨ R ⟩
+    _ : CommRingStr ⟨ R ⟩
     _ = snd R
     _ : CommAlgebraStr R ⟨ A ⟩
     _ = snd A
 
-  _/_ : CommAlgebra R ℓ
-  _/_ = commAlgebraFromCommRing
+  opaque
+    _/_ : CommAlgebra R ℓ
+    _/_ = commAlgebraFromCommRing
            A/IAsCommRing
            (λ r → elim (λ _ → squash/) (λ x → [ r ⋆ x ]) (eq r))
            (λ r s → elimProp (λ _ → squash/ _ _)
@@ -83,16 +83,19 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
                     r ⋆ x - r ⋆ y                   ∎ )
                   (isCommIdeal.·Closed (snd I) _ x-y∈I))
 
-  quotientHom : CommAlgebraHom A (_/_)
-  fst quotientHom x = [ x ]
-  IsAlgebraHom.pres0 (snd quotientHom) = refl
-  IsAlgebraHom.pres1 (snd quotientHom) = refl
-  IsAlgebraHom.pres+ (snd quotientHom) _ _ = refl
-  IsAlgebraHom.pres· (snd quotientHom) _ _ = refl
-  IsAlgebraHom.pres- (snd quotientHom) _ = refl
-  IsAlgebraHom.pres⋆ (snd quotientHom) _ _ = refl
+  opaque
+    unfolding _/_
+
+    quotientHom : CommAlgebraHom A (_/_)
+    fst quotientHom x = [ x ]
+    IsAlgebraHom.pres0 (snd quotientHom) = refl
+    IsAlgebraHom.pres1 (snd quotientHom) = refl
+    IsAlgebraHom.pres+ (snd quotientHom) _ _ = refl
+    IsAlgebraHom.pres· (snd quotientHom) _ _ = refl
+    IsAlgebraHom.pres- (snd quotientHom) _ = refl
+    IsAlgebraHom.pres⋆ (snd quotientHom) _ _ = refl
 
-module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
+module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
   open CommRingStr {{...}}
     hiding (_-_; -_; ·IdL; ·DistR+; is-set)
     renaming (_·_ to _·R_; _+_ to _+R_)
@@ -104,21 +107,24 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
     _ : CommAlgebraStr R ⟨ A ⟩
     _ = snd A
 
-  -- 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/ = idEquiv _
-  IsRingHom.pres0 (snd CommForget/) = refl
-  IsRingHom.pres1 (snd CommForget/) = refl
-  IsRingHom.pres+ (snd CommForget/) = λ _ _ → refl
-  IsRingHom.pres· (snd CommForget/) = λ _ _ → refl
-  IsRingHom.pres- (snd CommForget/) = λ _ → refl
+  opaque
+    unfolding _/_
+
+    -- 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/ = idEquiv _
+    IsRingHom.pres0 (snd CommForget/) = refl
+    IsRingHom.pres1 (snd CommForget/) = refl
+    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
+    where
 
     open IsAlgebraHom
     open RingTheory (CommRing→Ring (CommAlgebra→CommRing B))
@@ -130,95 +136,114 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
         _ : 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)
-            ((fst ϕ a) - (fst ϕ b)     ≡⟨ cong (λ u → (fst ϕ a) + u) (sym (IsAlgebraHom.pres- (snd ϕ) _)) ⟩
-             (fst ϕ a) + (fst ϕ (- b)) ≡⟨ sym (IsAlgebraHom.pres+ (snd ϕ) _ _) ⟩
-             fst ϕ (a - b)             ≡⟨ I⊆kernel (a - b) a-b∈I ⟩
-             0r ∎)
-    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 → 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
+    opaque
+      unfolding _/_
+
+      inducedHom : CommAlgebraHom (A / I) B
+      fst inducedHom =
+        rec is-set (λ x → fst ϕ x)
+          λ a b a-b∈I →
+            equalByDifference
+              (fst ϕ a) (fst ϕ b)
+              ((fst ϕ a) - (fst ϕ b)     ≡⟨ cong (λ u → (fst ϕ a) + u) (sym (IsAlgebraHom.pres- (snd ϕ) _)) ⟩
+               (fst ϕ a) + (fst ϕ (- b)) ≡⟨ sym (IsAlgebraHom.pres+ (snd ϕ) _ _) ⟩
+               fst ϕ (a - b)             ≡⟨ I⊆kernel (a - b) a-b∈I ⟩
+               0r ∎)
+      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)
+
+    opaque
+      unfolding inducedHom quotientHom
+
+      inducedHom∘quotientHom : inducedHom ∘a quotientHom A I ≡ ϕ
+      inducedHom∘quotientHom = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = B}) (funExt (λ a → refl))
+
+  opaque
+    unfolding quotientHom
+
+    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 → 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 -}
-module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where abstract
+module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
   open CommAlgebraStr (snd A)
 
-  oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal A)) (UnitCommAlgebra R {ℓ' = ℓ})
-  fst oneIdealQuotient =
-    isoToEquiv (iso (fst (terminalMap R (A / (1Ideal A))))
-                    (λ _ → [ 0a ])
-                    (λ _ → isPropUnit* _ _)
-                    (elimProp (λ _ → squash/ _ _)
-                              λ a → eq/ 0a a tt*))
-  snd oneIdealQuotient = snd (terminalMap R (A / (1Ideal A)))
-
-  zeroIdealQuotient : CommAlgebraEquiv A (A / (0Ideal A))
-  fst zeroIdealQuotient =
-    let open RingTheory (CommRing→Ring (CommAlgebra→CommRing A))
-    in isoToEquiv (iso (fst (quotientHom A (0Ideal A)))
-                    (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))
-
--- non-abstract notation
+  opaque
+    unfolding _/_
+
+    oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal A)) (UnitCommAlgebra R {ℓ' = ℓ})
+    fst oneIdealQuotient =
+      isoToEquiv (iso (fst (terminalMap R (A / (1Ideal A))))
+                      (λ _ → [ 0a ])
+                      (λ _ → isPropUnit* _ _)
+                      (elimProp (λ _ → squash/ _ _)
+                                λ a → eq/ 0a a tt*))
+    snd oneIdealQuotient = snd (terminalMap R (A / (1Ideal A)))
+
+  opaque
+    unfolding quotientHom
+
+    zeroIdealQuotient : CommAlgebraEquiv A (A / (0Ideal A))
+    fst zeroIdealQuotient =
+      let open RingTheory (CommRing→Ring (CommAlgebra→CommRing A))
+      in isoToEquiv (iso (fst (quotientHom A (0Ideal A)))
+                      (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))
+
 [_]/ : {R : CommRing ℓ} {A : CommAlgebra R ℓ} {I : IdealsIn A}
        → (a : fst A) → fst (A / I)
 [_]/ = fst (quotientHom _ _)
 
 
 
-module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
+module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where
   open CommIdeal using (isPropIsCommIdeal)
 
-  private module _ where
-    -- non-abstract abbreviation
+  private
     π : CommAlgebraHom A (A / I)
     π = quotientHom A I
 
-  kernel≡I : kernel A (A / I) π ≡ I
-  kernel≡I =
-    kernel A (A / I) π ≡⟨ Σ≡Prop
-                            (isPropIsCommIdeal (CommAlgebra→CommRing A))
-                            refl ⟩
-    _                  ≡⟨  CommRing.kernel≡I {R = CommAlgebra→CommRing A} I ⟩
-    I                  ∎
+  opaque
+    unfolding quotientHom
+
+    kernel≡I : kernel A (A / I) π ≡ I
+    kernel≡I =
+      kernel A (A / I) π ≡⟨ Σ≡Prop
+                              (isPropIsCommIdeal (CommAlgebra→CommRing A))
+                              refl ⟩
+      _                  ≡⟨  CommRing.kernel≡I {R = CommAlgebra→CommRing A} I ⟩
+      I                  ∎
 
 
 module _
   {R : CommRing ℓ}
   {A : CommAlgebra R ℓ}
   {I : IdealsIn A}
-  where abstract
+  where
 
-  isZeroFromIdeal : (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
-  isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (step x) x∈I )
-    where
-      open CommAlgebraStr (snd A)
-      step : (x : ⟨ A ⟩) → x ≡ x - 0a
-      step = solve (CommAlgebra→CommRing A)
+  opaque
+    unfolding quotientHom
+
+    isZeroFromIdeal : (x : ⟨ A ⟩) → x ∈ (fst I) → fst (quotientHom A I) x ≡ CommAlgebraStr.0a (snd (A / I))
+    isZeroFromIdeal x x∈I = eq/ x 0a (subst (_∈ fst I) (step x) x∈I )
+      where
+        open CommAlgebraStr (snd A)
+        step : (x : ⟨ A ⟩) → x ≡ x - 0a
+        step = solve (CommAlgebra→CommRing A)