Bijective functions on setoids

This is the Overture.Func.Bijective module of the agda-algebras library.

A bijective function from a setoid `๐จ = (A, โโ)` to a setoid `๐ฉ = (B, โโ)` is a function `f : ๐จ โถ ๐ฉ` that is both injective and surjective. (See the definitions in the modules Overture.Func.Injective and Overture.Func.Surjective.

```{-# OPTIONS --without-K --exact-split --safe #-}

open import Relation.Binary using ( Setoid )

module Overture.Func.Bijective {ฮฑ ฯแต ฮฒ ฯแต }{๐จ : Setoid ฮฑ ฯแต}{๐ฉ : Setoid ฮฒ ฯแต} where

-- Imports from Agda and the Agda Standard Library --------------------------
open import Agda.Primitive    using ( _โ_ ; Level ) renaming ( Set to Type )
open import Data.Product      using ( _,_ ; _ร_ )

-- Imports from agda-algebras -----------------------------------------------
open import Overture.Func.Preliminaries using ( _โถ_ )
open import Overture.Func.Inverses using ( Image_โ_ ; Inv )
open import Overture.Func.Surjective using ( IsSurjective )
open import Overture.Func.Injective using ( IsInjective )

open Image_โ_

open Setoid ๐จ using () renaming (Carrier to A; _โ_ to _โโ_)
open Setoid ๐ฉ using ( sym ; trans ) renaming (Carrier to B; _โ_ to _โโ_)

IsBijective : (๐จ โถ ๐ฉ) โ Type (ฮฑ โ ฮฒ โ ฯแต โ ฯแต)
IsBijective f = IsInjective f ร IsSurjective f

BijInv : (f : ๐จ โถ ๐ฉ) โ IsBijective f โ ๐ฉ โถ ๐จ
BijInv f (fM , fE) = record { f = finv ; cong = c }
where
finv : B โ A
finv b = Inv f fE

handler : โ {bโ bโ}(iโ : Image f โ bโ)(iโ : Image f โ bโ)
โ        bโ โโ bโ โ (Inv f iโ) โโ (Inv f iโ)

handler (eq a x) (eq aโ xโ) bโโbโ = fM (trans (sym x) (trans bโโbโ xโ))

c : โ {bโ bโ} โ bโ โโ bโ โ (finv bโ) โโ (finv bโ)
c bโโbโ = handler fE fE bโโbโ

```