Martin Escardo 2012. Lots of trivial isomorphisms.

\begin{code}

{-# OPTIONS --without-K #-}

module Isomorphism where

open import SetsAndFunctions
open import Equality
open import Extensionality
open import CurryHoward

infixr 10 _≅_

_≅_ : Set  Set  Prp
X  Y =  \(f : X  Y)   \(g : Y  X)  f  g  id  g  f  id

≅-refl : {X : Set}  X  X
≅-refl = (id , id , refl , refl)

≅-sym : {X Y : Set}  X  Y  Y  X
≅-sym (f , g , r , s) = (g , f , s , r)

≅-trans : {X Y Z : Set}  X  Y  Y  Z  X  Z
≅-trans (f , g , r , s) (f' , g' , r' , s') = (f'  f , g  g' ,  extensionality r'' , extensionality s'')
 where
  r'' :  z  f' (f (g (g' z)))  z
  r'' z = trans (cong f'(cong  t  t(g' z)) r)) (cong  u  u z) r')
  s'' :  x  g (g' (f' (f x)))  x
  s'' x = trans (cong g (cong  t  t(f x)) s')) (cong  u  u x) s)

only-one : ∀(x : )  *  x
only-one * = refl

only-one-iso : {X : Set}  inhabited X  (∀(x y : X)  x  y)  X  
only-one-iso {X} x h = (f , g , r , s)
 where
  f : X  
  f = unique-to-①
  g :   X
  g * = x
  r : f  g  id
  r = extensionality only-one
  s : g  f  id
  s = extensionality(h x)


lemma[∅×Y≅∅] : {Y : Set}   × Y  
lemma[∅×Y≅∅] {Y} = (f , g , extensionality r , extensionality s)
 where f :  × Y  
       f (() , y)
       g :    × Y
       g ()
       r :  x  f (g x)  x
       r ()
       s :  z  g (f z)  z
       s ((), y)

lemma[①×Y≅Y] : {Y : Set}   × Y  Y
lemma[①×Y≅Y] {Y} = (f , g , extensionality r , extensionality s)
 where f :  × Y  Y
       f (* , y) = y
       g : Y   × Y
       g y = (* , y)
       r :  x  f (g x)  x
       r y = refl
       s :  z  g (f z)  z
       s (* , y) = refl

lemma[X×Y≅Y×X] : {X Y : Set}  X × Y  Y × X
lemma[X×Y≅Y×X] {X} {Y} = (f , g , extensionality r , extensionality s)
 where f : X × Y  Y × X
       f (x , y) = (y , x)
       g : Y × X  X × Y
       g (y , x) = (x , y)
       r :  z  f (g z)  z
       r z = refl
       s :  t  g (f t)  t
       s t = refl

lemma[Y×①≅Y] : {Y : Set}  Y ×   Y
lemma[Y×①≅Y] = ≅-trans lemma[X×Y≅Y×X] lemma[①×Y≅Y]

lemma[Y×∅≅∅] : {Y : Set}  Y ×   
lemma[Y×∅≅∅] = ≅-trans lemma[X×Y≅Y×X] lemma[∅×Y≅∅]

lemma[X≅X'→Y≅Y'→[X×Y]≅[X'×Y']] : {X X' Y Y' : Set}  X  X'  Y  Y'  (X × Y)  (X' × Y')
lemma[X≅X'→Y≅Y'→[X×Y]≅[X'×Y']]  {X} {X'} {Y} {Y'} (f , g , r , s) (f' , g' , r' , s') = (f'' , g'' , extensionality r'' , extensionality s'')
 where f'' : X × Y  X' × Y'
       f'' (x , y) = (f x , f' y)
       g'' : X' × Y'  X × Y
       g'' (x' , y') = (g x' , g' y')
       r'' :  z'  f'' (g'' z')  z'
       r''(x' , y') = cong₂ _,_ lemma₀ lemma₁
         where lemma₀ : f(g x')  x'
               lemma₀ = cong  t  t x') r
               lemma₁ : f'(g' y')  y'
               lemma₁ = cong  u  u y') r'
       s'' :  z  g'' (f'' z)  z
       s''(x' , y') = cong₂ _,_ lemma₀ lemma₁
        where  lemma₀ : g(f x')  x'
               lemma₀ = cong  t  t x') s
               lemma₁ : g'(f' y')  y'
               lemma₁ = cong  u  u y') s'

lemma[X≅X'→X×Y≅X'×Y] : {X X' Y : Set}  X  X'  X × Y  X' × Y
lemma[X≅X'→X×Y≅X'×Y] {X} {X'} {Y} iso = lemma[X≅X'→Y≅Y'→[X×Y]≅[X'×Y']] iso ≅-refl

lemma[Y+∅≅Y] : {Y : Set}  Y +   Y
lemma[Y+∅≅Y] {Y} = (f , g , extensionality r , extensionality s)
 where f : Y +   Y
       f(in₀ y)= y
       f(in₁())
       g : Y  Y + 
       g y = in₀ y
       r :  y  f (g y)  y
       r y = refl
       s :  z  g (f z)  z
       s(in₀ y) = refl
       s(in₁())

lemma[X+Y≅Y+X] : {X Y : Set}  X + Y  Y + X
lemma[X+Y≅Y+X] {X} {Y} = (f , g , extensionality r , extensionality s)
 where f : X + Y  Y + X
       f(in₀ x) = in₁ x
       f(in₁ y) = in₀ y
       g : Y + X  X + Y
       g(in₀ y) = in₁ y
       g(in₁ x) = in₀ x
       r :  z  f (g z)  z
       r(in₀ y) = refl
       r(in₁ x) = refl
       s :  t  g (f t)  t
       s(in₀ x) = refl
       s(in₁ y) = refl

lemma[∅+Y≅Y] : {Y : Set}   + Y  Y
lemma[∅+Y≅Y] = ≅-trans lemma[X+Y≅Y+X] lemma[Y+∅≅Y]

lemma[X≅X'→Y≅Y'→[X+Y]≅[X'+Y']] : {X X' Y Y' : Set}  X  X'  Y  Y'  (X + Y)  (X' + Y')
lemma[X≅X'→Y≅Y'→[X+Y]≅[X'+Y']]   {X} {X'} {Y} {Y'} (f , g , r , s) (f' , g' , r' , s') =
 (f'' , g'' , extensionality r'' , extensionality s'')
 where f'' : X + Y  X' + Y'
       f''(in₀ x) = in₀(f x)
       f''(in₁ y) = in₁(f' y)
       g'' : X' + Y'  X + Y
       g''(in₀ x') = in₀(g x')
       g''(in₁ y') = in₁(g' y')
       r'' :  z'  f'' (g'' z')  z'
       r''(in₀ x') = cong in₀ (cong  h  h x') r)
       r''(in₁ y') = cong in₁ (cong  h  h y') r')
       s'' :  z  g'' (f'' z)  z
       s''(in₀ x) = cong in₀ (cong  h  h x) s)
       s''(in₁ y) = cong in₁ (cong  h  h y) s')


lemma[[∅→∅]≅①] : (  )  
lemma[[∅→∅]≅①] = (f , g , extensionality r , extensionality s)
 where f : (  )  
       f = unique-to-①
       g :   (  )
       g * = id
       r :  x  f (g x)  x
       r * = refl
       s :  h  g (f h)  h
       s h = extensionality (λ())

lemma[[①→∅]≅∅] : (  )  
lemma[[①→∅]≅∅] = (f , g , extensionality r , extensionality s)
 where f : (  )  
       f h = h *
       g :   (  )
       g x * = x
       r :  x  f (g x)  x
       r x = ⊥-elim x
       s :  h  g (f h)  h
       s h = ⊥-elim(h *)

lemma[X≅X'→[X→Y]≅[X'→Y]] : {X X' Y : Set}  X  X'  (X  Y)  (X'  Y)
lemma[X≅X'→[X→Y]≅[X'→Y]] {X} {X'} {Y} (f , g , r , s) = (f' , g' , extensionality r' , extensionality s')
 where f' : (X  Y)  (X'  Y)
       f' h = h  g
       g' : (X'  Y)  (X  Y)
       g' h' = h'  f
       r' :  h'  f' (g' h')  h'
       r' h' = extensionality lemma
        where lemma :  x'  f' (g' h') x'  h' x'
              lemma x' = cong h' (cong  t  t x') r)
       s' :  h  g' (f' h)  h
       s' h = extensionality lemma
        where lemma :  x  g' (f' h) x  h x
              lemma x = cong h (cong  u  u x) s)
\end{code}