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