Isomorphism vs. Bijection

gistfile1.hs

{-
  @author: Wojciech Jedynak (wjedynak@gmail.com)
-}

{-
2012-03-11

We show that the notions of isomorphism and bijection coincide in type theory.

This follows because from a constructive proof of surjectivity of a function f 
we must be able to extract the inverse of f.
-}

module isomorphism where

open import Data.Product

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

open ≡-Reasoning

--------------------------
--  Some basic notions  --
--------------------------

Injection : {A B : Set} → (A → B) → Set
Injection {A} f = (a a' : A) → f a ≡ f a' → a ≡ a'

Surjection : {A B : Set} → (A → B) → Set
Surjection {B = B} f = (b : B) → ∃ (λ a → f a ≡ b)

ComposeId : {A B : Set} → (A → B) → (B → A) → Set
ComposeId {B = B} f g = (b : B) → f (g b) ≡ b

--------------------------------------------------------------------------------------------
--  If both compositions of a pair of functions are identities, then they are bijections  --
--------------------------------------------------------------------------------------------

module Iso2Bij
  (A : Set)
  (B : Set)
  (f : A → B)
  (g : B → A)
  (f-g : ComposeId f g)
  (g-f : ComposeId g f)
  where
    f-injection : Injection f
    f-injection a a' eq = begin
      a          ≡⟨ sym (g-f a) ⟩
      g (f a)    ≡⟨ cong g eq ⟩
      g (f a')   ≡⟨ g-f a' ⟩
      a'
     ∎ where open ≡-Reasoning

    f-surjection : Surjection f
    f-surjection b = g b , f-g b

----------------------------------
--  A bijection has an inverse  --
----------------------------------

module Bij2Iso
  (A : Set)
  (B : Set)
  (f : A → B)
  (f-inj : Injection f)
  (f-sur : Surjection f)
  where
    f-inv : B → A
    f-inv b with f-sur b
    ... | a , _ = a

    f-g : ComposeId f f-inv
    f-g b with f-sur b
    ... | a , prf = prf

    g-f : ComposeId f-inv f
    g-f a with f-sur (f a)
    ... | a' , prf = f-inj a' a prf

-----------------------------------------------------
--  The same development, but packed into records  --
-----------------------------------------------------

record Isomorphism (A B : Set) : Set where
  constructor iso
  field
    f   : A → B
    g   : B → A
    f-g : ComposeId f g
    g-f : ComposeId g f

record Bijection (A B : Set) : Set where
  constructor bij
  field
    fun : A → B
    inj : Injection  fun
    sur : Surjection fun

iso2bij : ∀ {A B} → Isomorphism A B → Bijection A B
iso2bij (iso f g f-g g-f) = record { fun = f 
                                   ; inj = f-injection
                                   ; sur = f-surjection
                                   }
  where
    open Iso2Bij _ _ f g f-g g-f

bij2iso : ∀ {A B} → Bijection A B → Isomorphism A B
bij2iso (bij fun inj sur) = record { f   = fun
                                   ; g   = f-inv
                                   ; f-g = f-g
                                   ; g-f = g-f
                                   }
  where
    open Bij2Iso _ _ fun inj sur

iso-swap : ∀ {A B} → Isomorphism A B → Isomorphism B A
iso-swap (iso f g f-g g-f) = iso g f g-f f-g

bij-swap : ∀ {A B} → Bijection A B → Bijection B A
bij-swap = iso2bij ∘ iso-swap ∘ bij2iso 
  where
    open import Function