--- a/automaton-in-agda/src/halt.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/halt.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible  #-}
+
 module halt where
 
 open import Level renaming ( zero to Zero ; suc to Suc )
@@ -92,8 +94,8 @@
      h-just h y eq with h y
      h-just h y refl | true = refl
      TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
-     TN1 h y with h y | inspect h y
-     ... | true  | record { eq = eq1 } = begin
+     TN1 h y with h y in eq1
+     ... | true  = begin
         Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
         true ∎  where
           tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ just true
@@ -101,7 +103,7 @@
               tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
               h1 h y ≡⟨ h-just h y eq1  ⟩
               just true  ∎  
-     ... | false | record { eq = eq1 } = begin
+     ... | false = begin
         Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
         false ∎  where
           tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ nothing