\begin{code}
{-# OPTIONS --safe --without-K --postfix-projections #-}
module Generic.Simple.Environment (Ty : Set) where

  open import Data.LTree
  open import Data.LTree.Vector
  open import Function.Base
  open import Level
  open import Relation.Binary.PropositionalEquality
  open import Relation.Unary

  open import Generic.Simple.Syntax Ty

  private
    variable
      ℓ : Level
      𝓥 : Scoped ℓ
      T : Ctx → Set ℓ
      A : Ty
      Γ Δ Θ : Ctx

  record Var (A : Ty) (Γ : Ctx) : Set where
    constructor var
    field
      idx : Ptr (Γ .shape)
      tyq : Γ .ty-ctx idx ≡ A
  open Var public

  record _─Env (Γ : Ctx) (𝓥 : Scoped ℓ) (Δ : Ctx) : Set ℓ where
    constructor pack
    field lookup : ∀ {A} (v : Var A Γ) → 𝓥 A Δ
  open _─Env public

  leftᵛ : ∀ {s t A Γ} → Var A (ctx (Γ ∘ ↙)) → Var A (ctx {s <+> t} Γ)
  leftᵛ (var i q) = var (↙ i) q
  rightᵛ : ∀ {s t A Γ} → Var A (ctx (Γ ∘ ↘)) → Var A (ctx {s <+> t} Γ)
  rightᵛ (var i q) = var (↘ i) q

  Thinning : (Γ Δ : Ctx) → Set
  Thinning Γ Δ = (Γ ─Env) Var Δ

  □ : (Ctx → Set ℓ) → (Ctx → Set ℓ)
  (□ T) PΓ = ∀[ Thinning PΓ ⇒ T ]

  Thinnable : (Ctx → Set ℓ) → Set ℓ
  Thinnable T = ∀[ T ⇒ □ T ]

  th^Var : Thinnable (Var A)
  th^Var v th = th .lookup v

  identity : Thinning Γ Γ
  identity .lookup v = v

  select : Thinning Γ Δ → (Δ ─Env) 𝓥 Θ → (Γ ─Env) 𝓥 Θ
  select th ρ .lookup v = ρ .lookup (th .lookup v)

  extract : ∀[ □ T ⇒ T ]
  extract t = t identity

  duplicate : ∀[ □ T ⇒ □ (□ T) ]
  duplicate t th ph = t (select th ph)

  th^□ : Thinnable (□ T)
  th^□ = duplicate

  th^Env : (∀ {A} → Thinnable (𝓥 A)) → Thinnable ((Γ ─Env) 𝓥)
  th^Env th^𝓥 ρ th .lookup v = th^𝓥 (ρ .lookup v) th
\end{code}
