[Refractor] contradiction over ⊥-elim in ¬¬-pull def

Author: jmougeot

src/Relation/Nullary/Universe.agda

@@ -19,7 +19,7 @@ open import Function.Base using (_∘_; id)
 open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
 open import Level using (Level; _⊔_; suc; Lift; lift; lower)
 open import Relation.Nullary.Negation
-  using  (¬_; ¬¬-Monad; ¬¬-map; negated-stable)
+  using  (¬_; ¬¬-Monad; ¬¬-map; negated-stable; contradiction)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Construct.Always as Always using (setoid)
@@ -123,7 +123,7 @@ private
           ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
 ¬¬-pull = sequence rawApplicative
                    (λ f → f lower)
-                   (λ f g → g (λ x → ⊥-elim (f x (λ y → g (λ _ → y)))))
+                   (λ f g → g (λ x → contradiction (λ y → g (λ _ → y)) (f x )))
 
 ¬¬-remove : ∀ {p} (F : PropF p) {P} →
             ¬ ¬ ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P