diff --git a/Cubical/Data/Sigma/Base.agda b/Cubical/Data/Sigma/Base.agda
index 44c9d189b..88f051a35 100644
--- a/Cubical/Data/Sigma/Base.agda
+++ b/Cubical/Data/Sigma/Base.agda
@@ -50,9 +50,3 @@ infix 2 ∃!-syntax
 ∃!-syntax = ∃!
 
 syntax ∃!-syntax A (λ x → B) = ∃![ x ∈ A ] B
-
--- Instance
-
-instance
-  Σ-instance : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} ⦃ x : A ⦄ ⦃ _ : B x ⦄ → Σ A B
-  Σ-instance ⦃ x ⦄ ⦃ y ⦄ = (x , y)