---
layout: default
title : "Setoid.Functions.Bijective module"
date : "2021-09-13"
author: "the agda-algebras development team"
---

### Bijective functions on setoids

This is the [Setoid.Functions.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 [Setoid.Functions.Injective][] and [Setoid.Functions.Surjective][].


<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Relation.Binary using ( Setoid )

module Setoid.Functions.Bijective {α ρᵃ β ρᵇ}{𝑨 : Setoid α ρᵃ}{𝑩 : Setoid β ρᵇ} where

-- Imports from Agda and the Agda Standard Library --------------------------
open import Agda.Primitive    using ( _⊔_ )  renaming ( Set to Type )
open import Data.Product      using ( _,_ ; _×_ )
open import Function.Bundles  using ()               renaming ( Func to _⟶_ )

-- Imports from agda-algebras -----------------------------------------------
open import Setoid.Functions.Inverses    using ( Image_∋_ ; Inv )
open import Setoid.Functions.Surjective  using ( IsSurjective )
open import Setoid.Functions.Injective   using ( IsInjective )

open Image_∋_

open Setoid 𝑨  using ()               renaming (Carrier to A; _≈_ to _≈₁_)
open Setoid 𝑩  using ( sym ; trans )  renaming (Carrier to B; _≈_ to _≈₂_)
```
-->

```agda
IsBijective : (𝑨 ⟶ 𝑩) → Type (α ⊔ β ⊔ ρᵃ ⊔ ρᵇ)
IsBijective f = IsInjective f × IsSurjective f

BijInv : (f : 𝑨 ⟶ 𝑩) → IsBijective f → 𝑩 ⟶ 𝑨
BijInv f (fM , fE) = record { to = 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₁
```