diff --git a/src/Data/Rational/Properties.lagda.md b/src/Data/Rational/Properties.lagda.md
index cc962ea56..acb7c6406 100644
--- a/src/Data/Rational/Properties.lagda.md
+++ b/src/Data/Rational/Properties.lagda.md
@@ -119,7 +119,6 @@ abstract
 
   /ℚ-frac
     : ∀ {n d} ⦃ p : ℤ.Positive d ⦄
-    → (let instance _ = to-nonzero-frac (ℤ.positive→nonzero p))
     → (n / 1) /ℚ (d / 1) ≡ (n / d)
   /ℚ-frac {n} {d = ℤ.possuc x} ⦃ p = ℤ.pos x ⦄ = quotℚ (to-same-rational (sym (ℤ.*ℤ-associative n 1 (ℤ.possuc x))))
 
diff --git a/src/Prim/Data/Sigma.lagda.md b/src/Prim/Data/Sigma.lagda.md
index 583eadaaf..c544b586f 100644
--- a/src/Prim/Data/Sigma.lagda.md
+++ b/src/Prim/Data/Sigma.lagda.md
@@ -39,8 +39,8 @@ syntax Σ-syntax X (λ x → F) = Σ[ x ∈ X ] F
 infix 4 Σ-syntax
 
 instance
-  make-Σ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} ⦃ x : A ⦄ ⦃ y : B x ⦄ → Σ A B
-  make-Σ ⦃ x ⦄ ⦃ y ⦄ = x , y
+  Σ-of-instances : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} ⦃ x : A ⦄ ⦃ y : B x ⦄ → Σ A B
+  Σ-of-instances ⦃ x ⦄ ⦃ y ⦄ = x , y
 ```
 -->