{-# 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 }
{-
  module Hom {a} {A B : Set a} (f : B → A) where
    substitutive : ∀ ℓ' {ℓ} {≈ : Rel A ℓ} → Substitutive ≈ ℓ' → Substitutive (≈ on f) ℓ'
    substitutive ℓ' subst P xᵣ Px = subst {!P ∘ f!} xᵣ {!!}
-}

open Base public

--equality : ∀ {a} {A B : Set a} {f : A → B} {≡ : Rel B a} (≡-eq : Equality ≡) → Equality (≡ on f)
--equality ≡-eq = record { isEquivalence = {!Equality.isEquivalence ≡-eq!}; subst = {!Equality.subst ≡-eq!} }