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

open import Universe

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

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

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

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

-- Context extensions.

infixr 5 _◅_

data Ctxt₊ (Γ : Ctxt) : Set (i  u  e) where
  ε   : Ctxt₊ Γ
  _◅_ : (σ : Type Γ) (Γ₊ : Ctxt₊ (Γ  σ))  Ctxt₊ Γ

-- A synonym.

ε₊[_] : (Γ : Ctxt)  Ctxt₊ Γ
ε₊[ _ ] = ε

-- Appends a context extension to a context.

infixl 5 _++₊_

_++₊_ : (Γ : Ctxt)  Ctxt₊ Γ  Ctxt
Γ ++₊ ε        = Γ
Γ ++₊ (σ  Γ₊) = Γ  σ ++₊ Γ₊

-- The following operations append a context extension to a context
-- extension.

infixl 5 _₊++₊_ _⁺++₊_

_₊++₊_ :  {Γ} Γ₊  Ctxt₊ (Γ ++₊ Γ₊)  Ctxt₊ Γ
ε        ₊++₊ Γ₊₊ = Γ₊₊
(σ  Γ₊) ₊++₊ Γ₊₊ = σ  (Γ₊ ₊++₊ Γ₊₊)

_⁺++₊_ :  {Γ} Γ⁺  Ctxt₊ (Γ ++⁺ Γ⁺)  Ctxt₊ Γ
ε      ⁺++₊ Γ₊ = Γ₊
Γ⁺  σ ⁺++₊ Γ₊ = Γ⁺ ⁺++₊ (σ  Γ₊)

-- 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₊ Γ₊₂  σ₁  Γ₊₁ ≅-Ctxt₊ σ₂  Γ₊₂
◅-cong 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₊ Γ₊₂ 
            Γ⁺₁ ⁺++₊ Γ₊₁ ≅-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.

  private

    ++₊-right-identity-unique′ :
       {Γ} Γ⁺ Γ₊  Γ ≅-Ctxt Γ ++⁺ Γ⁺ ++₊ Γ₊  Γ₊ ≅-Ctxt₊ ε₊[ Γ ++⁺ Γ⁺ ]
    ++₊-right-identity-unique′ Γ⁺ ε        _  = P.refl
    ++₊-right-identity-unique′ Γ⁺ (σ  Γ₊) eq
      with ++₊-right-identity-unique′ (Γ⁺  σ) Γ₊ eq
    ++₊-right-identity-unique′ Γ⁺ (σ  .ε) eq | P.refl
      with ++⁺-right-identity-unique (Γ⁺  σ) eq
    ... | ()

  ++₊-right-identity-unique :
     {Γ} Γ₊  Γ ≅-Ctxt Γ ++₊ Γ₊  Γ₊ ≅-Ctxt₊ ε₊[ Γ ]
  ++₊-right-identity-unique Γ₊ = ++₊-right-identity-unique′ ε Γ₊

  -- Γ ++₊_ is left cancellative.

  private

    cancel-++₊-left′ :  {Γ} Γ⁺₁ Γ₊₁ Γ⁺₂ Γ₊₂ 
                       Γ ++⁺ Γ⁺₁ ++₊ Γ₊₁ ≅-Ctxt Γ ++⁺ Γ⁺₂ ++₊ Γ₊₂ 
                       Γ⁺₁ ⁺++₊ Γ₊₁ ≅-Ctxt₊ Γ⁺₂ ⁺++₊ Γ₊₂
    cancel-++₊-left′ Γ⁺₁ ε          Γ⁺₂ ε          eq = ⁺++₊-cong (cancel-++⁺-left Γ⁺₁ Γ⁺₂ eq) (ε₊-cong eq)
    cancel-++₊-left′ Γ⁺₁ (σ₁  Γ₊₁) Γ⁺₂ (σ₂  Γ₊₂) eq = cancel-++₊-left′ (Γ⁺₁  σ₁) Γ₊₁ (Γ⁺₂  σ₂) Γ₊₂ eq
    cancel-++₊-left′ Γ⁺₁ ε          Γ⁺₂ (σ₂  Γ₊₂) eq = cancel-++₊-left′  Γ⁺₁       ε   (Γ⁺₂  σ₂) Γ₊₂ eq
    cancel-++₊-left′ Γ⁺₁ (σ₁  Γ₊₁) Γ⁺₂ ε          eq = cancel-++₊-left′ (Γ⁺₁  σ₁) Γ₊₁  Γ⁺₂       ε   eq

  cancel-++₊-left :  {Γ} (Γ₊₁ Γ₊₂ : Ctxt₊ Γ) 
                    Γ ++₊ Γ₊₁ ≅-Ctxt Γ ++₊ Γ₊₂  Γ₊₁ ≅-Ctxt₊ Γ₊₂
  cancel-++₊-left Γ₊₁ Γ₊₂ = cancel-++₊-left′ ε Γ₊₁ ε Γ₊₂

  -- _++₊_/_₊++₊_ are associative.

  ++₊-++₊ :  {Γ} Γ₊ Γ₊₊  Γ ++₊ Γ₊ ++₊ Γ₊₊ ≅-Ctxt Γ ++₊ (Γ₊ ₊++₊ Γ₊₊)
  ++₊-++₊ ε        Γ₊₊ = P.refl
  ++₊-++₊ (σ  Γ₊) Γ₊₊ = ++₊-++₊ Γ₊ Γ₊₊

  -- The identity substitution has no effect.

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

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

  îd-↑̂₊ :  {Γ} (Γ₊ : Ctxt₊ Γ)  îd ↑̂₊ Γ₊ ≅-⇨̂ îd[ Γ ++₊ Γ₊ ]
  îd-↑̂₊ ε        = P.refl
  îd-↑̂₊ (σ  Γ₊) = begin
    [ îd ↑̂ ↑̂₊ Γ₊ ]  ≡⟨ P.refl 
    [ îd ↑̂₊ Γ₊   ]  ≡⟨ îd-↑̂₊ Γ₊ 
    [ î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 
    [ σ            ]  

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

  /̂₊-∘̂ :  {Γ Δ Ε} Γ₊ (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) 
         Γ₊ /̂₊ ρ̂₁ ∘̂ ρ̂₂ ≅-Ctxt₊ Γ₊ /̂₊ ρ̂₁ /̂₊ ρ̂₂
  /̂₊-∘̂ ε        ρ̂₁ ρ̂₂ = P.refl
  /̂₊-∘̂ (σ  Γ₊) ρ̂₁ ρ̂₂ = ◅-cong (/̂₊-∘̂ Γ₊ (ρ̂₁ ↑̂) (ρ̂₂ ↑̂))

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

  ∘̂-↑̂₊ :  {Γ Δ Ε} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) Γ₊ 
         (ρ̂₁ ∘̂ ρ̂₂) ↑̂₊ Γ₊ ≅-⇨̂ ρ̂₁ ↑̂₊ Γ₊ ∘̂ ρ̂₂ ↑̂₊ (Γ₊ /̂₊ ρ̂₁)
  ∘̂-↑̂₊ ρ̂₁ ρ̂₂ ε        = P.refl
  ∘̂-↑̂₊ ρ̂₁ ρ̂₂ (σ  Γ₊) = begin
    [ (ρ̂₁ ∘̂ ρ̂₂) ↑̂ ↑̂₊ Γ₊                     ]  ≡⟨ 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₊ (Γ₊ /̂₊ ρ̂ ↑̂)         ]  ≡⟨ P.refl 
    [ ŵk[ σ ] ∘̂ ρ̂ ↑̂ ∘̂ ŵk₊ (Γ₊ /̂₊ ρ̂ ↑̂)  ]  ≡⟨ ∘̂-cong (P.refl {x = [ ŵk ]}) (∘̂-ŵk₊ (ρ̂ ↑̂) Γ₊) 
    [ ŵk ∘̂ ŵk₊ Γ₊ ∘̂ ρ̂ ↑̂ ↑̂₊ Γ₊          ]  

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

  ŵk₊-₊++₊ :  {Γ} (Γ₊ : Ctxt₊ Γ) (Γ₊₊ : Ctxt₊ (Γ ++₊ Γ₊)) 
             ŵk₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨̂ ŵk₊ Γ₊ ∘̂ ŵk₊ Γ₊₊
  ŵk₊-₊++₊ ε        Γ₊₊ = P.refl
  ŵk₊-₊++₊ (σ  Γ₊) Γ₊₊ = ∘̂-cong (P.refl {x = [ ŵk ]}) (ŵk₊-₊++₊ Γ₊ Γ₊₊)

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

  ↑̂₊-₊++₊ :  {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ₊ Γ₊₊ 
            ρ̂ ↑̂₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨̂ ρ̂ ↑̂₊ Γ₊ ↑̂₊ Γ₊₊
  ↑̂₊-₊++₊ ρ̂ ε        Γ₊₊ = P.refl
  ↑̂₊-₊++₊ ρ̂ (σ  Γ₊) Γ₊₊ = ↑̂₊-₊++₊ (ρ̂ ↑̂) Γ₊ Γ₊₊

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

  ++₊-₊++₊-/̂₊ :
     {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ₊ Γ₊₊ 
    Δ ++₊ (Γ₊ ₊++₊ Γ₊₊) /̂₊ ρ̂ ≅-Ctxt Δ ++₊ Γ₊ /̂₊ ρ̂ ++₊ Γ₊₊ /̂₊ ρ̂ ↑̂₊ Γ₊
  ++₊-₊++₊-/̂₊         ρ̂ ε        Γ₊₊ = P.refl
  ++₊-₊++₊-/̂₊ {Δ = Δ} ρ̂ (σ  Γ₊) Γ₊₊ = ++₊-₊++₊-/̂₊ (ρ̂ ↑̂) Γ₊ Γ₊₊