deBruijn.Context.Extension.Right

------------------------------------------------------------------------
-- Context extensions with the rightmost element in the outermost
-- position
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Context.Extension.Right
  {i u e} (Uni : IndexedUniverse i u e) where

import deBruijn.Context.Basics as Basics
open import Data.Product
open import Function
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Basics Uni
open P.≡-Reasoning

------------------------------------------------------------------------
-- Context extensions along with various operations making use of them

mutual

  -- Context extensions.

  infixl 5 _▻_

  data Ctxt⁺ (Γ : Ctxt) : Set (i ⊔ u ⊔ e) where
    ε   : Ctxt⁺ Γ
    _▻_ : (Γ⁺ : Ctxt⁺ Γ) (σ : Type (Γ ++⁺ Γ⁺)) → Ctxt⁺ Γ

  -- Appends a context extension to a context.

  infixl 5 _++⁺_

  _++⁺_ : (Γ : Ctxt) → Ctxt⁺ Γ → Ctxt
  Γ ++⁺ ε        = Γ
  Γ ++⁺ (Γ⁺ ▻ σ) = (Γ ++⁺ Γ⁺) ▻ σ

-- A synonym.

ε⁺[_] : (Γ : Ctxt) → Ctxt⁺ Γ
ε⁺[ _ ] = ε

mutual

  -- Appends a context extension to a context extension.

  infixl 5 _⁺++⁺_

  _⁺++⁺_ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Ctxt⁺ (Γ ++⁺ Γ⁺) → Ctxt⁺ Γ
  Γ⁺ ⁺++⁺ ε         = Γ⁺
  Γ⁺ ⁺++⁺ (Γ⁺⁺ ▻ σ) = (Γ⁺ ⁺++⁺ Γ⁺⁺) ▻ P.subst Type (++⁺-++⁺ Γ⁺ Γ⁺⁺) σ

  abstract

    -- _++⁺_/_⁺++⁺_ are associative.

    ++⁺-++⁺ : ∀ {Γ} Γ⁺ Γ⁺⁺ →
              Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ≅-Ctxt Γ ++⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺)
    ++⁺-++⁺ Γ⁺ ε         = P.refl
    ++⁺-++⁺ Γ⁺ (Γ⁺⁺ ▻ σ) =
      ▻-cong (P.sym $ drop-subst-Type id (++⁺-++⁺ Γ⁺ Γ⁺⁺))

mutual

  -- Application of context morphisms to context extensions.

  infixl 8 _/̂⁺_

  _/̂⁺_ : ∀ {Γ Δ} → Ctxt⁺ Γ → Γ ⇨̂ Δ → Ctxt⁺ Δ
  ε        /̂⁺ ρ̂ = ε
  (Γ⁺ ▻ σ) /̂⁺ ρ̂ = Γ⁺ /̂⁺ ρ̂ ▻ σ /̂ ρ̂ ↑̂⁺ Γ⁺

  -- N-ary lifting of context morphisms.

  infixl 10 _↑̂⁺_

  _↑̂⁺_ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ⁺ → Γ ++⁺ Γ⁺ ⇨̂ Δ ++⁺ Γ⁺ /̂⁺ ρ̂
  ρ̂ ↑̂⁺ ε        = ρ̂
  ρ̂ ↑̂⁺ (Γ⁺ ▻ σ) = (ρ̂ ↑̂⁺ Γ⁺) ↑̂

-- N-ary weakening.

ŵk⁺ : ∀ {Γ} Γ⁺ → Γ ⇨̂ Γ ++⁺ Γ⁺
ŵk⁺ ε        = îd
ŵk⁺ (Γ⁺ ▻ σ) = ŵk⁺ Γ⁺ ∘̂ ŵk[ σ ]

------------------------------------------------------------------------
-- Equality

-- Equality of context extensions.

record [Ctxt⁺] : Set (i ⊔ u ⊔ e) where
  constructor [_]
  field
    {Γ} : Ctxt
    Γ⁺  : Ctxt⁺ Γ

infix 4 _≅-Ctxt⁺_

_≅-Ctxt⁺_ : ∀ {Γ₁} (Γ⁺₁ : Ctxt⁺ Γ₁)
              {Γ₂} (Γ⁺₂ : Ctxt⁺ Γ₂) → Set _
Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ = _≡_ {A = [Ctxt⁺]} [ Γ⁺₁ ] [ Γ⁺₂ ]

≅-Ctxt⁺-⇒-≡ : ∀ {Γ} {Γ⁺₁ Γ⁺₂ : Ctxt⁺ Γ} →
              Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → Γ⁺₁ ≡ Γ⁺₂
≅-Ctxt⁺-⇒-≡ P.refl = P.refl

-- Certain uses of substitutivity can be removed.

drop-subst-Ctxt⁺ : ∀ {a} {A : Set a} {x₁ x₂}
                   (f : A → Ctxt) {Γ⁺} (x₁≡x₂ : x₁ ≡ x₂) →
                   P.subst (λ x → Ctxt⁺ (f x)) x₁≡x₂ Γ⁺ ≅-Ctxt⁺ Γ⁺
drop-subst-Ctxt⁺ f P.refl = P.refl

------------------------------------------------------------------------
-- Some congruences

ε⁺-cong : ∀ {Γ₁ Γ₂} → Γ₁ ≅-Ctxt Γ₂ → ε⁺[ Γ₁ ] ≅-Ctxt⁺ ε⁺[ Γ₂ ]
ε⁺-cong P.refl = P.refl

▻⁺-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁} {σ₁}
            {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} {σ₂} →
          Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → σ₁ ≅-Type σ₂ →
          Γ⁺₁ ▻ σ₁ ≅-Ctxt⁺ Γ⁺₂ ▻ σ₂
▻⁺-cong P.refl P.refl = P.refl

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

⁺++⁺-cong : ∀ {Γ₁ Γ⁺₁} {Γ⁺⁺₁ : Ctxt⁺ (Γ₁ ++⁺ Γ⁺₁)}
              {Γ₂ Γ⁺₂} {Γ⁺⁺₂ : Ctxt⁺ (Γ₂ ++⁺ Γ⁺₂)} →
            Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → Γ⁺⁺₁ ≅-Ctxt⁺ Γ⁺⁺₂ →
            Γ⁺₁ ⁺++⁺ Γ⁺⁺₁ ≅-Ctxt⁺ Γ⁺₂ ⁺++⁺ Γ⁺⁺₂
⁺++⁺-cong P.refl P.refl = P.refl

/̂⁺-cong : ∀ {Γ₁ Δ₁} {Γ⁺₁ : Ctxt⁺ Γ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
            {Γ₂ Δ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
          Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → Γ⁺₁ /̂⁺ ρ̂₁ ≅-Ctxt⁺ Γ⁺₂ /̂⁺ ρ̂₂
/̂⁺-cong P.refl P.refl = P.refl

↑̂⁺-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {Γ⁺₁ : Ctxt⁺ Γ₁}
            {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
          ρ̂₁ ≅-⇨̂ ρ̂₂ → Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ̂₁ ↑̂⁺ Γ⁺₁ ≅-⇨̂ ρ̂₂ ↑̂⁺ Γ⁺₂
↑̂⁺-cong P.refl P.refl = P.refl

ŵk⁺-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁} {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
           Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ŵk⁺ Γ⁺₁ ≅-⇨̂ ŵk⁺ Γ⁺₂
ŵk⁺-cong P.refl = P.refl

------------------------------------------------------------------------
-- Some properties

abstract

  -- Γ ++⁺_ has at most one right identity.

  ++⁺-right-identity-unique :
    ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ ≅-Ctxt Γ ++⁺ Γ⁺ → Γ⁺ ≅-Ctxt⁺ ε⁺[ Γ ]
  ++⁺-right-identity-unique         ε        _  = P.refl
  ++⁺-right-identity-unique {ε}     (Γ⁺ ▻ σ) ()
  ++⁺-right-identity-unique {Γ ▻ τ} (Γ⁺ ▻ σ) eq
    with ++⁺-right-identity-unique (ε ▻ τ ⁺++⁺ Γ⁺) (begin
           Γ                      ≡⟨ proj₁ $ ▻-injective eq ⟩
           Γ ▻ τ ++⁺ Γ⁺           ≡⟨ ++⁺-++⁺ (ε ▻ τ) Γ⁺ ⟩
           Γ ++⁺ (ε ▻ τ ⁺++⁺ Γ⁺)  ∎)
  ++⁺-right-identity-unique {Γ ▻ τ} (ε     ▻ σ) eq | ()
  ++⁺-right-identity-unique {Γ ▻ τ} (_ ▻ _ ▻ σ) eq | ()

  -- _++⁺_ is left cancellative.

  cancel-++⁺-left : ∀ {Γ} (Γ⁺₁ Γ⁺₂ : Ctxt⁺ Γ) →
                    Γ ++⁺ Γ⁺₁ ≅-Ctxt Γ ++⁺ Γ⁺₂ → Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂
  cancel-++⁺-left ε          ε          _  = P.refl
  cancel-++⁺-left (Γ⁺₁ ▻ σ₁) (Γ⁺₂ ▻ σ₂) eq with ▻-injective eq
  ... | eq₁ , eq₂ = ▻⁺-cong (cancel-++⁺-left Γ⁺₁ Γ⁺₂ eq₁) eq₂
  cancel-++⁺-left ε (Γ⁺₂ ▻ σ₂) eq
    with ++⁺-right-identity-unique (Γ⁺₂ ▻ σ₂) eq
  ... | ()
  cancel-++⁺-left (Γ⁺₁ ▻ σ₁) ε eq
    with ++⁺-right-identity-unique (Γ⁺₁ ▻ σ₁) (P.sym eq)
  ... | ()

  mutual

    -- The identity substitution has no effect.

    /̂⁺-îd : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ⁺ /̂⁺ îd ≅-Ctxt⁺ Γ⁺
    /̂⁺-îd ε        = P.refl
    /̂⁺-îd (Γ⁺ ▻ σ) = ▻⁺-cong (/̂⁺-îd Γ⁺) (/̂-cong P.refl (îd-↑̂⁺ Γ⁺))

    -- The n-ary lifting of the identity substitution is the identity
    -- substitution.

    îd-↑̂⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → îd ↑̂⁺ Γ⁺ ≅-⇨̂ îd[ Γ ++⁺ Γ⁺ ]
    îd-↑̂⁺ ε        = P.refl
    îd-↑̂⁺ (Γ⁺ ▻ σ) = begin
      [ (îd ↑̂⁺ Γ⁺) ↑̂ ]  ≡⟨ ↑̂-cong (îd-↑̂⁺ Γ⁺) P.refl ⟩
      [ îd ↑̂         ]  ≡⟨ P.refl ⟩
      [ îd           ]  ∎

  -- The identity substitution has no effect even if lifted.

  /̂-îd-↑̂⁺ : ∀ {Γ} Γ⁺ (σ : Type (Γ ++⁺ Γ⁺)) → σ /̂ îd ↑̂⁺ Γ⁺ ≅-Type σ
  /̂-îd-↑̂⁺ Γ⁺ σ = begin
    [ σ /̂ îd ↑̂⁺ Γ⁺ ]  ≡⟨ /̂-cong (P.refl {x = [ σ ]}) (îd-↑̂⁺ Γ⁺) ⟩
    [ σ /̂ îd       ]  ≡⟨ P.refl ⟩
    [ σ            ]  ∎

  mutual

    -- Applying two substitutions is equivalent to applying their
    -- composition.

    /̂⁺-∘̂ : ∀ {Γ Δ Ε} Γ⁺ (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) →
           Γ⁺ /̂⁺ ρ̂₁ ∘̂ ρ̂₂ ≅-Ctxt⁺ Γ⁺ /̂⁺ ρ̂₁ /̂⁺ ρ̂₂
    /̂⁺-∘̂ ε        ρ̂₁ ρ̂₂ = P.refl
    /̂⁺-∘̂ (Γ⁺ ▻ σ) ρ̂₁ ρ̂₂ =
      ▻⁺-cong (/̂⁺-∘̂ Γ⁺ ρ̂₁ ρ̂₂) (/̂-cong (P.refl {x = [ σ ]}) (∘̂-↑̂⁺ ρ̂₁ ρ̂₂ Γ⁺))

    -- _↑̂⁺_ distributes over _∘̂_.

    ∘̂-↑̂⁺ : ∀ {Γ Δ Ε} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) Γ⁺ →
           (ρ̂₁ ∘̂ ρ̂₂) ↑̂⁺ Γ⁺ ≅-⇨̂ ρ̂₁ ↑̂⁺ Γ⁺ ∘̂ ρ̂₂ ↑̂⁺ (Γ⁺ /̂⁺ ρ̂₁)
    ∘̂-↑̂⁺ ρ̂₁ ρ̂₂ ε        = P.refl
    ∘̂-↑̂⁺ ρ̂₁ ρ̂₂ (Γ⁺ ▻ σ) = begin
      [ ((ρ̂₁ ∘̂ ρ̂₂) ↑̂⁺ Γ⁺) ↑̂                   ]  ≡⟨ ↑̂-cong (∘̂-↑̂⁺ ρ̂₁ ρ̂₂ Γ⁺) P.refl ⟩
      [ (ρ̂₁ ↑̂⁺ Γ⁺ ∘̂ ρ̂₂ ↑̂⁺ (Γ⁺ /̂⁺ ρ̂₁)) ↑̂       ]  ≡⟨ P.refl ⟩
      [ (ρ̂₁ ↑̂⁺ Γ⁺) ↑̂ σ ∘̂ (ρ̂₂ ↑̂⁺ (Γ⁺ /̂⁺ ρ̂₁)) ↑̂ ]  ∎

  -- A corollary.

  /̂-↑̂⁺-/̂-ŵk-↑̂⁺ : ∀ {Γ Δ} σ (ρ̂ : Γ ⇨̂ Δ) (Γ⁺ : Ctxt⁺ Γ) τ →
                 τ /̂ ρ̂ ↑̂⁺ Γ⁺ /̂ ŵk[ σ /̂ ρ̂ ] ↑̂⁺ (Γ⁺ /̂⁺ ρ̂) ≅-Type
                 τ /̂ ŵk[ σ ] ↑̂⁺ Γ⁺ /̂ ρ̂ ↑̂ ↑̂⁺ (Γ⁺ /̂⁺ ŵk)
  /̂-↑̂⁺-/̂-ŵk-↑̂⁺ σ ρ̂ Γ⁺ τ = /̂-cong (P.refl {x = [ τ ]}) (begin
    [ ρ̂ ↑̂⁺ Γ⁺ ∘̂ ŵk ↑̂⁺ (Γ⁺ /̂⁺ ρ̂)         ]  ≡⟨ P.sym $ ∘̂-↑̂⁺ ρ̂ ŵk Γ⁺ ⟩
    [ (ρ̂ ∘̂ ŵk) ↑̂⁺ Γ⁺                    ]  ≡⟨ P.refl ⟩
    [ (ŵk[ σ ] ∘̂ ρ̂ ↑̂) ↑̂⁺ Γ⁺             ]  ≡⟨ ∘̂-↑̂⁺ ŵk[ σ ] (ρ̂ ↑̂) Γ⁺ ⟩
    [ ŵk[ σ ] ↑̂⁺ Γ⁺ ∘̂ ρ̂ ↑̂ ↑̂⁺ (Γ⁺ /̂⁺ ŵk) ]  ∎)

  -- ŵk⁺ commutes (modulo lifting) with arbitrary context morphisms.

  ∘̂-ŵk⁺ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ⁺ →
          ρ̂ ∘̂ ŵk⁺ (Γ⁺ /̂⁺ ρ̂) ≅-⇨̂ ŵk⁺ Γ⁺ ∘̂ ρ̂ ↑̂⁺ Γ⁺
  ∘̂-ŵk⁺ ρ̂ ε        = P.refl
  ∘̂-ŵk⁺ ρ̂ (Γ⁺ ▻ σ) = begin
    [ ρ̂ ∘̂ ŵk⁺ (Γ⁺ /̂⁺ ρ̂) ∘̂ ŵk         ]  ≡⟨ ∘̂-cong (∘̂-ŵk⁺ ρ̂ Γ⁺) P.refl ⟩
    [ ŵk⁺ Γ⁺ ∘̂ ρ̂ ↑̂⁺ Γ⁺ ∘̂ ŵk          ]  ≡⟨ P.refl ⟩
    [ ŵk⁺ Γ⁺ ∘̂ ŵk[ σ ] ∘̂ (ρ̂ ↑̂⁺ Γ⁺) ↑̂ ]  ∎

  -- ŵk⁺ is homomorphic with respect to _⁺++⁺_/_∘̂_.

  ŵk⁺-⁺++⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) (Γ⁺⁺ : Ctxt⁺ (Γ ++⁺ Γ⁺)) →
             ŵk⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) ≅-⇨̂ ŵk⁺ Γ⁺ ∘̂ ŵk⁺ Γ⁺⁺
  ŵk⁺-⁺++⁺ Γ⁺ ε         = P.refl
  ŵk⁺-⁺++⁺ Γ⁺ (Γ⁺⁺ ▻ σ) =
    ∘̂-cong (ŵk⁺-⁺++⁺ Γ⁺ Γ⁺⁺)
           (ŵk-cong (drop-subst-Type id (++⁺-++⁺ Γ⁺ Γ⁺⁺)))

  -- Two n-ary liftings can be merged into one.

  ↑̂⁺-⁺++⁺ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ⁺ Γ⁺⁺ →
            ρ̂ ↑̂⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) ≅-⇨̂ ρ̂ ↑̂⁺ Γ⁺ ↑̂⁺ Γ⁺⁺
  ↑̂⁺-⁺++⁺ ρ̂ Γ⁺ ε         = P.refl
  ↑̂⁺-⁺++⁺ ρ̂ Γ⁺ (Γ⁺⁺ ▻ σ) = begin
    [ (ρ̂ ↑̂⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺)) ↑̂ ]  ≡⟨ ↑̂-cong (↑̂⁺-⁺++⁺ ρ̂ Γ⁺ Γ⁺⁺) (drop-subst-Type id (++⁺-++⁺ Γ⁺ Γ⁺⁺)) ⟩
    [ (ρ̂ ↑̂⁺ Γ⁺ ↑̂⁺ Γ⁺⁺) ↑̂     ]  ∎

  -- _/̂⁺_ distributes over _⁺++⁺_ (sort of).

  ++⁺-⁺++⁺-/̂⁺ :
    ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ⁺ Γ⁺⁺ →
    Δ ++⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) /̂⁺ ρ̂ ≅-Ctxt Δ ++⁺ Γ⁺ /̂⁺ ρ̂ ++⁺ Γ⁺⁺ /̂⁺ ρ̂ ↑̂⁺ Γ⁺
  ++⁺-⁺++⁺-/̂⁺         ρ̂ Γ⁺ ε         = P.refl
  ++⁺-⁺++⁺-/̂⁺ {Δ = Δ} ρ̂ Γ⁺ (Γ⁺⁺ ▻ σ) = begin
    Δ ++⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) /̂⁺ ρ̂ ▻
      P.subst Type (++⁺-++⁺ Γ⁺ Γ⁺⁺) σ /̂ ρ̂ ↑̂⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺)  ≡⟨ ▻-cong (/̂-cong (drop-subst-Type id (++⁺-++⁺ Γ⁺ Γ⁺⁺))
                                                                              (↑̂⁺-⁺++⁺ ρ̂ Γ⁺ Γ⁺⁺)) ⟩
    Δ ++⁺ Γ⁺ /̂⁺ ρ̂ ++⁺ Γ⁺⁺ /̂⁺ ρ̂ ↑̂⁺ Γ⁺ ▻ σ /̂ ρ̂ ↑̂⁺ Γ⁺ ↑̂⁺ Γ⁺⁺   ∎