Add computation transitivity, some sanity checking

code/gcbpv.agda

@@ -59,9 +59,14 @@ vtrans Atop Abot p ⟨ Bot ⟩v = Abot ⟨ Bot ⟩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 ->
+           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
 
 vrefl : VType (cdot _) -> VType onevar
 crefl : CType (cdot _) -> CType onevar
@@ -72,3 +77,31 @@ vrefl (U B) = U (crefl B)
 crefl (A ⇀ B) = vrefl A ⇀ crefl B
 crefl (F A) = F (vrefl A)
 
+vreflretract : forall A i -> vrefl A ⟨ i ⟩v ≡ A
+creflretract : forall B i -> crefl B ⟨ i ⟩c ≡ B
+
+vreflretract (VUnit .(ctx None ⊥-elim)) i = refl
+vreflretract (A × A₁) i = cong₂ _×_ (vreflretract A i) (vreflretract A₁ i)
+vreflretract (U B) i = cong U (creflretract B i)
+
+creflretract (A ⇀ B) i = cong₂ _⇀_ (vreflretract A i) (creflretract B i)
+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'
+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₃