Martin Escardo, 27 April 2014

\begin{code}

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

module Isomorphism where

open import SetsAndFunctions
open import Equality

_∼_ : {X Y : Set}  (X  Y)  (X  Y)  Set
f  g =  x  f x  g x

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

infix 19 _≅_

Sym : {X Y : Set}  X  Y  Y  X 
Sym (f , g , fg , gf) = g , f , gf , fg

≅-trans : {X Y Z : Set}  X  Y  Y  Z  X  Z
≅-trans {X} {Y} {Z} (f , g , fg , gf) (f' , g' , fg' , gf')  = f'  f , g  g' , fg'' , gf''
 where
  fg'' : (z : Z)  f' (f (g (g' z)))  z
  fg'' z =  trans (cong f' (fg (g' z))) (fg' z)
  gf'' : (x : X)  g (g' (f' (f x)))  x
  gf'' x = trans (cong g (gf' (f x))) (gf x)

Curry-Uncurry : {X : Set} {Y : X  Set} {Z : (Σ \(x : X)  Y x)  Set}
   ((w : Σ \(x : X)  Y x)  Z w)  ((x : X) (y : Y x)  Z(x , y))
Curry-Uncurry {X} {Y} {Z} = c , u , cu , uc
 where
  c : ((w : Σ \(x : X)  Y x)  Z w)  ((x : X) (y : Y x)  Z(x , y))
  c f x y = f (x , y)
  u : ((x : X) (y : Y x)  Z(x , y))  ((w : Σ \(x : X)  Y x)  Z w) 
  u g (x , y) = g x y
  open import Extensionality
  cu :  g  c (u g)  g
  cu g = funext  x  funext  y  refl))
  uc :  f  u (c f)  f
  uc f = funext  w  refl)

Σ-congruence : (X : Set) (Y Y' : X  Set)
             ((x : X)  Y x  Y' x)  Σ Y  Σ Y'
Σ-congruence X Y Y' φ = (F , G , FG , GF)
 where
  f : (x : X)  Y x  Y' x
  f x = π₀(φ x)
  g : (x : X)  Y' x  Y x
  g x = π₀(π₁(φ x))
  fg : (x : X) (y' : Y' x)  f x (g x y')  y' 
  fg x = π₀(π₁(π₁(φ x)))
  gf : (x : X) (y : Y x)  g x (f x y)  y  
  gf x = π₁(π₁(π₁(φ x)))

  F : Σ Y  Σ Y'
  F (x , y) = x , f x y
  G : Σ Y'  Σ Y
  G (x , y') = x , (g x y')
  FG : (w' : Σ Y')  F(G w')  w'
  FG (x , y') = Σ-≡' x _ y' (fg x y')
  GF : (w : Σ Y)  G(F w)  w
  GF (x , y) = Σ-≡' x _ y (gf x y)

-- Not yet used, but for the record:
Π-congruence : (X : Set) (Y Y' : X  Set)
             ((x : X)  Y x  Y' x)  ((x : X)  Y x)  ((x : X)  Y' x)
Π-congruence X Y Y' φ = (F , G , FG , GF)
 where
  f : (x : X)  Y x  Y' x
  f x = π₀(φ x)
  g : (x : X)  Y' x  Y x
  g x = π₀(π₁(φ x))
  fg : (x : X) (y' : Y' x)  f x (g x y')  y' 
  fg x = π₀(π₁(π₁(φ x)))
  gf : (x : X) (y : Y x)  g x (f x y)  y  
  gf x = π₁(π₁(π₁(φ x)))

  F : ((x : X)  Y x)  ((x : X)  Y' x)
  F = λ z x  π₀ (φ x) (z x)
  G : ((x : X)  Y' x)  (x : X)  Y x 
  G = λ z x  π₀(π₁(φ x)) (z x)

  FG :  (w' : ((x : X)  Y' x))  F(G w')  w'
  FG w' = funext FG'
   where
    open import Extensionality
    FG' : (x : X)  F(G w') x  w' x
    FG' x = fg x (w' x)

  GF : (w : ((x : X)  Y x))  G(F w)  w
  GF w = funext GF'
   where
    open import Extensionality
    GF' : (x : X)  G(F w) x  w x
    GF' x = gf x (w x)


lemma[𝟙×Y≅Y] : {Y : Set}  𝟙 × Y  Y
lemma[𝟙×Y≅Y] {Y} = (f , g , fg , gf)
 where 
  f : 𝟙 × Y  Y
  f (* , y) = y
  g : Y  𝟙 × Y 
  g y = (* , y)
  fg :  x  f (g x)  x 
  fg y = refl 
  gf :  z  g (f z)  z
  gf (* , y) = refl

lemma[X×Y≅Y×X] : {X Y : Set}  X × Y  Y × X
lemma[X×Y≅Y×X] {X} {Y} = (f , g , fg , gf)
 where 
  f : X × Y  Y × X
  f (x , y) = (y , x)
  g : Y × X  X × Y
  g (y , x) = (x , y)
  fg :  z  f (g z)  z 
  fg z = refl 
  gf :  t  g (f t)  t
  gf t = 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 , fg , gf) (f' , g' , fg' , gf') = (f'' , g'' , fg'' , gf'')
 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')
  fg'' :  z'  f'' (g'' z')  z' 
  fg''(x' , y') = cong₂ _,_ lemma₀ lemma₁ 
   where 
    lemma₀ : f(g x')  x'
    lemma₀ = fg x' 
    lemma₁ : f'(g' y')  y'
    lemma₁ = fg' y' 
  gf'' :  z  g'' (f'' z)  z
  gf''(x' , y') = cong₂ _,_ lemma₀ lemma₁ 
    where  
     lemma₀ : g(f x')  x'
     lemma₀ = gf x'
     lemma₁ : g'(f' y')  y'
     lemma₁ = gf' y'

\end{code}