```------------------------------------------------------------------------
-- The two definitions of context extensions are isomorphic
------------------------------------------------------------------------

open import Universe

module deBruijn.Context.Extension.Isomorphic
{i u e} (Uni : Indexed-universe i u e) where

import deBruijn.Context.Basics          as Basics
import deBruijn.Context.Extension.Left  as Left
import deBruijn.Context.Extension.Right as Right
open import Function
open import Function.Inverse using (_↔_)
import Relation.Binary.PropositionalEquality as P

open Basics Uni
open Left   Uni
open Right  Uni
open P.≡-Reasoning

-- Ctxt₊-s can be turned into Ctxt⁺-s.

₊-to-⁺ : ∀ {Γ} → Ctxt₊ Γ → Ctxt⁺ Γ
₊-to-⁺ ε        = ε
₊-to-⁺ (σ ◅ Γ₊) = ε ▻ σ ⁺++⁺ ₊-to-⁺ Γ₊

abstract

-- The semantics is preserved.

++⁺-₊-to-⁺ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ ++₊ Γ₊ ≅-Ctxt Γ ++⁺ ₊-to-⁺ Γ₊
++⁺-₊-to-⁺     ε        = P.refl
++⁺-₊-to-⁺ {Γ} (σ ◅ Γ₊) = begin
Γ ▻ σ ++₊ Γ₊                  ≡⟨ ++⁺-₊-to-⁺ Γ₊ ⟩
Γ ▻ σ ++⁺ ₊-to-⁺ Γ₊           ≡⟨ ++⁺-++⁺ (ε ▻ σ) (₊-to-⁺ Γ₊) ⟩
Γ ++⁺ (ε ▻ σ ⁺++⁺ ₊-to-⁺ Γ₊)  ∎

mutual

-- Ctxt⁺-s can be turned into Ctxt₊-s.

⁺-to-₊ : ∀ {Γ} → Ctxt⁺ Γ → Ctxt₊ Γ
⁺-to-₊ ε        = ε
⁺-to-₊ (Γ⁺ ▻ σ) =
⁺-to-₊ Γ⁺ ₊++₊ P.subst Ctxt₊ (++₊-⁺-to-₊ Γ⁺) (σ ◅ ε)

abstract

-- The semantics is preserved.

++₊-⁺-to-₊ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ ++⁺ Γ⁺ ≅-Ctxt Γ ++₊ ⁺-to-₊ Γ⁺
++₊-⁺-to-₊     ε        = P.refl
++₊-⁺-to-₊ {Γ} (Γ⁺ ▻ σ) =
let σ◅ε = P.subst Ctxt₊ (++₊-⁺-to-₊ Γ⁺) (σ ◅ ε)

in begin
Γ ++⁺ Γ⁺ ▻ σ                ≡⟨ P.refl ⟩
Γ ++⁺ Γ⁺ ++₊ (σ ◅ ε)        ≡⟨ P.sym \$ ++₊-cong \$ drop-subst-Ctxt₊ id (++₊-⁺-to-₊ Γ⁺) ⟩
Γ ++₊ ⁺-to-₊ Γ⁺ ++₊ σ◅ε     ≡⟨ ++₊-++₊ (⁺-to-₊ Γ⁺) σ◅ε ⟩
Γ ++₊ (⁺-to-₊ Γ⁺ ₊++₊ σ◅ε)  ∎

-- Some congruence lemmas.

₊-to-⁺-cong : ∀ {Γ₁} {Γ₊₁ : Ctxt₊ Γ₁}
{Γ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ₊-to-⁺ Γ₊₁ ≅-Ctxt⁺ ₊-to-⁺ Γ₊₂
₊-to-⁺-cong P.refl = P.refl

⁺-to-₊-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁}
{Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ⁺-to-₊ Γ⁺₁ ≅-Ctxt₊ ⁺-to-₊ Γ⁺₂
⁺-to-₊-cong P.refl = P.refl

-- Ctxt⁺ and Ctxt₊ are isomorphic.

Ctxt⁺↔Ctxt₊ : ∀ Γ → Ctxt⁺ Γ ↔ Ctxt₊ Γ
Ctxt⁺↔Ctxt₊ Γ = record
{ to         = P.→-to-⟶ ⁺-to-₊
; from       = P.→-to-⟶ ₊-to-⁺
; inverse-of = record
{ left-inverse-of  = λ Γ⁺ → ≅-Ctxt⁺-⇒-≡ \$ ₊-to-⁺-⁺-to-₊ Γ⁺
; right-inverse-of = λ Γ₊ → ≅-Ctxt₊-⇒-≡ \$ ⁺-to-₊-₊-to-⁺ Γ₊
}
}
where
abstract
₊-to-⁺-⁺-to-₊ : (Γ⁺ : Ctxt⁺ Γ) → ₊-to-⁺ (⁺-to-₊ Γ⁺) ≅-Ctxt⁺ Γ⁺
₊-to-⁺-⁺-to-₊ Γ⁺ = cancel-++⁺-left _ _ (begin
Γ ++⁺ ₊-to-⁺ (⁺-to-₊ Γ⁺)  ≡⟨ P.sym \$ ++⁺-₊-to-⁺ (⁺-to-₊ Γ⁺) ⟩
Γ ++₊ (⁺-to-₊ Γ⁺)         ≡⟨ P.sym \$ ++₊-⁺-to-₊ Γ⁺ ⟩
Γ ++⁺ Γ⁺                  ∎)

⁺-to-₊-₊-to-⁺ : (Γ₊ : Ctxt₊ Γ) → ⁺-to-₊ (₊-to-⁺ Γ₊) ≅-Ctxt₊ Γ₊
⁺-to-₊-₊-to-⁺ Γ₊ = cancel-++₊-left _ _ (begin
Γ ++₊ ⁺-to-₊ (₊-to-⁺ Γ₊)  ≡⟨ P.sym \$ ++₊-⁺-to-₊ (₊-to-⁺ Γ₊) ⟩
Γ ++⁺ (₊-to-⁺ Γ₊)         ≡⟨ P.sym \$ ++⁺-₊-to-⁺ Γ₊ ⟩
Γ ++₊ Γ₊                  ∎)
```