โ†‘ Top


Bijective functions on setoids

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


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

open import Relation.Binary using ( Setoid )

module Setoid.Overture.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 ( _,_ ; _ร—_ )
open import Function.Bundles  using ()               renaming ( Func to _โŸถ_ )

-- Imports from agda-algebras -----------------------------------------------
open import Setoid.Overture.Inverses    using ( Image_โˆ‹_ ; Inv )
open import Setoid.Overture.Surjective  using ( IsSurjective )
open import Setoid.Overture.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โ‚


โ† Setoid.Overture.Surjective