start doing the boundary calculuations, a lot of unexpectedly dumb obligations

code/gcbpv.agda

@@ -216,7 +216,11 @@ _⟨_⟩vv : forall {Γ : VCtx onevar} {A} ->
          Value Γ A ->
          (i : Dimension) ->
          Value (Γ ⟪ i ⟫v) (A ⟨ i ⟩v)
-record ValCompat Γ⊤ Γ⊥ A⊤ A⊥ (pctx : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) (pty  : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v) : Set₁
+record ValCompat Γ⊤ Γ⊥ A⊤ A⊥
+  (pctx : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v)
+  (pty  : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v)
+  (v⊤ : Value Γ⊤ A⊤)
+  (v⊥ : Value Γ⊥ A⊥) : Set₁
 data Term  : forall {I} -> VCtx I -> CCtx I -> CType I -> Set₁
 _⟨_⟩cc : forall {Γ : VCtx onevar}{Δ}{B} ->
          Term Γ Δ B ->
@@ -237,18 +241,24 @@ data Value where
   valtrans : forall {Γ⊤}{Γ⊥}{A⊤}{A⊥} ->
              (pctx : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) ->
              (pty  : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v) ->
-             ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty ->
+             (v⊤ : Value Γ⊤ A⊤) ->
+             (v⊥ : Value Γ⊥ A⊥) -> 
+             ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty v⊤ v⊥ ->
              Value (vctxtrans Γ⊤ Γ⊥ pctx) (vtrans A⊤ A⊥ pty)
              -- VCtx.Vars Γ⊤ ≡ VCtx.Vars Γ⊥ ->
              -- {!!}
 
-_⟨_⟩vv = {!!}
+var Γ x ⟨ i ⟩vv = var (Γ ⟪ i ⟫v) x 
+vunit Γ ⟨ i ⟩vv = vunit (Γ ⟪ i ⟫v)
+vpair V V' ⟨ i ⟩vv = vpair (V ⟨ i ⟩vv) (V' ⟨ i ⟩vv)
+vdestr V Vk ⟨ i ⟩vv = vdestr (V ⟨ i ⟩vv) {!Vk ⟨ i ⟩vv!}
+vthunk M ⟨ i ⟩vv = vthunk {!M ⟨ i ⟩cc!}
+(valtrans pctx pty v⊤ v⊥ compat) ⟨ Top ⟩vv  = v⊤ ⟨ Top ⟩vv
+(valtrans pctx pty v⊤ v⊥ compat) ⟨ Bot ⟩vv  = {!v⊥ ⟨ Bot ⟩vv!}
 
-record ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty where
+record ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty v⊤ v⊥ where
   inductive
   field
-    v⊤ : Value Γ⊤ A⊤
-    v⊥ : Value Γ⊥ A⊥
     compat :
       subst (λ Γm → Value Γm (A⊥ ⟨ Top ⟩v)) pctx (subst (λ Am → Value (Γ⊤ ⟪ Bot ⟫v) Am) pty
       (v⊤ ⟨ Bot ⟩vv))
@@ -274,10 +284,26 @@ data Term where
          Term Γ (cdot _) B ->
          Term Γ Δ B
 
-_⟨_⟩cc = {!!}
+hole ⟨ i ⟩cc = hole
+lambda M ⟨ i ⟩cc = {!lambda (M ⟨ i ⟩cc)!}
+app M V ⟨ i ⟩cc = app (M ⟨ i ⟩cc) (V ⟨ i ⟩vv)
+force V ⟨ i ⟩cc = {!force (V ⟨ i ⟩vv)!}
+ret V ⟨ i ⟩cc = {!ret (V ⟨ i ⟩vv)!}
+lett M Mk ⟨ i ⟩cc = lett (M ⟨ i ⟩cc) {!Mk ⟨ i ⟩cc!}
 
 valrefl : forall {Γ}{A} -> Value Γ A -> Value (vctxrefl Γ) (vrefl A)
-valrefl = {!!}
-
 termrefl : forall {Γ}{Δ}{B} -> Term Γ Δ B -> Term (vctxrefl Γ) (cctxrefl Δ) (crefl B)
-termrefl = {!!}
+
+valrefl (var Γ x) = var _ x
+valrefl (vunit Γ) = vunit _
+valrefl (vpair V V') = vpair (valrefl V) (valrefl V')
+valrefl (vdestr V Vk) = vdestr (valrefl V) {!valrefl Vk!}
+valrefl (vthunk M) = vthunk {!termrefl M!}
+
+termrefl hole = hole
+termrefl (lambda M) = {!lambda (termrefl M)!}
+termrefl (app M V) = app (termrefl M) (valrefl V)
+termrefl (force V) = {!force (valrefl V)!}
+termrefl (ret V) = {!ret (valrefl V)!}
+termrefl (lett M Mk) = lett (termrefl M) {!(termrefl Mk)!}
+