Programming Language Foundations in Agda: Isomorphism

Isomorphism.agda

module Isomorphism where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(f ∘ g) x = f (g x)

_∘'_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘' g = λ x → f (g x)

postulate
    extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
    ∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀ (a : A) → B a}
        → (∀ (a : A) → f a ≡ g a) → f ≡ g

_+'_ : ℕ → ℕ → ℕ
a +' zero  = a
a +' suc b = suc (a +' b)

same-app : ∀ (a b : ℕ) → a +' b ≡ a + b
same-app a b rewrite +-comm a b = go a b
    where
    go : ∀ (a b : ℕ) → a +' b ≡ b + a
    go a zero    = refl
    go a (suc b) = cong suc (go a b)

same : _+'_ ≡ _+_
same = extensionality (λ a → extensionality (λ b → same-app a b))

record _≃_ (A B : Set) : Set where

    field
        to   : A → B
        from : B → A
        from∘to : ∀ (x : A) → from (to x) ≡ x
        to∘from : ∀ (x : B) → to (from x) ≡ x

open _≃_

infix 0 _≃_

≃-refl : ∀ {A : Set} → A ≃ A
≃-refl =
    record
        { to      = λ x → x
        ; from    = λ x → x
        ; from∘to = λ x → refl
        ; to∘from = λ x → refl
        }

≃-sym : ∀ {A B : Set} → A ≃ B → B ≃ A
≃-sym A≃B =
    record
        { to      = from A≃B
        ; from    = to A≃B
        ; from∘to = to∘from A≃B
        ; to∘from = from∘to A≃B
        }

≃-trans : ∀ {A B C : Set} → A ≃ B → B ≃ C → A ≃ C
≃-trans A≃B B≃C =
    record
        { to      = to B≃C ∘ to A≃B
        ; from    = from A≃B ∘ from B≃C
        ; from∘to = λ { x →
                begin
                    from A≃B (from B≃C (to B≃C (to A≃B x)))
                ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
                    from A≃B (to A≃B x)
                ≡⟨ from∘to A≃B x ⟩
                    x
                ∎
            }
        ; to∘from = λ { x →
                begin
                    to B≃C (to A≃B (from A≃B (from B≃C x)))
                ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C x)) ⟩
                    to B≃C (from B≃C x)
                ≡⟨ to∘from B≃C x ⟩
                    x
                ∎
            }
        }

module ≃-Reasoning where

    infix  1 ≃-begin_
    infixr 2 _≃⟨_⟩_
    infix  3 _≃-∎

    ≃-begin_ : ∀ {A B : Set} → A ≃ B → A ≃ B
    ≃-begin A≃B = A≃B

    _≃⟨_⟩_ : ∀ (A : Set) {B C : Set} → A ≃ B → B ≃ C → A ≃ C
    A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

    _≃-∎ : ∀ (A : Set) → A ≃ A
    A ≃-∎ = ≃-refl

open ≃-Reasoning

record _≲_ (A B : Set) : Set where

    field
        to   : A → B
        from : B → A
        from∘to : ∀ (x : A) → from (to x) ≡ x

open _≲_

infix 0 _≲_

≲-refl : ∀ {A : Set} → A ≲ A
≲-refl =
    record
        { to      = λ x → x
        ; from    = λ x → x
        ; from∘to = λ x → refl
        }

≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C =
    record
        { to      = to B≲C ∘ to A≲B
        ; from    = from A≲B ∘ from B≲C
        ; from∘to = λ { x →
                begin
                    from A≲B (from B≲C (to B≲C (to A≲B x)))
                ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
                    from A≲B (to A≲B x)
                ≡⟨ from∘to A≲B x ⟩
                    x
                ∎
            }
        }

≲-antisym : ∀ {A B : Set} → (A≲B : A ≲ B) → (B≲A : B ≲ A)
    → (to A≲B ≡ from B≲A) → (from A≲B ≡ to B≲A) → A ≃ B
≲-antisym AB BA tf ft =
    record
        { to      = to AB
        ; from    = from AB
        ; from∘to = from∘to AB
        ; to∘from = λ { x → -- (x : B) → to AB (from AB x) ≡ x
                begin
                    to AB (from AB x)
                ≡⟨ cong-app tf (from AB x) ⟩
                    from BA (from AB x)
                ≡⟨ cong (from BA) (cong-app ft x) ⟩
                    from BA (to BA x)
                ≡⟨ from∘to BA x ⟩
                    x
                ∎
            }
        }

module ≲-Reasoning where

    infix  1 ≲-begin_
    infixr 2 _≲⟨_⟩_
    infix  3 _≲-∎

    ≲-begin_ : ∀ {A B : Set} → A ≲ B → A ≲ B
    ≲-begin A≲B = A≲B

    _≲⟨_⟩_ : ∀ (A : Set) {B C : Set} → A ≲ B → B ≲ C → A ≲ C
    A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

    _≲-∎ : ∀ (A : Set) → A ≲ A
    A ≲-∎ = ≲-refl

open ≲-Reasoning

≃-implies-≲ : ∀ {A B : Set} → A ≃ B → A ≲ B
≃-implies-≲ AB =
    record
        { to      = to AB
        ; from    = from AB
        ; from∘to = from∘to AB
        }

record _⇔_ (A B : Set) : Set where

    field
        to   : A → B
        from : B → A

open _⇔_

⇔-refl : {A : Set} → A ⇔ A
⇔-refl =
    record
        { to   = λ x → x
        ; from = λ x → x
        }

⇔-sym : {A B : Set} → A ⇔ B → B ⇔ A
⇔-sym AB =
    record
        { to   = from AB
        ; from = to AB
        }

⇔-trans : {A B C : Set} → A ⇔ B → B ⇔ C → A ⇔ C
⇔-trans AB BC =
    record
        { to   = to BC ∘ to AB
        ; from = from AB ∘ from BC
        }

data Bin : Set where
  <> : Bin
  _O : Bin → Bin
  _I : Bin → Bin

infixl 10 _O
infixl 10 _I

-- Proofs: https://gist.github.com/pedrominicz/0f8feb3783eb75eca8df7483a36626de
postulate
    to' : ℕ → Bin
    from' : Bin → ℕ
    from∘to' : ∀ (n : ℕ) → from' (to' n) ≡ n

Nat≲Bin : ℕ ≲ Bin
Nat≲Bin =
    record
        { to      = to'
        ; from    = from'
        ; from∘to = from∘to'
        }