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  _≅_

_≅_ : 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}