{-# OPTIONS --universe-polymorphism #-}
module Relation.Binary.On.NP where
import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≡_;_≢_;_with-≡_)
open import Function
open import Relation.Binary.Extras
import Relation.Binary.On
open import Relation.Binary.Bijection
private
module Base {a b} {A : Set a} {B : Set b} (f : B → A) where
open Relation.Binary.On {a} {b} {A} {B} f public
module Inj (f-inj : ∀ {i j} → f i ≡ f j → i ≡ j) where
injective : ∀ {ℓ} {∼ : Rel A ℓ} → InjectiveRel A ∼ → InjectiveRel B (∼ on f)
injective ∼-inj fx∼fz fy∼fz = f-inj (∼-inj fx∼fz fy∼fz)
surjective : ∀ {ℓ} {∼ : Rel A ℓ} → SurjectiveRel A ∼ → SurjectiveRel B (∼ on f)
surjective ∼-inj fx∼fz fy∼fz = f-inj (∼-inj fx∼fz fy∼fz)
bijective : ∀ {ℓ} {∼ : Rel A ℓ} → BijectiveRel A ∼ → BijectiveRel B (∼ on f)
bijective ∼-bij
= record { injectiveREL = injective (λ {x} {y} {z} → ∼-inj {x} {y} {z})
; surjectiveREL = surjective (λ {x} {y} {z} → ∼-sur {x} {y} {z}) }
where open BijectiveREL ∼-bij renaming (injectiveREL to ∼-inj; surjectiveREL to ∼-sur)
open Inj public
setoid : ∀ {ℓ} {≈ : Rel A ℓ} (≈-eqi : IsEquivalence ≈) → Setoid _ _
setoid {≈ = ≈} eqi = record { Carrier = B; _≈_ = ≈ on f; isEquivalence = isEquivalence eqi }
open Base public