module CBPV (Σv : Set) (Σc : Set) where

open import Data.Maybe
open import Relation.Binary.PropositionalEquality

data VType : Set
data CType : Set

data VType where
  base : Σv -> VType

data CType where
  base : Σc -> CType

data Nat : Set where
  O : Nat
  S : Nat -> Nat

data Fin : Nat -> Set where
  fO : ∀ n -> Fin (S n)
  fS : ∀ n -> Fin n -> Fin (S n)

record Iso (A B : Set) : Set where
  field
    to : A -> B
    fro : B -> A
    sect : ∀ (a : A) -> fro (to a) ≡ a
    retr : ∀ (b : B) -> to (fro b) ≡ b

record FinSet : Set₁ where
  field
    X : Set
    card : Nat
    is-finite : Iso X (Fin card)

VCtx : FinSet -> Set
VCtx U = FinSet.X U -> VType

record VCCtx (U : FinSet) : Set where
  constructor _/_
  field
    vvars : VCtx U
    stoup : Maybe CType

ValSig : Set₁
ValSig = ∀ {U} -> VCtx U -> VType -> Set

CompSig : Set₁
CompSig = ∀ {U} -> VCCtx U -> CType -> Set

module Terms (Σtmv : ValSig) (Σtmc : CompSig) where

  data _|-v_ {U} (Γ : VCtx U) : VType -> Set₁
  data _|-c_ {U} : (ΓH : VCCtx U) -> CType -> Set₁
  val-subst : ∀ U V -> VCtx U -> VCtx V -> Set₁
  data _|-mayc_ : ∀ {U} -> VCCtx U -> Maybe CType -> Set₁
  record comp-subst U V (ΓH : VCCtx U) (ΔH : VCCtx V) : Set₁

  data _|-v_ {U} (Γ : VCtx U) where
    var  : ∀ (u : FinSet.X U) -> Γ |-v (Γ u)
    base : ∀ V (Δ : VCtx V) A (f : Σtmv {V} Δ A) -> val-subst U V Γ Δ -> Γ |-v A
  data _|-c_ {U} where
    hole : ∀ (Γ : VCtx U) B -> (Γ / just B) |-c B
    base : ∀ (ΓH : VCCtx U) V (ΔH : VCCtx V) B (p : Σtmc {V} ΔH B) -> comp-subst U V ΓH ΔH -> ΓH |-c B
  val-subst U V Γ Δ    = ∀ (v : FinSet.X V) -> _|-v_ {U} Γ (Δ v)
  data _|-mayc_ where
    done : ∀ U (ΓH : VCCtx U)-> ΓH |-mayc nothing
    one  : ∀ U (ΓH : VCCtx U) B -> ΓH |-c B -> ΓH |-mayc (just B)
  record comp-subst U V ΓH ΔH where
    inductive
    field
      vsubst : val-subst U V (VCCtx.vvars ΓH) (VCCtx.vvars ΔH)
      csubst : ΓH |-mayc (VCCtx.stoup ΔH)

  vv-substitute : ∀ U V (Γ : VCtx U)(Δ : VCtx V) A -> val-subst U V Γ Δ -> Δ |-v A -> Γ |-v A
  vv-compose : ∀ U V W (Γ : VCtx U) (Δ : VCtx V) (E : VCtx W) -> val-subst W V E Δ -> val-subst V U Δ Γ -> val-subst W U E Γ
  vv-substitute U V Γ Δ .(Δ u) δ (var u) = δ u
  vv-substitute U V Γ Δ A δ (base V₁ Δ' .A f δ') = base V₁ Δ' A f (vv-compose V₁ V U _ _ _ δ δ')
  vv-compose U V W Γ Δ E δ γ = λ v → vv-substitute _ _ _ _ _ δ (γ v)