htyp -> typ, #3

hazelgrove · Oct 12, 2020 · db4317b · db4317b
1 parent c192aad
commit db4317b
Show file tree

Hide file tree

Showing 21 changed files with 146 additions and 146 deletions.
diff --git a/canonical-boxed-forms.agda b/canonical-boxed-forms.agda
@@ -15,19 +15,19 @@ module canonical-boxed-forms where
 
   -- this type gives somewhat nicer syntax for the output of the canonical
   -- forms lemma for boxed values at arrow type
-  data cbf-arr : (Δ : hctx) (d : iexp) (τ1 τ2 : htyp) → Set where
+  data cbf-arr : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
     CBFLam : ∀{Δ d τ1 τ2} →
       (Σ[ x ∈ Nat ] Σ[ d' ∈ iexp ]
          (d == (·λ x [ τ1 ] d') × Δ , ■ (x , τ1) ⊢ d' :: τ2))
       → cbf-arr Δ d τ1 τ2
     CBFCastArr : ∀{Δ d τ1 τ2} →
-      (Σ[ d' ∈ iexp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
+      (Σ[ d' ∈ iexp ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
          (d == (d' ⟨ τ1' ==> τ2' ⇒ τ1 ==> τ2 ⟩) ×
          (τ1' ==> τ2' ≠ τ1 ==> τ2) ×
          (Δ , ∅ ⊢ d' :: τ1' ==> τ2')))
       → cbf-arr Δ d τ1 τ2
 
-  data cbf-prod : (Δ : hctx) (d : iexp) (τ1 τ2 : htyp) → Set where
+  data cbf-prod : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
     CBFPairVal : ∀{Δ d τ1 τ2} →
               (Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ]
                (d == ⟨ d1 , d2 ⟩ ×
@@ -45,7 +45,7 @@ module canonical-boxed-forms where
                 d2 boxedval  ))
               → cbf-prod Δ d τ1 τ2
     CBFCastProd : ∀{Δ d τ1 τ2} →
-                  (Σ[ d' ∈ iexp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
+                  (Σ[ d' ∈ iexp ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
                    (d == (d' ⟨ τ1' ⊗ τ2' ⇒ τ1 ⊗ τ2 ⟩) ×
                    (τ1' ⊗ τ2' ≠ τ1 ⊗ τ2) ×
                    (τ1' ⊗ τ2' ~ τ1 ⊗ τ2) ×
@@ -71,7 +71,7 @@ module canonical-boxed-forms where
   canonical-boxed-forms-hole : ∀{Δ d} →
                                Δ , ∅ ⊢ d :: ⦇·⦈ →
                                d boxedval →
-                               Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+                               Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
                                  ((d == d' ⟨ τ' ⇒ ⦇·⦈ ⟩) ×
                                   (τ' ground) ×
                                   (Δ , ∅ ⊢ d' :: τ'))
@@ -105,9 +105,9 @@ module canonical-boxed-forms where
                                    Δ , ∅ ⊢ d :: τ →
                                    d boxedval →
                                    τ ≠ b →
-                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
+                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ==> τ2)) →
                                    τ ≠ ⦇·⦈ →
-                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊗ τ2)) →
+                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ⊗ τ2)) →
                                    ⊥
   canonical-boxed-forms-coverage TAConst (BVVal x) nb na nh = λ _ → nb refl
   canonical-boxed-forms-coverage (TAVar x₁) (BVVal ()) nb na nh

diff --git a/canonical-indeterminate-forms.agda b/canonical-indeterminate-forms.agda
@@ -17,7 +17,7 @@ module canonical-indeterminate-forms where
         )
        → cif-base Δ d
     CIFBNEHole : ∀ {Δ d} →
-      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
         ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
          (Δ , ∅ ⊢ d' :: τ') ×
          (d' final) ×
@@ -26,17 +26,17 @@ module canonical-indeterminate-forms where
         )
         → cif-base Δ d
     CIFBAp : ∀ {Δ d} →
-      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2 ∈ htyp ]
+      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2 ∈ typ ]
         ((d == d1 ∘ d2) ×
          (Δ , ∅ ⊢ d1 :: τ2 ==> b) ×
          (Δ , ∅ ⊢ d2 :: τ2) ×
          (d1 indet) ×
          (d2 final) ×
-         ((τ3 τ4 τ3' τ4' : htyp) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
+         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
         )
         → cif-base Δ d
     CIFBFst : ∀{Δ d} →
-      Σ[ d' ∈ iexp ] Σ[ τ2 ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ2 ∈ typ ]
         ((d == fst d') ×
          (Δ , ∅ ⊢ d' :: b ⊗ τ2) ×
          (d' indet) ×
@@ -45,7 +45,7 @@ module canonical-indeterminate-forms where
         )
         → cif-base Δ d
     CIFBSnd : ∀{Δ d} →
-        Σ[ d' ∈ iexp ] Σ[ τ1 ∈ htyp ]
+        Σ[ d' ∈ iexp ] Σ[ τ1 ∈ typ ]
         ((d == snd d') ×
          (Δ , ∅ ⊢ d' :: τ1 ⊗ b) ×
          (d' indet) ×
@@ -58,11 +58,11 @@ module canonical-indeterminate-forms where
         ((d == d' ⟨ ⦇·⦈ ⇒ b ⟩) ×
          (Δ , ∅ ⊢ d' :: ⦇·⦈) ×
          (d' indet) ×
-         ((d'' : iexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
+         ((d'' : iexp) (τ' : typ) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
         )
         → cif-base Δ d
     CIFBFailedCast : ∀ {Δ d} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
         ((d == d' ⟨ τ' ⇒⦇⦈⇏ b ⟩) ×
          (Δ , ∅ ⊢ d' :: τ') ×
          (τ' ground) ×
@@ -86,7 +86,7 @@ module canonical-indeterminate-forms where
 
   -- this type gives somewhat nicer syntax for the output of the canonical
   -- forms lemma for indeterminates at arrow type
-  data cif-arr : (Δ : hctx) (d : iexp) (τ1 τ2 : htyp) → Set where
+  data cif-arr : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
     CIFAEHole : ∀{d Δ τ1 τ2} →
       Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
         ((d == ⦇⦈⟨ u , σ ⟩) ×
@@ -95,7 +95,7 @@ module canonical-indeterminate-forms where
         )
       → cif-arr Δ d τ1 τ2
     CIFANEHole : ∀{d Δ τ1 τ2} →
-      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
+      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ] Σ[ Γ ∈ tctx ]
         ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
          (Δ , ∅ ⊢ d' :: τ') ×
          (d' final) ×
@@ -104,17 +104,17 @@ module canonical-indeterminate-forms where
         )
         → cif-arr Δ d τ1 τ2
     CIFAAp : ∀{d Δ τ1 τ2} →
-      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2' ∈ htyp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
+      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2' ∈ typ ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ]
         ((d == d1 ∘ d2) ×
          (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ==> τ2)) ×
          (Δ , ∅ ⊢ d2 :: τ2') ×
          (d1 indet) ×
          (d2 final) ×
-         ((τ3 τ4 τ3' τ4' : htyp) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
+         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
         )
         → cif-arr Δ d τ1 τ2
     CIFAFst : ∀{Δ d τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
         ((d == fst d') ×
          (Δ , ∅ ⊢ d' :: (τ1 ==> τ2) ⊗ τ') ×
          (d' indet) ×
@@ -123,7 +123,7 @@ module canonical-indeterminate-forms where
         )
         → cif-arr Δ d τ1 τ2
     CIFASnd : ∀{Δ d τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
         ((d == snd d') ×
          (Δ , ∅ ⊢ d' :: τ' ⊗ (τ1 ==> τ2)) ×
          (d' indet) ×
@@ -132,7 +132,7 @@ module canonical-indeterminate-forms where
         )
         → cif-arr Δ d τ1 τ2
     CIFACast : ∀{d Δ τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
         ((d == d' ⟨ (τ1' ==> τ2') ⇒ (τ1 ==> τ2) ⟩) ×
           (Δ , ∅ ⊢ d' :: τ1' ==> τ2') ×
           (d' indet) ×
@@ -146,11 +146,11 @@ module canonical-indeterminate-forms where
          (τ2 == ⦇·⦈) ×
          (Δ , ∅ ⊢ d' :: ⦇·⦈) ×
          (d' indet) ×
-         ((d'' : iexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
+         ((d'' : iexp) (τ' : typ) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
         )
         → cif-arr Δ d τ1 τ2
     CIFAFailedCast : ∀{d Δ τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
           ((d == (d' ⟨ τ' ⇒⦇⦈⇏ ⦇·⦈ ==> ⦇·⦈ ⟩) ) ×
            (τ1 == ⦇·⦈) ×
            (τ2 == ⦇·⦈) ×
@@ -186,7 +186,7 @@ module canonical-indeterminate-forms where
         )
       → cif-hole Δ d
     CIFHNEHole : ∀ {Δ d} →
-      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
+      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ] Σ[ Γ ∈ tctx ]
         ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
          (Δ , ∅ ⊢ d' :: τ') ×
          (d' final) ×
@@ -195,17 +195,17 @@ module canonical-indeterminate-forms where
         )
       → cif-hole Δ d
     CIFHAp : ∀ {Δ d} →
-      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2 ∈ htyp ]
+      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2 ∈ typ ]
         ((d == d1 ∘ d2) ×
          (Δ , ∅ ⊢ d1 :: (τ2 ==> ⦇·⦈)) ×
          (Δ , ∅ ⊢ d2 :: τ2) ×
          (d1 indet) ×
          (d2 final) ×
-         ((τ3 τ4 τ3' τ4' : htyp) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
+         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
         )
       → cif-hole Δ d
     CIFHFst : ∀{Δ d} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: ⦇·⦈ ⊗ τ') ×
         (d' indet) ×
@@ -214,7 +214,7 @@ module canonical-indeterminate-forms where
        )
       → cif-hole Δ d
     CIFHSnd : ∀{Δ d} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊗ ⦇·⦈) ×
         (d' indet) ×
@@ -223,7 +223,7 @@ module canonical-indeterminate-forms where
        )
       → cif-hole Δ d
     CIFHCast : ∀ {Δ d} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
         ((d == d' ⟨ τ' ⇒ ⦇·⦈ ⟩) ×
          (Δ , ∅ ⊢ d' :: τ') ×
          (τ' ground) ×
@@ -247,7 +247,7 @@ module canonical-indeterminate-forms where
 
   -- this type gives somewhat nicer syntax for the output of the canonical
   -- forms lemma for indeterminates at product type
-  data cif-prod : (Δ : hctx) (d : iexp) (τ1 τ2 : htyp) → Set where
+  data cif-prod : (Δ : hctx) (d : iexp) (τ1 τ2 : typ) → Set where
     CIFPEHole : ∀{d Δ τ1 τ2} →
       Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
         ((d == ⦇⦈⟨ u , σ ⟩) ×
@@ -256,7 +256,7 @@ module canonical-indeterminate-forms where
         )
       → cif-prod Δ d τ1 τ2
     CIFPNEHole : ∀{d Δ τ1 τ2} →
-      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
+      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ] Σ[ Γ ∈ tctx ]
         ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
          (Δ , ∅ ⊢ d' :: τ') ×
          (d' final) ×
@@ -265,17 +265,17 @@ module canonical-indeterminate-forms where
         )
         → cif-prod Δ d τ1 τ2
     CIFPAp : ∀{d Δ τ1 τ2} →
-      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2' ∈ htyp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
+      Σ[ d1 ∈ iexp ] Σ[ d2 ∈ iexp ] Σ[ τ2' ∈ typ ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ]
         ((d == d1 ∘ d2) ×
          (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ⊗ τ2)) ×
          (Δ , ∅ ⊢ d2 :: τ2') ×
          (d1 indet) ×
          (d2 final) ×
-         ((τ3 τ4 τ3' τ4' : htyp) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
+         ((τ3 τ4 τ3' τ4' : typ) (d1' : iexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
         )
         → cif-prod Δ d τ1 τ2
     CIFPFst : ∀{Δ d τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
         ((d == fst d') ×
          (Δ , ∅ ⊢ d' :: (τ1 ⊗ τ2) ⊗ τ') ×
          (d' indet) ×
@@ -284,7 +284,7 @@ module canonical-indeterminate-forms where
         )
         → cif-prod Δ d τ1 τ2
     CIFPSnd : ∀{Δ d τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
         ((d == snd d') ×
          (Δ , ∅ ⊢ d' :: τ' ⊗ (τ1 ⊗ τ2)) ×
          (d' indet) ×
@@ -311,7 +311,7 @@ module canonical-indeterminate-forms where
         )
         → cif-prod Δ d τ1 τ2
     CIFPCast : ∀{d Δ τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ1 ∈ typ ] Σ[ τ2 ∈ typ ] Σ[ τ1' ∈ typ ] Σ[ τ2' ∈ typ ]
         ((d == d' ⟨ (τ1' ⊗ τ2') ⇒ (τ1 ⊗ τ2) ⟩) ×
           (Δ , ∅ ⊢ d' :: τ1' ⊗ τ2') ×
           (d' indet) ×
@@ -326,11 +326,11 @@ module canonical-indeterminate-forms where
          (τ2 == ⦇·⦈) ×
          (Δ , ∅ ⊢ d' :: ⦇·⦈) ×
          (d' indet) ×
-         ((d'' : iexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
+         ((d'' : iexp) (τ' : typ) → d' ≠ (d'' ⟨ τ' ⇒ ⦇·⦈ ⟩))
         )
         → cif-prod Δ d τ1 τ2
     CIFPFailedCast : ∀{d Δ τ1 τ2} →
-      Σ[ d' ∈ iexp ] Σ[ τ' ∈ htyp ]
+      Σ[ d' ∈ iexp ] Σ[ τ' ∈ typ ]
           ((d == (d' ⟨ τ' ⇒⦇⦈⇏ ⦇·⦈ ⊗ ⦇·⦈ ⟩) ) ×
            (τ1 == ⦇·⦈) ×
            (τ2 == ⦇·⦈) ×
@@ -360,9 +360,9 @@ module canonical-indeterminate-forms where
                                            Δ , ∅ ⊢ d :: τ →
                                            d indet →
                                            τ ≠ b →
-                                           ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
+                                           ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ==> τ2)) →
                                            τ ≠ ⦇·⦈ →
-                                           ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊗ τ2)) →
+                                           ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ⊗ τ2)) →
                                            ⊥
   canonical-indeterminate-forms-coverage TAConst () nb na nh
   canonical-indeterminate-forms-coverage (TAVar x₁) () nb na nh

diff --git a/canonical-value-forms.agda b/canonical-value-forms.agda
@@ -60,8 +60,8 @@ module canonical-value-forms where
                                    Δ , ∅ ⊢ d :: τ →
                                    d val →
                                    τ ≠ b →
-                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
-                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊗ τ2)) →
+                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ==> τ2)) →
+                                   ((τ1 : typ) (τ2 : typ) → τ ≠ (τ1 ⊗ τ2)) →
                                    ⊥
   canonical-value-forms-coverage1 TAConst VConst = λ z _ _ → z refl
   canonical-value-forms-coverage1 (TAVar x₁) ()

diff --git a/complete-preservation.agda b/complete-preservation.agda
@@ -29,7 +29,7 @@ module complete-preservation where
   -- bound in any of the constructors explicitly since it's only in the
   -- lambda case; so below i have no idea how else to get a name for it,
   -- instead of leaving it dotted in the context
-  lem-proj : {x : Nat} {d : iexp} { τ : htyp} → (·λ_[_]_ x τ d) dcomplete → Σ[ y ∈ Nat ] (y == x)
+  lem-proj : {x : Nat} {d : iexp} { τ : typ} → (·λ_[_]_ x τ d) dcomplete → Σ[ y ∈ Nat ] (y == x)
   lem-proj {x} (DCLam dc x₁) = x , refl
 
   -- a complete well typed term steps to a complete term.

diff --git a/complete-progress.agda b/complete-progress.agda
@@ -14,7 +14,7 @@ module complete-progress where
     V : ∀{d Δ} → d val → okc d Δ
     S : ∀{d Δ} → Σ[ d' ∈ iexp ] (d ↦ d') → okc d Δ
 
-  complete-progress : {Δ : hctx} {d : iexp} {τ : htyp} →
+  complete-progress : {Δ : hctx} {d : iexp} {τ : typ} →
                        Δ , ∅ ⊢ d :: τ →
                        d dcomplete →
                        okc d Δ

diff --git a/continuity.agda b/continuity.agda
@@ -16,17 +16,17 @@ module continuity where
     action : Set
     zexp : Set
     _◆ : zexp → eexp
-    _⊢_=>_~_~>_=>_ : (Γ : tctx) → (e1 : zexp) → (t1 : htyp)
-                        → (α : action) → (e2 : zexp) → (t2 : htyp) → Set
-    sensibility : {Γ : tctx} {e e' : zexp} {τ τ' : htyp} {α : action} →
+    _⊢_=>_~_~>_=>_ : (Γ : tctx) → (e1 : zexp) → (t1 : typ)
+                        → (α : action) → (e2 : zexp) → (t2 : typ) → Set
+    sensibility : {Γ : tctx} {e e' : zexp} {τ τ' : typ} {α : action} →
                   Γ ⊢ (e ◆) => τ →
                   Γ ⊢ e => τ ~ α ~> e' => τ' →
                   Γ ⊢ (e' ◆) => τ'
     binders-unique-h : eexp → Set
     binders-unique-z : zexp → Set
     binders-unique-cursor1 : ∀{e} → binders-unique-z e → binders-unique-h (e ◆)
     binders-unique-cursor2 : ∀{e} → binders-unique-h (e ◆) → binders-unique-z e
-    binders-unique-sensibility : {Γ : tctx} {e e' : zexp} {τ τ' : htyp} {α : action} →
+    binders-unique-sensibility : {Γ : tctx} {e e' : zexp} {τ τ' : typ} {α : action} →
                   binders-unique-z e →
                   Γ ⊢ e => τ ~ α ~> e' => τ' →
                   binders-unique-z e'