diff --git a/Cubical/Algebra/Algebra/Properties.agda b/Cubical/Algebra/Algebra/Properties.agda
index 0bffb60665..1631e45053 100644
--- a/Cubical/Algebra/Algebra/Properties.agda
+++ b/Cubical/Algebra/Algebra/Properties.agda
@@ -110,7 +110,7 @@ module AlgebraEquivs where
     (invAlgebraEquiv {A = A} {B = B} f').snd = hom
       where
         open AlgebraStr {{...}}
-        private instance
+        instance
           _ = snd A
           _ = snd B
 
diff --git a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
index 0c89652f21..1a11d384dd 100644
--- a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
+++ b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda
@@ -373,12 +373,10 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
                                       ; ·IdR to ·A-rid)
   open Units A' renaming (Rˣ to Aˣ ; RˣInvClosed to AˣInvClosed)
   open PathToS⁻¹R ⦃...⦄
-  private
-   A = fst A'
-   instance
-    _ = cond
-   χ = (S⁻¹RHasUniversalProp A' φ φS⊆Aˣ .fst .fst)
-   open RingHomTheory χ
+  A = fst A'
+  instance _ = cond
+  χ = (S⁻¹RHasUniversalProp A' φ φS⊆Aˣ .fst .fst)
+  open RingHomTheory χ
 
   S⁻¹R≃A : S⁻¹R ≃ A
   S⁻¹R≃A = fst χ , isEmbedding×isSurjection→isEquiv (Embχ , Surχ)
diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda
index 0ca7597380..a86dd5be80 100644
--- a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda
+++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheaf.agda
@@ -137,8 +137,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
     open S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) using (_/1)
     open RadicalIdeal R'
 
-    private
-     instance
+    instance
       _ = snd R[1/ f ]AsCommRing
 
     f∈√⟨g⟩ : f ∈ √ ⟨ g ⟩ₛ
diff --git a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda
index 41695c786a..452bcd4fbd 100644
--- a/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda
+++ b/Cubical/AlgebraicGeometry/ZariskiLattice/StructureSheafPullback.agda
@@ -158,8 +158,7 @@ module _ (R' : CommRing ℓ) where
     open S⁻¹RUniversalProp R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f) using (_/1)
     open RadicalIdeal R'
 
-    private
-     instance
+    instance
       _ = snd R[1/ f ]AsCommRing
 
     Df≤Dg : D f ≤ D g
diff --git a/Cubical/Categories/DistLatticeSheaf/Extension.agda b/Cubical/Categories/DistLatticeSheaf/Extension.agda
index 4687ad8189..417e43b762 100644
--- a/Cubical/Categories/DistLatticeSheaf/Extension.agda
+++ b/Cubical/Categories/DistLatticeSheaf/Extension.agda
@@ -736,11 +736,10 @@ module PreSheafExtension (L : DistLattice ℓ) (C : Category ℓ' ℓ'')
       s₁ (cospanPath i) = DLRan F .F-hom (≤m→≤j _ _ (∧≤LCancel _ _))
       s₂ (cospanPath i) = DLRan F .F-hom (≤m→≤j _ _ (∧≤RCancel _ _))
 
-      private
-        F[⋁β]Cone = limitC _ (F* (⋁ β)) .limCone
-        F[⋁γ]Cone = limitC _ (F* (⋁ γ)) .limCone
-        F[⋁β∧⋁γ]Cone = limitC _ (F* (⋁ β ∧l ⋁ γ)) .limCone
-        F[⋁β++γ]Cone = limitC _ (F* (⋁ (β ++Fin γ))) .limCone
+      F[⋁β]Cone = limitC _ (F* (⋁ β)) .limCone
+      F[⋁γ]Cone = limitC _ (F* (⋁ γ)) .limCone
+      F[⋁β∧⋁γ]Cone = limitC _ (F* (⋁ β ∧l ⋁ γ)) .limCone
+      F[⋁β++γ]Cone = limitC _ (F* (⋁ (β ++Fin γ))) .limCone
 
       -- the family of squares we need to construct cones over β++γ
       to++ConeSquare : {c : ob C} (f : C [ c , ⋁Cospan .l ]) (g : C [ c , ⋁Cospan .r ])
diff --git a/Cubical/Experiments/ZCohomologyOld/Properties.agda b/Cubical/Experiments/ZCohomologyOld/Properties.agda
index faaadde8c8..8d09d5de98 100644
--- a/Cubical/Experiments/ZCohomologyOld/Properties.agda
+++ b/Cubical/Experiments/ZCohomologyOld/Properties.agda
@@ -268,12 +268,12 @@ cancelₖ (suc (suc (suc (suc (suc n))))) x = cong (ΩKn+1→Kn (5 + n)) (rCance
                  ∙∙ cong (ΩKn+1→Kn (suc n)) (sym (rUnit (Kn→ΩKn+1 (suc n) x)))
                  ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 (suc n)) x
 
+open Iso renaming (inv to inv')
 abstract
   isCommΩK1 : (n : ℕ) → isComm∙ ((Ω^ n) (coHomK-ptd 1))
   isCommΩK1 zero = isCommA→isCommTrunc 2 comm-ΩS¹ isGroupoidS¹
   isCommΩK1 (suc n) = EH n
 
-  open Iso renaming (inv to inv')
   isCommΩK : (n : ℕ) → isComm∙ (coHomK-ptd n)
   isCommΩK zero p q = isSetℤ _ _ (p ∙ q) (q ∙ p)
   isCommΩK (suc zero) = isCommA→isCommTrunc 2 comm-ΩS¹ isGroupoidS¹