Add infix declartions to exists syntax (#1340)

Author: Taneb

CHANGELOG.md

@@ -164,3 +164,5 @@ Other minor additions
   ```agda
   +-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
   ```
+
+* Added infix declarations to `Data.Product.∃-syntax` and `Data.Product.∄-syntax`.

src/Data/Product.agda

@@ -75,11 +75,15 @@ _,′_ = _,_
 
 -- Syntax
 
+infix 2 ∃-syntax
+
 ∃-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
 ∃-syntax = ∃
 
 syntax ∃-syntax (λ x → B) = ∃[ x ] B
 
+infix 2 ∄-syntax
+
 ∄-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
 ∄-syntax = ∄