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)