extend tests

TestNat.agda

@@ -5,7 +5,8 @@ open import EWRSg
 open import Lib
 open import IFA
 
-module TestNat (N : Set) (z : N) (s : N → N) where
+module TestNat (N' : Set) (z' : N') (s' : N' → N')
+  (N : Set) (z : N) (s : N → N) where
 
 Γ : Con
 Γ = ∙ ▶S U ▶P El vz ▶P ΠP (vs{S}{P} vz) (El (vs{S}{P} (vs{S}{P} vz)))
@@ -25,3 +26,13 @@ module TestNat (N : Set) (z : N) (s : N → N) where
 Γw  : _
 Γw  = Con.w Γ {lift tt , N}
               (lift tt , z , s)
+
+ΓRc : _
+ΓRc = Con.Rc Γ {lift tt , N'}
+               (lift tt , z' , s')
+               (lift tt , N , z , s)
+
+ΓR : _
+ΓR = Con.R Γ {lift tt , N'}
+             (lift tt , z' , s')
+             (lift tt , N , z , s)

TestVec.agda

@@ -5,24 +5,36 @@ open import EWRSg
 open import Lib
 
 module TestVec (A : Set) (N : Set) (z : N) (s : N → N)
-   (V : Set) (n : V) (c : A → N → V → V) where
+   (V' : Set) (n' : V') (c' : A → N → V' → V')
+   (V : N → Set) (n : V z) (c : A → (n : N) → V n → V (s n)) where
 
 Γ : Con
 Γ = ∙ ▶S Π̂S N (λ _ → U)
       ▶P El (âppS vz z)
-      ▶P Π̂P A (λ a → Π̂P N (λ n → ΠP (âppS (vs{S}{P} vz) n) (El (âppS (vs{S}{P} (vs{S}{P} vz)) (s n)))))
+      ▶P Π̂P A (λ a → Π̂P N (λ n' → ΠP (âppS (vs{S}{P} vz) n') (El (âppS (vs{S}{P} (vs{S}{P} vz)) (s n')))))
 {-
-Γsg : Con.ᴬ Γ
-Γsg = Con.sg Γ (lift tt , )
+Γsg : C'on'.ᴬ Γ
+Γsg = C'on'.sg Γ (lift tt , )
                (lift tt , e)
-               (lift tt , Cw , Tw)
+               (lift tt , C'w , Tw)
                (lift tt , ew)
 -}
 
 Γwc : _
-Γwc = Con.wc Γ {lift tt , V}
-               (lift tt , n , c)
+Γwc = Con.wc Γ {lift tt , V'}
+               (lift tt , n' , c')
 
 Γw  : _
-Γw  = Con.w Γ {lift tt , V}
-              (lift tt , n , c)
+Γw  = Con.w Γ {lift tt , V'}
+              (lift tt , n' , c')
+
+ΓRc : _
+ΓRc = Con.Rc Γ {lift tt , V'}
+               (lift tt , n' , c')
+               (lift tt , V , n , c)               
+
+ΓR : _
+ΓR = Con.R Γ {lift tt , V'}
+             (lift tt , n' , c')
+             (lift tt , V , n , c)               
+