--- a/src/nat.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/nat.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module nat where
 
 open import Data.Nat 
@@ -104,15 +105,15 @@
 div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
 div2-eq zero = refl
 div2-eq (suc zero) = refl
-div2-eq (suc (suc x)) with div2 x | inspect div2 x 
-... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
+div2-eq (suc (suc x)) with div2 x in eq1 
+... | ⟪ x1 , true ⟫ = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
      div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩
      suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1  _ ) ⟩
      suc (suc (suc (x1 + x1))) ≡⟨⟩    
      suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ 
      suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ 
      suc (suc x) ∎  where open ≡-Reasoning
-... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
+... | ⟪ x1 , false ⟫ = begin
      div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩
      suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1  _ ) ⟩
      suc (suc (x1 + x1)) ≡⟨⟩    
@@ -724,15 +725,15 @@
           m ∎  where open ≤-Reasoning  
 
 0<factor : { m k : ℕ } → k > 0 → m > 0 →  (d :  Dividable k m ) → Dividable.factor d > 0
-0<factor {m} {k} k>0 m>0 d with Dividable.factor d | inspect Dividable.factor d 
-... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< ff1 m>0 ) where
+0<factor {m} {k} k>0 m>0 d with Dividable.factor d in eq1 
+... | zero = ⊥-elim ( nat-≡< ff1 m>0 ) where
     ff1 : 0 ≡ m 
     ff1 = begin
           0 ≡⟨⟩
           0 * k + 0 ≡⟨ cong  (λ j → j * k + 0) (sym eq1) ⟩
           Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d  ⟩
           m ∎  where open ≡-Reasoning  
-... | suc t | _ = s≤s z≤n 
+... | suc t = s≤s z≤n 
 
 div→k≤m : { m k : ℕ } → k > 1 → m > 0 →  Dividable k m → m ≥ k
 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k