Remove some explicitly bound variables in type signatures

Author: WhatisRT

src/Data/Product/Function/Dependent/Propositional.agda

@@ -317,7 +317,5 @@ cong {B = B} {k = leftInverse}        I↔J A↩B = ↩⇒↪ (Σ-↩ (↔⇒↩
 cong {k = surjection}                 I↔J A↠B = Σ-↠ (↔⇒↠ I↔J) A↠B
 cong {k = bijection}                  I↔J A↔B = Σ-↔ I↔J A↔B
 
-cong′ : ∀ {k} → {A : Set a} {B₁ : A → Set b} {B₂ : A → Set c} →
-        (∀ {x} → B₁ x ∼[ k ] B₂ x) →
-        Σ A B₁ ∼[ k ] Σ A B₂
+cong′ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
 cong′ = cong (refl _)

src/Function/Related/TypeIsomorphisms.agda

@@ -357,6 +357,6 @@ True↔ (false because ofⁿ ¬p) _ =
 -- Relating a predicate to an existentially quantified one with the
 -- restriction that the quantified variable is equal to the given one
 
-∃-≡ : ∀ {A : Set a} (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
+∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
 ∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , (refl , Py)) → Py)
   (λ where (_ , refl , _) → refl) (λ where _ → refl)