module NaPa.LogicalRelation.Bijection where

open import Data.Nat             using (zero; suc)
open import Data.Nat.Logical     using (zero; suc)
open import Function.Equality    using (_⟶_; _⟨$⟩_)
open import Function.Injection   using (module Injection)
open import Function.Surjection  using (Surjective)
open import Function.LeftInverse using (_LeftInverseOf_)
open import Function.Bijection   using (Bijective)
open import NaPa                 using (Nm; Name→-to-Nm⟶; _↑1; _+1; lift↑1; predNm; su; _,_)
open import NaPa.LogicalRelation using (⟦World⟧; _⟦↑1⟧; _⟦+1⟧)

_⟦↑1⟧-bij : ∀ {α₁ α₂} (αᵣ : ⟦World⟧ α₁ α₂) → Bijective (Injection.to αᵣ) → Bijective (Injection.to (αᵣ ⟦↑1⟧)) 
_⟦↑1⟧-bij {α₁} {α₂} αᵣ αᵣ-bij = record { injective = injective; surjective = to-surj } where
  open Injection (αᵣ ⟦↑1⟧)
  from : Nm (α₂ ↑1) ⟶ Nm (α₁ ↑1)
  from = Name→-to-Nm⟶ (lift↑1 (_⟨$⟩_ (Bijective.from αᵣ-bij)))
  to-left-inv-from : to LeftInverseOf from
  to-left-inv-from (zero ,  _)   = zero
  to-left-inv-from (suc n , pfx) = suc (Bijective.right-inverse-of αᵣ-bij (n , pfx))
  to-surj : Surjective to
  to-surj = record { from = from; right-inverse-of = to-left-inv-from }

_⟦+1⟧-bij : ∀ {α₁ α₂} (αᵣ : ⟦World⟧ α₁ α₂) → Bijective (Injection.to αᵣ) → Bijective (Injection.to (αᵣ ⟦+1⟧)) 
_⟦+1⟧-bij {α₁} {α₂} αᵣ αᵣ-bij = record { injective = injective; surjective = sur } where
  open Injection (αᵣ ⟦+1⟧)
  from : Nm (α₂ +1) ⟶ Nm (α₁ +1)
  from = Name→-to-Nm⟶ (λ x → su (Bijective.from αᵣ-bij ⟨$⟩ (predNm x)))
  to-left-inv-from : to LeftInverseOf from
  to-left-inv-from (zero  , ())
  to-left-inv-from (suc n , p) = suc (Bijective.right-inverse-of αᵣ-bij (n , p))
  sur : Surjective to
  sur = record { from = from; right-inverse-of = to-left-inv-from }