module Bijection where

open import Equality
open import Function
open import Level

record
  isBij
    {ℓ ℓ' : Level}
    {A : Set ℓ}
    {B : Set ℓ'}
    (f : A → B)
    : ------------
    Set (ℓ ⊔ ℓ')
  where
  infix  _⁻¹
  field
    _⁻¹  : B → A
    bijl : _⁻¹ ∘ f ≡ id 
    bijr : f ∘ _⁻¹ ≡ id

open isBij{{...}} public