[agda] new version of composites, might work?

code/gcbpv.agda

@@ -2,11 +2,12 @@ module gcbpv where
 
 open import Data.Empty
 open import Data.Unit
-open import Data.Sum
+open import Data.Sum hiding (map)
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat
 open import Data.Fin
 open import Data.Vec
+import Data.Vec
 import Data.Vec.Properties
 open ≡-Reasoning
 
@@ -51,24 +52,34 @@ onevar = hstoup tt
 infix 90 _⟨_⟩v
 infix 90 _⟨_⟩c
 
+record VTC : Set
 data VType : DCtx -> Set
 _⟨_⟩v : VType onevar -> Dimension -> VType (cdot _)
 data CType : DCtx -> Set
 _⟨_⟩c : CType onevar -> Dimension -> CType (cdot _)
 
+-- | Transitivvity-composable pair of value types
+-- | "Value Transitivity Composite"
+record VTC where
+  inductive
+  field
+    A⊤ : VType onevar
+    A⊥ : VType onevar
+    eq : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v
+
 data VType where
   VUnit  : forall I -> VType I
   _×_    : forall {I} -> VType I -> VType I -> VType I
   U      : forall {I} -> CType I -> VType I
-  vtrans : forall (Atop : VType onevar) (Abot : VType onevar) ->
-           Atop ⟨ Bot ⟩v ≡ Abot ⟨ Top ⟩v ->
-           VType onevar
+  vtrans : VTC -> VType onevar
 
 VUnit _ ⟨ i ⟩v = VUnit _
 (A × A') ⟨ i ⟩v = (A ⟨ i ⟩v) × (A' ⟨ i ⟩v)
 U B ⟨ i ⟩v = U (B ⟨ i ⟩c)
-vtrans Atop Abot p ⟨ Top ⟩v = Atop ⟨ Top ⟩v
-vtrans Atop Abot p ⟨ Bot ⟩v = Abot ⟨ Bot ⟩v
+vtrans comp ⟨ Top ⟩v = VTC.A⊤ comp ⟨ Top ⟩v
+vtrans comp ⟨ Bot ⟩v = VTC.A⊥ comp ⟨ Bot ⟩v
+-- vtrans Atop Abot p ⟨ Top ⟩v = Atop ⟨ Top ⟩v
+-- vtrans Atop Abot p ⟨ Bot ⟩v = Abot ⟨ Bot ⟩v
 
 data CType where
   _⇀_ : forall {I} -> VType I -> CType I -> CType I
@@ -111,8 +122,8 @@ data CLt (B B' : CType (cdot _)) : Set where
 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₃
+-- 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))
@@ -128,11 +139,12 @@ clttrans B1 B2 B3 (lt B12 x x₁) (lt B23 x₂ x₃) = lt (ctrans B12 B23 (trans
 -- types we can implement reflexivity as weakening and only have to add in
 -- transitivity, beta and eta
 
-record VCtx (I : DCtx) : Set₁ where
+record VCtx (I : DCtx) : Set where
+  constructor vctx
   field
     Vars : ℕ
     vty  : Vec (VType I) Vars
-
+open VCtx
 
 infixl 20 _,,_
 _,,_ : forall {I} -> VCtx I -> VType I -> VCtx I
@@ -149,14 +161,14 @@ _⟪_⟫v : VCtx onevar -> Dimension -> VCtx (cdot _)
 vctxrefl : VCtx (cdot _) -> VCtx onevar
 vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map vrefl (VCtx.vty Γ) }
 
--- record VctxComp (Γ⊤ Γ⊥ : VCtx onevar) : Set₁ where
---   field
---     SameVar : Set
---     eq⊤     : SameVar ≡ VCtx.Vars Γ⊤
---     eq⊥     : SameVar ≡ VCtx.Vars Γ⊥
---     eqδ     :
---       forall (x : SameVar) ->
---       (VCtx.vty Γ⊤ (subst _ eq⊤ x) ⟨ Bot ⟩v) ≡ VCtx.vty Γ⊥ (subst _ eq⊥ x) ⟨ Top ⟩v
+record VCtxTC : Set where
+  field
+    Γ⊤ : VCtx onevar
+    Γ⊥ : VCtx onevar
+    eqvars : Vars Γ⊤ ≡ Vars Γ⊥
+    eqδ    : Vec VTC (VCtx.Vars Γ⊤)
+open VCtxTC
+
 
 -- eq-to-compvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VCtx.Vars Γ⊤ ≡ VCtx.Vars Γ⊥
 -- eq-to-compvars Γ⊤ Γ⊥ eq =
@@ -189,8 +201,39 @@ vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map vrefl (VCtx.vty
 --     VCtx.vty Γ⊥ Vars⊥ ⟨ Top ⟩v
 --   ∎
 
--- eq-to-comp : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VctxComp Γ⊤ Γ⊥
--- eq-to-comp Γ⊤ Γ⊥ p =
+-- mkeqvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> Vars Γ⊤ ≡ Vars Γ⊥
+-- mkeqvars Γ⊤ Γ⊥ p = 
+--     begin
+--       Vars Γ⊤
+--       ≡⟨ refl ⟩
+--       Vars (Γ⊤ ⟪ Bot ⟫v)
+--       ≡⟨ cong Vars p ⟩
+--       Vars (Γ⊥ ⟪ Top ⟫v)
+--       ≡⟨ refl ⟩
+--       Vars Γ⊥
+--     ∎
+
+
+-- eq-to-comp : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VctxTransComp Γ⊤ Γ⊥
+-- eq-to-comp Γ⊤ Γ⊥ p = record {
+--   eqvars = mkeqvars Γ⊤ Γ⊥ p;
+--   eqδ = tabulate λ x⊤ → record {
+--     A⊤ = lookup x⊤ (vty Γ⊤) ;
+--     A⊥ = lookup (subst Fin (mkeqvars Γ⊤ Γ⊥ p)  x⊤) (vty Γ⊥) ;
+--     compat =
+--       begin
+--         lookup x⊤ (vty Γ⊤) ⟨ Bot ⟩v
+--         ≡⟨ sym (lookup-map x⊤ (λ z → z ⟨ Bot ⟩v) (vty Γ⊤)) ⟩
+--         lookup x⊤ (vty (Γ⊤ ⟪ Bot ⟫v))
+--         ≡⟨ cong (lookup x⊤) {!p!} ⟩
+--         lookup x⊤ (subst (Vec (VType _)) _ (vty (Γ⊥ ⟪ Top ⟫v)))
+--         ≡⟨ {!!} ⟩
+--         lookup (subst Fin _ x⊤) (vty (Γ⊥ ⟪ Top ⟫v))
+--         ≡⟨ lookup-map _ (\z -> z ⟨ Top ⟩v) (vty Γ⊥) ⟩
+--         lookup (subst Fin _ x⊤) (vty Γ⊥) ⟨ Top ⟩v
+--       ∎
+--     }
+--   }
 --   record {
 --   SameVar = VCtx.Vars Γ⊤ ;
 --   eq⊤ = refl ;
@@ -207,14 +250,9 @@ vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map vrefl (VCtx.vty
 --     ∎
 --   }
 
--- vctxtrans : ∀ (Γ⊤ Γ⊥ : VCtx onevar) -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VCtx onevar
--- vctxtrans Γ⊤ Γ⊥ p with eq-to-comp Γ⊤ Γ⊥ p
--- vctxtrans Γ⊤ Γ⊥ p | record { SameVar = SameVar ; eq⊤ = eq⊤ ; eq⊥ = eq⊥ ; eqδ = eqδ } =
---   record { Vars = SameVar ; vty = λ x →
---     vtrans (VCtx.vty Γ⊤ (subst (λ z → z) eq⊤ x))
---            (VCtx.vty Γ⊥ (subst (λ z → z) eq⊥ x))
---            (eqδ x)
---   }
+vctxtrans : VCtxTC -> VCtx onevar
+vctxtrans record { Γ⊤ = Γ⊤ ; Γ⊥ = Γ⊥ ; eqvars = eqvars ; eqδ = eqδ } =
+ vctx (VCtx.Vars Γ⊤) (map vtrans eqδ)
 
 CCtx : DCtx -> Set
 CCtx I = StCtx (CType I)
@@ -227,22 +265,26 @@ cctxrefl : CCtx (cdot _) -> CCtx onevar
 cctxrefl (stctx None ty) = stctx None tt
 cctxrefl (stctx One ty) = stctx One (crefl ty) 
 
-data Value : forall {I} -> VCtx I -> VType I -> Set₁
+data Value : forall {I} -> VCtx I -> VType I -> Set
 _⟨_⟩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)
-  (v⊤ : Value Γ⊤ A⊤)
-  (v⊥ : Value Γ⊥ A⊥) : Set₁
-data Term  : forall {I} -> VCtx I -> CCtx I -> CType I -> Set₁
+record ValTC : Set
+data Term  : forall {I} -> VCtx I -> CCtx I -> CType I -> Set
 _⟨_⟩cc : forall {Γ : VCtx onevar}{Δ}{B} ->
          Term Γ Δ B ->
          (i : Dimension) ->
          Term (Γ ⟪ i ⟫v) (Δ ⟪ i ⟫c) (B ⟨ i ⟩c)
 
+record ValTC where
+  inductive
+  field
+    ΓΓ : VCtxTC
+    AA : VTC
+    V⊤ : Value (VCtxTC.Γ⊤ ΓΓ) (VTC.A⊤ AA)
+    V⊥ : Value (VCtxTC.Γ⊥ ΓΓ) (VTC.A⊥ AA)
+
 data Value where
   var : forall {I} (Γ : VCtx I) (x : Fin (VCtx.Vars Γ)) A -> A ≡ lookup x (VCtx.vty Γ) -> Value Γ A
   vunit : forall {I} (Γ : VCtx I) -> Value Γ (VUnit _)
@@ -254,13 +296,9 @@ data Value where
   vthunk : forall {I}{Γ : VCtx I}{B} ->
            Term Γ (cdot _) B ->
            Value Γ (U B)
-  -- valtrans : forall {Γ⊤}{Γ⊥}{A⊤}{A⊥} ->
-  --            (pctx : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) ->
-  --            (pty  : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v) ->
-  --            (v⊤ : Value Γ⊤ A⊤) ->
-  --            (v⊥ : Value Γ⊥ A⊥) -> 
-  --            ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty v⊤ v⊥ ->
-  --            Value (vctxtrans Γ⊤ Γ⊥ pctx) (vtrans A⊤ A⊥ pty)
+  valtrans : forall
+              (sq : ValTC) ->
+              Value (vctxtrans (ValTC.ΓΓ sq)) (vtrans (ValTC.AA sq))
 
 var Γ x A p ⟨ i ⟩vv = var (Γ ⟪ i ⟫v) x (A ⟨ i ⟩v)
   (begin
@@ -274,14 +312,8 @@ 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)
-
-record ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty v⊤ v⊥ where
-  inductive
-  field
-    compat :
-      subst (λ Γm → Value Γm (A⊥ ⟨ Top ⟩v)) pctx (subst (λ Am → Value (Γ⊤ ⟪ Bot ⟫v) Am) pty
-      (v⊤ ⟨ Bot ⟩vv))
-      ≡ v⊥ ⟨ Top ⟩vv
+valtrans sq ⟨ Top ⟩vv = {!!}
+valtrans sq ⟨ Bot ⟩vv = {!!}
 
 data Term where
   hole : forall {I}{Γ : VCtx I}{B} -> Term Γ (hstoup B) B
@@ -332,4 +364,3 @@ 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))
-