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

open import Universe

module deBruijn.Context.Extension.Right
  {i u e} (Uni : Indexed-universe 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.

ŵk⁺ :  {Γ} Γ⁺  Γ ⇨̂ Γ ++⁺ Γ⁺
ŵk⁺ ε        = îd
ŵk⁺ (Γ⁺  σ) = ŵk⁺ Γ⁺ ∘̂ ŵ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⁺ Γ⁺₂ = [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

ŵk⁺-cong :  {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁} {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} 
           Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂  ŵk⁺ Γ⁺₁ ≅-⇨̂ ŵk⁺ Γ⁺₂
ŵ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.

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

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

    îd-↑̂⁺ :  {Γ} (Γ⁺ : Ctxt⁺ Γ)  îd ↑̂⁺ Γ⁺ ≅-⇨̂ îd[ Γ ++⁺ Γ⁺ ]
    îd-↑̂⁺ ε        = P.refl
    îd-↑̂⁺ (Γ⁺  σ) = begin
      [ (îd ↑̂⁺ Γ⁺) ↑̂ ]  ≡⟨ ↑̂-cong (îd-↑̂⁺ Γ⁺) P.refl 
      [ îd ↑̂         ]  ≡⟨ P.refl 
      [ îd           ]  

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

  /̂-îd-↑̂⁺ :  {Γ} Γ⁺ (σ : Type (Γ ++⁺ Γ⁺))  σ  îd ↑̂⁺ Γ⁺ ≅-Type σ
  /̂-îd-↑̂⁺ Γ⁺ σ = begin
    [ σ  îd ↑̂⁺ Γ⁺ ]  ≡⟨ /̂-cong (P.refl {x = [ σ ]}) (îd-↑̂⁺ Γ⁺) 
    [ σ  î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.

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

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

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

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

  ŵk⁺-⁺++⁺ :  {Γ} (Γ⁺ : Ctxt⁺ Γ) (Γ⁺⁺ : Ctxt⁺ (Γ ++⁺ Γ⁺)) 
             ŵk⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) ≅-⇨̂ ŵk⁺ Γ⁺ ∘̂ ŵk⁺ Γ⁺⁺
  ŵk⁺-⁺++⁺ Γ⁺ ε         = P.refl
  ŵk⁺-⁺++⁺ Γ⁺ (Γ⁺⁺  σ) =
    ∘̂-cong (ŵk⁺-⁺++⁺ Γ⁺ Γ⁺⁺)
           (ŵ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 (++⁺-++⁺ Γ⁺ Γ⁺⁺))
                                                                              (↑̂⁺-⁺++⁺ ρ̂ Γ⁺ Γ⁺⁺)) 
    Δ ++⁺ Γ⁺ /̂⁺ ρ̂ ++⁺ Γ⁺⁺ /̂⁺ ρ̂ ↑̂⁺ Γ⁺  σ  ρ̂ ↑̂⁺ Γ⁺ ↑̂⁺ Γ⁺⁺