deBruijn.Context.Extension.Left

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

open import Data.Universe.Indexed

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

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₊ Γ₊₂ → σ₁ ◅ Γ₊₁ ≅-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

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.

  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.

  /̂₊-îd : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ₊ /̂₊ îd ≅-Ctxt₊ Γ₊
  /̂₊-îd ε        = P.refl
  /̂₊-îd (σ ◅ Γ₊) = ◅-cong (/̂₊-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 ↑̂ ↑̂₊ Γ₊ ]  ≡⟨ P.refl ⟩
    [ îd ↑̂₊ Γ₊   ]  ≡⟨ îd-↑̂₊ Γ₊ ⟩
    [ 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 ⟩
    [ σ            ]  ∎

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

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

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

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

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

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

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

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