{-# OPTIONS --without-K #-}
{-# OPTIONS --universe-polymorphism #-}
module Relation.Binary.Bijection where

open import Level
open import Function
open import Data.Sum
open import Relation.Binary
import Relation.Binary.PropositionalEquality as 
open  using (_≡_;_≢_)

InjectiveREL :  {a b } (A : Set a) (B : Set b)  REL A B   Set _
InjectiveREL _ _ _∼_ =  {x y z}  x  z  y  z  x  y

InjectiveRel :  {a } (A : Set a)  Rel A   Set _
InjectiveRel A = InjectiveREL A A

SurjectiveREL :  {a b } (A : Set a) (B : Set b)  REL A B   Set _
SurjectiveREL A B  = InjectiveREL B A (flip )

SurjectiveRel :  {a } (A : Set a)  Rel A   Set _
SurjectiveRel A = SurjectiveREL A A

record BijectiveREL {a b } (A : Set a) (B : Set b) ( : REL A B ) : Set (  a  b) where
  constructor mkBijectiveREL
  field
    injectiveREL  : InjectiveREL A B 
    surjectiveREL : SurjectiveREL A B 

BijectiveRel :  {a } (A : Set a) ( : Rel A )  Set _
BijectiveRel A = BijectiveREL A A

{-
private
  -- probably already defined somewhere
  _`on`_ : ∀ {a ℓ} {A : Set a} (f : A → A) → Rel A ℓ → Rel A ℓ
  _`on`_ f _∼_ i j = f i ∼ f j

module Pres-Bij-Props
                 {a} {A : Set a}
                 (f : A → A)
                 (f-inj : ∀ {i j} → f i ≡ f j → i ≡ j) where
  pres-bij : ∀ {ℓ} {α : Rel A ℓ} → BijectiveREL A A α → BijectiveREL A A (f `on` α)
  pres-bij {_} {α} α-bij
     = record { injectiveREL = λ {x} {y} {z} → α+-inj {x} {y} {z}
              ; surjectiveREL = λ {x} {y} {z} → α+-sur {x} {y} {z} }
     where
       open BijectiveREL α-bij renaming (injectiveREL to α-inj; surjectiveREL to α-sur)
       α+-inj : InjectiveREL A A (f `on` α)
       α+-inj fx⟨α⟩fz fy⟨α⟩fz = f-inj (α-inj fx⟨α⟩fz fy⟨α⟩fz)
       α+-sur : SurjectiveREL A A (f `on` α)
       α+-sur fx⟨α⟩fz fy⟨α⟩fz = f-inj (α-sur fx⟨α⟩fz fy⟨α⟩fz)
-}