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}