deBruijn.Context.Term-like

------------------------------------------------------------------------
-- An abstraction: term-like things
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Context.Term-like
  {i u e} (Uni : IndexedUniverse i u e) where

import Axiom.Extensionality.Propositional as E
open import Data.Product
import deBruijn.Context.Basics          as Basics
import deBruijn.Context.Extension.Right as Right
open import Function.Base hiding (_∋_)
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

------------------------------------------------------------------------
-- Term-like things

record Term-like ℓ : Set (i ⊔ u ⊔ e ⊔ Level.suc ℓ) where
  infix 3 _⊢_
  field
    _⊢_ : (Γ : Ctxt) → Type Γ → Set ℓ
    ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → Value Γ σ

  -- Equality of term-like things.

  record [⊢] : Set (i ⊔ u ⊔ e ⊔ ℓ) where
    constructor [_]
    field
      {Γ} : Ctxt
      {σ} : Type Γ
      t   : Γ ⊢ σ

  infix 4 _≅-⊢_

  _≅-⊢_ : ∀ {Γ₁ σ₁} (t₁ : Γ₁ ⊢ σ₁)
            {Γ₂ σ₂} (t₂ : Γ₂ ⊢ σ₂) → Set _
  t₁ ≅-⊢ t₂ = _≡_ {A = [⊢]} [ t₁ ] [ t₂ ]

  ≅-⊢-⇒-≡ : ∀ {Γ σ} {t₁ t₂ : Γ ⊢ σ} →
            t₁ ≅-⊢ t₂ → t₁ ≡ t₂
  ≅-⊢-⇒-≡ P.refl = P.refl

  -- Certain uses of substitutivity can be removed.

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

  -- A congruence lemma.

  ⟦⟧-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁}
              {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
            t₁ ≅-⊢ t₂ → ⟦ t₁ ⟧ ≅-Value ⟦ t₂ ⟧
  ⟦⟧-cong P.refl = P.refl

-- Values are term-like.

Val : Term-like _
Val = record { _⊢_ = Value; ⟦_⟧ = id }

-- Variables are term-like.

Var : Term-like _
Var = record { _⊢_ = _∋_; ⟦_⟧ = lookup }

------------------------------------------------------------------------
-- Families of functions which, on the semantic side, correspond to
-- the application of a given context morphism

record [_⟶_] {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂)
             {Γ Δ : Ctxt} (ρ̂ : Γ ⇨̂ Δ) : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
  constructor _,_

  open Term-like T₁ renaming (_⊢_ to _⊢₁_; ⟦_⟧ to ⟦_⟧₁)
  open Term-like T₂ renaming (_⊢_ to _⊢₂_; ⟦_⟧ to ⟦_⟧₂)

  field
    function    : ∀ σ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂
    corresponds :
      ∀ σ (t : Γ ⊢₁ σ) → ⟦ t ⟧₁ /̂Val ρ̂ ≅-Value ⟦ function σ t ⟧₂

-- Functions which do not change the context or type.

[_⟶⁼_] : ∀ {t₁ t₂} → Term-like t₁ → Term-like t₂ → Set _
[ T₁ ⟶⁼ T₂ ] = ∀ {Γ} → [ T₁ ⟶ T₂ ] îd[ Γ ]

-- Projections. (The fields above have explicit σ's to avoid some
-- problems; the projections below have implicit σ's.)

infixl 9 _·_

_·_ : ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
      let open Term-like T₁ renaming (_⊢_ to _⊢₁_)
          open Term-like T₂ renaming (_⊢_ to _⊢₂_) in
      ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
      [ T₁ ⟶ T₂ ] ρ̂ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂
_·_ f = [_⟶_].function f _

corresponds :
  ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
  let open Term-like T₁ renaming (_⊢_ to _⊢₁_; ⟦_⟧ to ⟦_⟧₁)
      open Term-like T₂ renaming (⟦_⟧ to ⟦_⟧₂) in
  ∀ {Γ Δ : Ctxt} {ρ̂ : Γ ⇨̂ Δ} {σ}
  (f : [ T₁ ⟶ T₂ ] ρ̂) (t : Γ ⊢₁ σ) →
  ⟦ t ⟧₁ /̂Val ρ̂ ≅-Value ⟦ f · t ⟧₂
corresponds f = [_⟶_].corresponds f _

-- Weakening of variables (the successor function).

weaken∋ : ∀ {Γ} {σ : Type Γ} → [ Var ⟶ Var ] ŵk[ σ ]
weaken∋ = record
  { function    = λ _ → suc
  ; corresponds = λ _ _ → P.refl
  }

weaken∋[_] : ∀ {Γ} (σ : Type Γ) → [ Var ⟶ Var ] ŵk[ σ ]
weaken∋[ _ ] = weaken∋

-- Lifts a function on variables, f, to a function which leaves a
-- prefix of the context unchanged and otherwise behaves as f.

lift : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} →
       [ Var ⟶ Var ] ρ̂ → ∀ Γ⁺ → [ Var ⟶ Var ] (ρ̂ ↑̂⁺ Γ⁺)
lift             f ε        = f
lift {Γ} {Δ} {ρ̂} f (Γ⁺ ▻ σ) = record
  { function    = function
  ; corresponds = corr
  }
  where
  function : ∀ τ → Γ ++⁺ Γ⁺ ▻ σ ∋ τ →
             Δ ++⁺ (Γ⁺ ▻ σ) /̂⁺ ρ̂ ∋ τ /̂ ρ̂ ↑̂⁺ (Γ⁺ ▻ σ)
  function ._ zero    = zero
  function ._ (suc x) = suc (lift f Γ⁺ · x)

  abstract
    corr : ∀ τ (x : Γ ++⁺ Γ⁺ ▻ σ ∋ τ) →
           lookup x /̂Val ρ̂ ↑̂⁺ (Γ⁺ ▻ σ) ≅-Value lookup (function _ x)
    corr ._ zero    = P.refl
    corr ._ (suc x) = begin
      [ lookup x /̂Val ρ̂ ↑̂⁺ Γ⁺ /̂Val ŵk  ]  ≡⟨ /̂Val-cong (corresponds (lift f Γ⁺) x) P.refl ⟩
      [ lookup (lift f Γ⁺ · x) /̂Val ŵk ]  ≡⟨ P.refl ⟩
      [ lookup (suc (lift f Γ⁺ · x))   ]  ∎

------------------------------------------------------------------------
-- Equality for the functions introduced above

-- Note that the definition of equality does not take the
-- "corresponds" proof into account.

record [⟶] {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂)
           : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
  constructor [_]
  open Term-like T₁ renaming (_⊢_ to _⊢₁_)
  open Term-like T₂ renaming (_⊢_ to _⊢₂_)
  field
    {Γ Δ} : Ctxt
    {ρ̂}   : Γ ⇨̂ Δ
    f     : ∀ σ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂

[_]⟶ : ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂}
         {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} →
       [ T₁ ⟶ T₂ ] ρ̂ → [⟶] T₁ T₂
[ f ]⟶ = [ [_⟶_].function f ]

-- Equality is defined as a record type to make it possible to infer
-- ρ₁ and ρ₂ from a value of type ρ₁ ≅-⟶ ρ₂.

infix 4 _≅-⟶_

record _≅-⟶_
  {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂}
  {Γ₁ Δ₁ : Ctxt} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} (f₁ : [ T₁ ⟶ T₂ ] ρ̂₁)
  {Γ₂ Δ₂ : Ctxt} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} (f₂ : [ T₁ ⟶ T₂ ] ρ̂₂)
  : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
  constructor [_]
  field
    [f₁]⟶≡[f₂]⟶ : [ f₁ ]⟶ ≡ [ f₂ ]⟶

-- Some equational reasoning combinators.

module ≅-⟶-Reasoning
  {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂}
  where

  infix  3 _∎-⟶
  infixr 2 _≅-⟶⟨_⟩_

  _≅-⟶⟨_⟩_ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂}
               {Γ₃ Δ₃} {ρ̂₃ : Γ₃ ⇨̂ Δ₃}
             (f₁ : [ T₁ ⟶ T₂ ] ρ̂₁) {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂}
                                   {f₃ : [ T₁ ⟶ T₂ ] ρ̂₃} →
             f₁ ≅-⟶ f₂ → f₂ ≅-⟶ f₃ → f₁ ≅-⟶ f₃
  _ ≅-⟶⟨ [ f₁≅f₂ ] ⟩ [ f₂≅f₃ ] = [ P.trans f₁≅f₂ f₂≅f₃ ]

  _∎-⟶ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (f : [ T₁ ⟶ T₂ ] ρ̂) → f ≅-⟶ f
  _ ∎-⟶ = [ P.refl ]

  sym-⟶ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁}
            {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} →
          f₁ ≅-⟶ f₂ → f₂ ≅-⟶ f₁
  sym-⟶ [ f₁≅f₂ ] = [ P.sym f₁≅f₂ ]

open ≅-⟶-Reasoning public

-- A setoid for [_⟶_].

[_⟶_]-setoid : ∀ {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂) →
             ∀ {Γ Δ} → Γ ⇨̂ Δ → Setoid _ _
[ T₁ ⟶ T₂ ]-setoid ρ̂ = record
  { Carrier       = [ T₁ ⟶ T₂ ] ρ̂
  ; _≈_           = λ f₁ f₂ → f₁ ≅-⟶ f₂
  ; isEquivalence = record
    { refl  = _ ∎-⟶
    ; sym   = sym-⟶
    ; trans = λ p q → _ ≅-⟶⟨ p ⟩ q
    }
  }

-- A congruence lemma.

·-cong :
  ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
  let open Term-like T₁ renaming (_⊢_ to _⊢₁_; _≅-⊢_ to _≅-⊢₁_)
      open Term-like T₂ renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_) in
  ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁} {t₁ : Γ₁ ⊢₁ σ₁}
    {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} {t₂ : Γ₂ ⊢₁ σ₂} →
  f₁ ≅-⟶ f₂ → t₁ ≅-⊢₁ t₂ → f₁ · t₁ ≅-⊢₂ f₂ · t₂
·-cong {f₁ = _ , _} {f₂ = ._ , _} [ P.refl ] P.refl = P.refl

abstract

  -- Two variants of extensional equality (assuming ordinary
  -- extensional equality).

  extensional-equality₁ :
    ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
    let open Term-like T₁ renaming (_⊢_ to _⊢₁_)
        open Term-like T₂ renaming (_≅-⊢_ to _≅-⊢₂_)
    in
    E.Extensionality (i ⊔ u ⊔ e ⊔ t₁) (t₁ ⊔ t₂) →
    ∀ {Γ Δ₁} {ρ̂₁ : Γ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁}
        {Δ₂} {ρ̂₂ : Γ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} →
    ρ̂₁ ≅-⇨̂ ρ̂₂ → (∀ {σ} (t : Γ ⊢₁ σ) → f₁ · t ≅-⊢₂ f₂ · t) →
    f₁ ≅-⟶ f₂
  extensional-equality₁ {t₁} {t₂} {T₂ = T₂} ext P.refl f₁≅f₂ =
    [ P.cong [_] (ext₁ λ σ → ext₂ λ t → ≅-⊢₂-⇒-≡ (f₁≅f₂ t)) ]
    where
    open Term-like T₂ using () renaming (≅-⊢-⇒-≡ to ≅-⊢₂-⇒-≡)

    ext₁ : E.Extensionality (i ⊔ u ⊔ e) (t₁ ⊔ t₂)
    ext₁ = E.lower-extensionality t₁ Level.zero ext

    ext₂ : E.Extensionality t₁ t₂
    ext₂ = E.lower-extensionality (i ⊔ u ⊔ e) t₁ ext

  extensional-equality₂ :
    ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
    let open Term-like T₁ renaming (_≅-⊢_ to _≅-⊢₁_; _⊢_ to _⊢₁_)
        open Term-like T₂ renaming (_≅-⊢_ to _≅-⊢₂_)
    in
    E.Extensionality (i ⊔ u ⊔ e ⊔ t₁) (t₁ ⊔ t₂) →
    ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁}
      {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} →
    ρ̂₁ ≅-⇨̂ ρ̂₂ →
    (∀ {σ₁} {t₁ : Γ₁ ⊢₁ σ₁} {σ₂} {t₂ : Γ₂ ⊢₁ σ₂} →
       t₁ ≅-⊢₁ t₂ → f₁ · t₁ ≅-⊢₂ f₂ · t₂) →
    f₁ ≅-⟶ f₂
  extensional-equality₂ {T₁ = T₁} ext P.refl f₁≅f₂ =
    extensional-equality₁ ext P.refl (λ t → f₁≅f₂ (P.refl {x = [ t ]}))
    where open Term-like T₁ using ([_])

  -- lift ∘ weaken∋ sort of commutes with a lifted version of itself.

  lift-weaken∋-lift-lift-weaken∋ :
    ∀ {Γ} σ Γ⁺ τ Γ⁺⁺ {υ} (x : Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ∋ υ) →
    lift weaken∋[ τ /̂ ŵk ↑̂⁺ Γ⁺ ] (Γ⁺⁺ /̂⁺ ŵk ↑̂⁺ Γ⁺) ·
         (lift (lift weaken∋[ σ ] Γ⁺) Γ⁺⁺ · x) ≅-∋
    lift (lift weaken∋[ σ ] (Γ⁺ ▻ τ)) (Γ⁺⁺ /̂⁺ ŵk) ·
         (lift weaken∋[ τ ] Γ⁺⁺ · x)
  lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ ε         x       = P.refl
  lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ (Γ⁺⁺ ▻ υ) zero    =
    zero-cong (/̂-↑̂⁺-/̂-ŵk-↑̂⁺ τ (ŵk ↑̂⁺ Γ⁺) Γ⁺⁺ υ)
  lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ (Γ⁺⁺ ▻ υ) (suc x) =
    suc-cong (/̂-↑̂⁺-/̂-ŵk-↑̂⁺ τ (ŵk ↑̂⁺ Γ⁺) Γ⁺⁺ υ)
             (lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ Γ⁺⁺ x)

------------------------------------------------------------------------
-- Term-like t and [_⟶_] form a category

-- At least if we ignore the context morphism index.

-- Identity.

[id] : ∀ {t} {T : Term-like t} {Γ} → [ T ⟶ T ] îd[ Γ ]
[id] = record { function = λ _ → id; corresponds = λ _ _ → P.refl }

-- Composition.

infixl 9 _[∘]_

_[∘]_ : ∀ {t₁ t₂ t₃}
          {T₁ : Term-like t₁} {T₂ : Term-like t₂} {T₃ : Term-like t₃}
          {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
        [ T₂ ⟶ T₃ ] ρ̂₂ → [ T₁ ⟶ T₂ ] ρ̂₁ → [ T₁ ⟶ T₃ ] (ρ̂₁ ∘̂ ρ̂₂)
_[∘]_ {T₁ = T₁} {T₂} {T₃} {ρ̂₁ = ρ̂₁} {ρ̂₂} f g = record
  { function    = λ _ → _·_ f ∘ _·_ g
  ; corresponds = corr
  }
  where
  open P.≡-Reasoning
  open Term-like T₁ renaming (⟦_⟧ to ⟦_⟧₁; _⊢_ to _⊢₁_)
  open Term-like T₂ renaming (⟦_⟧ to ⟦_⟧₂)
  open Term-like T₃ renaming (⟦_⟧ to ⟦_⟧₃)

  abstract
    corr : ∀ σ (t : _ ⊢₁ σ) →
           ⟦ t ⟧₁ /̂Val ρ̂₁ ∘̂ ρ̂₂ ≅-Value ⟦ f · (g · t) ⟧₃
    corr = λ σ t → begin
      [ ⟦ t ⟧₁ /̂Val ρ̂₁ ∘̂ ρ̂₂ ]  ≡⟨ /̂Val-cong (corresponds g t) P.refl ⟩
      [ ⟦ g · t ⟧₂ /̂Val ρ̂₂  ]  ≡⟨ corresponds f (g · t) ⟩
      [ ⟦ f · (g · t) ⟧₃    ]  ∎

-- [id] and _[∘]_ preserve equality.

[id]-cong :
  ∀ {t} {T : Term-like t} {Γ₁ Γ₂} →
  Γ₁ ≅-Ctxt Γ₂ → [id] {T = T} {Γ = Γ₁} ≅-⟶ [id] {T = T} {Γ = Γ₂}
[id]-cong P.refl = [ P.refl ]

private
 module Dummy {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} where

  [∘]-cong : ∀ {t₃} {T₃ : Term-like t₃}
               {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
               {f₁₁ : [ T₁ ⟶ T₂ ] ρ̂₁₁} {f₂₁ : [ T₂ ⟶ T₃ ] ρ̂₂₁}
               {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
               {f₁₂ : [ T₁ ⟶ T₂ ] ρ̂₁₂} {f₂₂ : [ T₂ ⟶ T₃ ] ρ̂₂₂} →
             f₁₁ ≅-⟶ f₁₂ → f₂₁ ≅-⟶ f₂₂ → f₂₁ [∘] f₁₁ ≅-⟶ f₂₂ [∘] f₁₂
  [∘]-cong {f₁₁ = _ , _} {f₂₁ = _ , _} {f₁₂ = ._ , _} {f₂₂ = ._ , _}
           [ P.refl ] [ P.refl ] = [ P.refl ]

  -- [id] is a left and right identity of _[∘]_, which is associative.

  [id]-[∘] : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
             (f : [ T₁ ⟶ T₂ ] ρ̂) → [id] [∘] f ≅-⟶ f
  [id]-[∘] f = [ P.refl ]

  [∘]-[id] : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
             (f : [ T₁ ⟶ T₂ ] ρ̂) → f [∘] [id] ≅-⟶ f
  [∘]-[id] f = [ P.refl ]

  [∘]-[∘] :
    ∀ {t₃ t₄} {T₃ : Term-like t₃} {T₄ : Term-like t₄}
      {Γ Δ Ε Ζ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {ρ̂₃ : Ε ⇨̂ Ζ}
    (f₃ : [ T₃ ⟶ T₄ ] ρ̂₃) (f₂ : [ T₂ ⟶ T₃ ] ρ̂₂)
    (f₁ : [ T₁ ⟶ T₂ ] ρ̂₁) →
    f₃ [∘] (f₂ [∘] f₁) ≅-⟶ (f₃ [∘] f₂) [∘] f₁
  [∘]-[∘] f₃ f₂ f₁ = [ P.refl ]

open Dummy public