Martin Escardo 2012. Lots of trivial isomorphisms.

\begin{code}

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

module IsomorphismOld where

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

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' ,  funext r'' , funext 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)

empty-is-empty : {X : Set}  empty X  X
empty-is-empty f = (f , unique-from-∅ , funext r , funext s)
where
r :  y  f(unique-from-∅ y)  y
r y = unique-from-∅ y
s :  x  unique-from-∅(f x)  x
s x = unique-from-∅(f x)

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

only-one-iso : {X : Set}  X  hprop X  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 = funext only-one
s : g  f  id
s = funext(h x)

empty-is-one : {X : Set}  empty X  empty X  𝟙
empty-is-one f = only-one-iso f  g h  funext  x  unique-from-∅ (g x)))

lemma[∅×Y≅∅] : {Y : Set}   × Y
lemma[∅×Y≅∅] {Y} = (f , g , funext r , funext 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 , funext r , funext 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 , funext r , funext 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'' , funext r'' , funext 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 , funext r , funext 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 , funext r , funext 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'' , funext r'' , funext 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 , funext r , funext 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 = funext (λ())

lemma[[𝟙→∅]≅∅] : (𝟙  )
lemma[[𝟙→∅]≅∅] = (f , g , funext r , funext 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' , funext r' , funext 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' = funext 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 = funext lemma
where
lemma :  x  g' (f' h) x  h x
lemma x = cong h (cong  u  u x) s)

\end{code}