{-# OPTIONS --universe-polymorphism #-}
module Relation.Binary.On.NP where

import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≡_;_≢_)
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