Remove the instance

agda · Jan 13, 2025 · 933df36 · 933df36
1 parent ae50c10
commit 933df36
Showing 1 changed file with 0 additions and 6 deletions.
diff --git 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)