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}