{-# OPTIONS --universe-polymorphism #-} module Function.Injection.NP where open import Function.Injection public open import Function.Equality open import Relation.Binary open import Data.Product open import Level _∈_ : ∀ {a₁ a₂} {A₁ A₂ : Setoid a₁ a₂} (xᵢ : Setoid.Carrier A₁ × Setoid.Carrier A₂) (inj : Injection A₁ A₂) → Set a₂ _∈_ {A₂ = A₂} (x₁ , x₂) inj = Injection.to inj ⟨$⟩ x₁ ≈ x₂ where open Setoid A₂