\begin{code}
{-# OPTIONS --without-K #-}
module Isomorphism where
open import SetsAndFunctions
open import Equality
open import Extensionality
open import CurryHoward
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' , 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}