module PLFA.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)
-- * -- lambda expressions
-- so far : function definitions by name
add : ℕ → ℕ → ℕ
add m n = m + n
add' : ℕ → ℕ → ℕ
add' = λ (m : ℕ) → λ (n : ℕ) → m + n
ind : ℕ → ℕ
ind zero = 1
ind (suc n) = zero
ind' : ℕ → ℕ
ind' = λ{ zero → 1 ; (suc x) → zero }
ind-x≡ind'-x : ∀ x → ind x ≡ ind' x
ind-x≡ind'-x zero = refl
ind-x≡ind'-x (suc x) = refl
-- * -- function composition
-- f : A -> B, g : B -> C
-- want to compose f and g and use the result as a new function g ∘ f
_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘ f = λ a → g (f a)
_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘′ f) a = g (f a)
-- * -- extensionality
-- := two functions are equal iff they yield equal results for all arguments
cong-app′ : ∀ {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
cong-app′ refl = λ x → refl
-- but the reverse direction cannot be proved in Agda!
-- but it is consistent with Agda's logic.
-- let's add the reverse direction as an axiom
postulate
extensionality : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
ind≡ind' : ind ≡ ind'
ind≡ind' = extensionality ind-x≡ind'-x
_+′_ : ℕ → ℕ → ℕ
m +′ zero = m
m +′ suc n = suc (m +′ n)
same-add : ∀ m n → m +′ n ≡ m + n
same-add m n rewrite +-comm m n = helper m n
where helper : ∀ m n → m +′ n ≡ n + m
helper m zero = refl
helper m (suc n) = cong suc (helper m n)
add=add : _+′_ ≡ _+_
add=add = extensionality (λ x → extensionality (λ x₁ → same-add x x₁))
-- * -- isomorphism
infix 0 _≃_
-- two types A, B are isomorphic if (four conditions hold)
-- to : A → B
-- from : B → A
-- from ∘ to is the identity on A
-- to ∘ from is the identity on B
record _≃_ (A B : Set) : Set where
field
to : A → B
from : B → A
from∘to : ∀ (a : A) → from (to a) ≡ a
to∘from : ∀ (b : B) → to (from b) ≡ b
-- this notation is just syntactic sugar for a particular style of datatype definition
-- the above record corresponds to
data _≃′_ (A B : Set) : Set where
mk-≃′ : ∀ (to : A → B) →
∀ (from : B → A) →
∀ (from∘to : (∀ (a : A) → from (to a) ≡ a)) →
∀ (to∘from : ∀ (b : B) → to (from b) ≡ b) →
A ≃′ B
to' : ∀ {A B} → A ≃′ B → (A → B)
to' (mk-≃′ to from from∘to to∘from) = to
-- and so on
-- isomorphism is an equivalence
≃-refl : ∀ {A} → A ≃ A
≃-refl = record {
to = λ x → x ;
from = λ x → x ;
from∘to = λ a → refl ;
to∘from = λ b → refl
}
open _≃_
≃-sym : ∀ {A B} → A ≃ B → B ≃ A
≃-sym A≃B = record {
to = from A≃B ;
from = to A≃B ;
from∘to = λ b → to∘from A≃B b ;
to∘from = from∘to A≃B
}
≃-trans : ∀ {A B C} → 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 = λ a → begin
(from A≃B (from B≃C (to B≃C (to A≃B a)))
≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B a)) ⟩
from A≃B (to A≃B a)
≡⟨ from∘to A≃B a ⟩
a
∎) ;
to∘from = λ b → begin
(to B≃C (to A≃B (from A≃B (from B≃C b)))
≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C b)) ⟩
to B≃C (from B≃C b)
≡⟨ to∘from B≃C b ⟩
b
∎)
}
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
-- * -- embedding
infix 0 _≲_
record _≲_ (A B : Set) : Set where
field
to : A → B
from : B → A
from∘to : ∀ (a : A) → from (to a) ≡ a
open _≲_
-- embedding is a preorder (partial order)
-- reflexivity
≲-refl : {A : Set}
→ A ≲ A
≲-refl = record {
to = λ x → x ;
from = λ x → x ;
from∘to = λ a → refl
}
-- transitivity
≲-trans : {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C = record {
to = λ a → to B≲C (to A≲B a) ;
from = (from A≲B) ∘ (from B≲C) ;
from∘to = λ a → begin
(from A≲B (from B≲C (to B≲C (to A≲B a)))
≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B a)) ⟩
from A≲B (to A≲B a)
≡⟨ from∘to A≲B a ⟩
a
∎)
}
-- for a partial order, antisymmetry is required
≲-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 A≲B B≲A to-A≲B≡from-B≲A from-A≲B≡to-B≲A = record {
to = to A≲B ;
from = from A≲B ;
from∘to = λ a → from∘to A≲B a ;
to∘from = λ b → begin
to A≲B (from A≲B b)
≡⟨ cong (to A≲B) (cong-app from-A≲B≡to-B≲A b) ⟩
to A≲B (to B≲A b)
≡⟨ cong-app to-A≲B≡from-B≲A (to B≲A b) ⟩
from∘to B≲A b
}
-- equational-style reasoning for embeddings
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