--- a/automaton-in-agda/src/cfg1.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/cfg1.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible  #-}
+
 module cfg1 where
 
 open import Level renaming ( suc to succ ; zero to Zero )
@@ -35,7 +37,7 @@
    field
       cfg : Symbol → Body Symbol 
       top : Symbol
-      eq? : Symbol → Symbol → Bool
+      eqP : Symbol → Symbol → Bool
       typeof : Symbol →  Node Symbol
 
 infixr  80 _｜_
@@ -64,11 +66,11 @@
 cfg-language1 :  {Symbol  : Set} → CFGGrammer Symbol   → Seq Symbol  →  List Symbol → Bool
 cfg-language1 cg Error x = false
 cfg-language1 cg (S ， seq) x with typeof cg S
-cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eq? cg x x' /\ cfg-language1 cg seq t
+cfg-language1 cg (_ ， seq) (x' ∷ t) | T x =  eqP cg x x' /\ cfg-language1 cg seq t
 cfg-language1 cg (_ ， seq) [] | T x = false
 cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x
 cfg-language1 cg (S ．) x with typeof cg S
-cfg-language1 cg (_ ．) (x' ∷ []) | T x =  eq? cg x x'
+cfg-language1 cg (_ ．) (x' ∷ []) | T x =  eqP cg x x'
 cfg-language1 cg (_ ．) _ | T x = false
 cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x
 
@@ -117,7 +119,7 @@
 IFGrammer = record {
       cfg = cfg'
     ; top = statement
-    ; eq? = token-eq?
+    ; eqP = token-eq?
     ; typeof = typeof-IFG 
    } where
      cfg' : IFToken → Body IFToken 
@@ -168,7 +170,7 @@
 E1Grammer = record {
       cfg = cfgE
     ; top = expr
-    ; eq? = E1-token-eq?
+    ; eqP = E1-token-eq?
     ; typeof = typeof-E1
    } where
      cfgE : E1Token → Body E1Token
@@ -286,7 +288,7 @@
 pda→cfg pda = record {
       cfg = {!!}
     ; top = {!!}
-    ; eq? = {!!}
+    ; eqP = {!!}
     ; typeof = {!!}
    } 
 
@@ -299,6 +301,6 @@
    field
       cdg : Seq Symbol  → Body Symbol 
       top : Symbol
-      eq? : Symbol → Symbol → Bool
+      eqP : Symbol → Symbol → Bool
       typeof : Symbol →  Node Symbol