{-# 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