[agda] change names, add upcast cells, need to add substitution

code/gcbpv.agda

@@ -34,8 +34,8 @@ hstoup : forall {Y : Set} -> Y -> StCtx Y
 hstoup B = record { S = One ; ty = B }
 
 data Dimension : Set where
-  Top : Dimension
-  Bot : Dimension
+  GT : Dimension
+  LT : Dimension
 
 DCtx : Set
 DCtx = StCtx ⊤
@@ -58,10 +58,9 @@ _⟨_⟩c : CType onevar -> Dimension -> CType (cdot _)
 record VTC where
   inductive
   field
-    A⊤ : VType onevar
-    A⊥ : VType onevar
-    eq : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v
-
+    Agt : VType onevar
+    Alt : VType onevar
+    eq : Agt ⟨ LT ⟩v ≡ Alt ⟨ GT ⟩v
 
 data VType where
   VUnit  : forall I -> VType I
@@ -72,26 +71,26 @@ data VType where
 VUnit _ ⟨ i ⟩v = VUnit _
 (A × A') ⟨ i ⟩v = (A ⟨ i ⟩v) × (A' ⟨ i ⟩v)
 U B ⟨ i ⟩v = U (B ⟨ i ⟩c)
-vtrans Vsq ⟨ Top ⟩v = VTC.A⊤ Vsq ⟨ Top ⟩v -- morally this: Vsq ⟨ Top ⟩vsq ⟨ Top ⟩v
-vtrans Vsq ⟨ Bot ⟩v = VTC.A⊥ Vsq ⟨ Bot ⟩v -- morally this: Vsq ⟨ Bot ⟩vsq ⟨ Bot ⟩v
--- vtrans Atop Abot p ⟨ Top ⟩v = Atop ⟨ Top ⟩v
--- vtrans Atop Abot p ⟨ Bot ⟩v = Abot ⟨ Bot ⟩v
+vtrans Vsq ⟨ GT ⟩v = VTC.Agt Vsq ⟨ GT ⟩v -- morally this: Vsq ⟨ GT ⟩vsq ⟨ GT ⟩v
+vtrans Vsq ⟨ LT ⟩v = VTC.Alt Vsq ⟨ LT ⟩v -- morally this: Vsq ⟨ LT ⟩vsq ⟨ LT ⟩v
+-- vtrans Atop Abot p ⟨ GT ⟩v = Atop ⟨ GT ⟩v
+-- vtrans Atop Abot p ⟨ LT ⟩v = Abot ⟨ LT ⟩v
 
 data CType where
   _⇀_ : forall {I} -> VType I -> CType I -> CType I
   F   : forall {I} -> VType I -> CType I
   ctrans : forall (Btop : CType onevar) (Bbot : CType onevar) ->
-           Btop ⟨ Bot ⟩c ≡ Bbot ⟨ Top ⟩c ->
+           Btop ⟨ LT ⟩c ≡ Bbot ⟨ GT ⟩c ->
            CType onevar
 
 (A ⇀ B) ⟨ i ⟩c = (A ⟨ i ⟩v) ⇀ (B ⟨ i ⟩c)
 F A ⟨ i ⟩c = F (A ⟨ i ⟩v)
-ctrans Btop Bbot p ⟨ Top ⟩c = Btop ⟨ Top ⟩c
-ctrans Btop Bbot p ⟨ Bot ⟩c = Bbot ⟨ Bot ⟩c
+ctrans Btop Bbot p ⟨ GT ⟩c = Btop ⟨ GT ⟩c
+ctrans Btop Bbot p ⟨ LT ⟩c = Bbot ⟨ LT ⟩c
 
 _⟨_⟩vsq : VTC -> Dimension -> VType onevar
-Vsq ⟨ Top ⟩vsq = VTC.A⊤ Vsq
-Vsq ⟨ Bot ⟩vsq = VTC.A⊥ Vsq
+Vsq ⟨ GT ⟩vsq = VTC.Agt Vsq
+Vsq ⟨ LT ⟩vsq = VTC.Alt Vsq
 
 vrefl : VType (cdot _) -> VType onevar
 crefl : CType (cdot _) -> CType onevar
@@ -114,22 +113,9 @@ creflretract (F A) i = cong F (vreflretract A i)
 
 -- | For a more traditional presentation of ordering
 data VLt (A A' : VType (cdot _)) : Set where
-  lt : forall (Aord : VType onevar) -> Aord ⟨ Top ⟩v ≡ A -> Aord ⟨ Bot ⟩v ≡ A' -> VLt A A'
+  lt : forall (Aord : VType onevar) -> Aord ⟨ GT ⟩v ≡ A -> Aord ⟨ LT ⟩v ≡ A' -> VLt A A'
 data CLt (B B' : CType (cdot _)) : Set where
-  lt : forall (Bord : CType onevar) -> Bord ⟨ Top ⟩c ≡ B -> Bord ⟨ Bot ⟩c ≡ B' -> CLt B B'
-
--- | Some sanity checking
--- vltrefl : forall A -> VLt A A
--- vltrefl A = lt (vrefl A) (vreflretract A Top) ((vreflretract A Bot))
-
--- vlttrans : forall A1 A2 A3 -> VLt A1 A2 -> VLt A2 A3 -> VLt A1 A3
--- vlttrans A1 A2 A3 (lt A12 x x₁) (lt A23 x₂ x₃) = lt (vtrans A12 A23 (trans x₁ (sym x₂))) x x₃
-
--- cltrefl : forall B -> CLt B B
--- cltrefl B = lt (crefl B) (creflretract B Top) ((creflretract B Bot))
-
-clttrans : forall B1 B2 B3 -> CLt B1 B2 -> CLt B2 B3 -> CLt B1 B3
-clttrans B1 B2 B3 (lt B12 x x₁) (lt B23 x₂ x₃) = lt (ctrans B12 B23 (trans x₁ (sym x₂))) x x₃
+  lt : forall (Bord : CType onevar) -> Bord ⟨ GT ⟩c ≡ B -> Bord ⟨ LT ⟩c ≡ B' -> CLt B B'
 
 -- | Now the term structure
 -- Values correspond to complex values in cbpv
@@ -146,6 +132,9 @@ record VCtx (I : DCtx) : Set where
     vty  : Vec (VType I) Vars
 open VCtx
 
+vcdot : ∀ I -> VCtx I
+vcdot I = vctx zero []
+
 infixl 20 _,,_
 _,,_ : forall {I} -> VCtx I -> VType I -> VCtx I
 Vars (Γ ,, A) = suc (Vars Γ)
@@ -179,8 +168,8 @@ vctxtrans : VCtxTC -> VCtx onevar
 vctxtrans Γsq = vctx (Vars Γsq) (map vtrans (vty Γsq))
 
 vtrans-dapp-lem : ∀ Vsq i ->  vtrans Vsq ⟨ i ⟩v ≡ Vsq ⟨ i ⟩vsq ⟨ i ⟩v
-vtrans-dapp-lem Vsq Top = refl
-vtrans-dapp-lem Vsq Bot = refl
+vtrans-dapp-lem Vsq GT = refl
+vtrans-dapp-lem Vsq LT = refl
 
 ctxttrans-dapp-lem : ∀ Γsq i -> vctxtrans Γsq ⟪ i ⟫v ≡ Γsq ⟪ i ⟫vsq ⟪ i ⟫v
 ctxttrans-dapp-lem Γsq i =
@@ -209,7 +198,7 @@ stctx One ty ⟪ i ⟫c = stctx One (ty ⟨ i ⟩c)
 
 cctxrefl : CCtx (cdot _) -> CCtx onevar
 cctxrefl (stctx None ty) = stctx None tt
-cctxrefl (stctx One ty) = stctx One (crefl ty) 
+cctxrefl (stctx One ty) = stctx One (crefl ty)
 
 data Value : forall {I} -> VCtx I -> VType I -> Set
 _⟨_⟩vv : forall {Γ : VCtx onevar} {A} ->
@@ -228,8 +217,8 @@ record ValTC where
   field
     ΓΓ : VCtxTC
     AA : VTC
-    V⊤ : Value (ΓΓ ⟪ Top ⟫vsq) (AA ⟨ Top ⟩vsq)
-    V⊥ : Value (ΓΓ ⟪ Bot ⟫vsq) (AA ⟨ Bot ⟩vsq)
+    Vgt : Value (ΓΓ ⟪ GT ⟫vsq) (AA ⟨ GT ⟩vsq)
+    Vlt : Value (ΓΓ ⟪ LT ⟫vsq) (AA ⟨ LT ⟩vsq)
 
 data Value where
   var : forall {I} (Γ : VCtx I) (x : Fin (Vars Γ)) A -> A ≡ lookup x (vty Γ) -> Value Γ A
@@ -245,6 +234,16 @@ data Value where
   valtrans : forall
               (sq : ValTC) ->
               Value (vctxtrans (ValTC.ΓΓ sq)) (vtrans (ValTC.AA sq))
+  vupcast : forall
+              {Γ} Aord ->
+              Value Γ (Aord ⟨ LT ⟩v) ->
+              Value Γ (Aord ⟨ GT ⟩v)
+  vupl : forall
+           Aord ->
+           Value (vcdot _ ,, vrefl (Aord ⟨ LT ⟩v)) Aord
+  vupr : forall
+           Aord ->
+           Value (vcdot _ ,, Aord) (vrefl (Aord ⟨ GT ⟩v))
 
 var Γ x A p ⟨ i ⟩vv = var (Γ ⟪ i ⟫v) x (A ⟨ i ⟩v)
   (begin
@@ -258,8 +257,12 @@ 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 sq ⟨ Top ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) Top = ValTC.V⊤ sq ⟨ Top ⟩vv
-valtrans sq ⟨ Bot ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) Bot = ValTC.V⊥ sq ⟨ Bot ⟩vv
+valtrans sq ⟨ GT ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) GT = ValTC.Vgt sq ⟨ GT ⟩vv
+valtrans sq ⟨ LT ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) LT = ValTC.Vlt sq ⟨ LT ⟩vv
+vupl Aord ⟨ GT ⟩vv = vupcast Aord (var _ zero _ (sym (vreflretract _ _)))
+vupl Aord ⟨ LT ⟩vv = var _ zero _ (sym (vreflretract _ _))
+vupr Aord ⟨ GT ⟩vv = var _ zero _ (vreflretract _ _)
+vupr Aord ⟨ LT ⟩vv rewrite vreflretract (Aord ⟨ GT ⟩v) LT = vupcast Aord (var _ zero _ refl)
 
 data Term where
   hole : forall {I}{Γ : VCtx I}{B} -> Term Γ (hstoup B) B
@@ -303,6 +306,7 @@ 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)
+valrefl (vupcast Aord V) = {!!} -- Need to use substitution here!
 
 termrefl hole = hole
 termrefl (lambda M) = lambda (termrefl M)