# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1694852690 -32400
# Node ID 77f01da94c4e7947c5270655b51223d50ebf8c98
# Parent  a067959c1799ca84947cd831fd8235c0ad3cfcdd
use safe option

diff -r a067959c1799 -r 77f01da94c4e src/FLComm.agda
--- a/src/FLComm.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/FLComm.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 module FLComm (n : ℕ) where
 
diff -r a067959c1799 -r 77f01da94c4e src/FLutil.agda
--- a/src/FLutil.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/FLutil.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 module FLutil where
 
 open import Level hiding ( suc ; zero )
diff -r a067959c1799 -r 77f01da94c4e src/Gutil.agda
--- a/src/Gutil.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Gutil.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module Gutil {n m : Level} (G : Group n m ) where
diff -r a067959c1799 -r 77f01da94c4e src/Homomorphism.agda
--- a/src/Homomorphism.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Homomorphism.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 -- fundamental homomorphism theorem
 --
diff -r a067959c1799 -r 77f01da94c4e src/NormalSubgroup.agda
--- a/src/NormalSubgroup.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/NormalSubgroup.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 module NormalSubgroup  where
 
diff -r a067959c1799 -r 77f01da94c4e src/Putil.agda
--- a/src/Putil.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Putil.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module Putil where
 
 open import Level hiding ( suc ; zero )
diff -r a067959c1799 -r 77f01da94c4e src/Solvable.agda
--- a/src/Solvable.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Solvable.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module Solvable {n m : Level} (G : Group n m ) where
diff -r a067959c1799 -r 77f01da94c4e src/Symmetric.agda
--- a/src/Symmetric.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Symmetric.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module Symmetric where
 
 open import Level hiding ( suc ; zero )
diff -r a067959c1799 -r 77f01da94c4e src/fin.agda
--- a/src/fin.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/fin.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible  #-}
+{-# OPTIONS --with-K #-}
 
 module fin where
 
diff -r a067959c1799 -r 77f01da94c4e src/logic.agda
--- a/src/logic.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/logic.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module logic where
 
 open import Level
@@ -97,55 +99,57 @@
 ¬-bool refl ()
 
 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
-lemma-∧-0 {true} {true} refl ()
 lemma-∧-0 {true} {false} ()
 lemma-∧-0 {false} {true} ()
 lemma-∧-0 {false} {false} ()
+lemma-∧-0 {true} {true} eq1 ()
 
 lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
-lemma-∧-1 {true} {true} refl ()
 lemma-∧-1 {true} {false} ()
 lemma-∧-1 {false} {true} ()
 lemma-∧-1 {false} {false} ()
+lemma-∧-1 {true} {true} eq1 ()
 
 bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
 bool-and-tt refl refl = refl
 
 bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
-bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {true} {true} eq =  refl
 bool-∧→tt-0 {false} {_} ()
 
 bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
-bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {true} eq = refl
 bool-∧→tt-1 {true} {false} ()
 bool-∧→tt-1 {false} {false} ()
 
 bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
-bool-or-1 {false} {true} refl = refl
-bool-or-1 {false} {false} refl = refl
+bool-or-1 {false} {true} eq = refl
+bool-or-1 {false} {false} eq = refl
 bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
-bool-or-2 {true} {false} refl = refl
-bool-or-2 {false} {false} refl = refl
+bool-or-2 {true} {false} eq = refl
+bool-or-2 {false} {false} eq = refl
 
 bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
 bool-or-3 {true} = refl
 bool-or-3 {false} = refl
 
 bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
-bool-or-31 {true} {true} refl = refl
-bool-or-31 {false} {true} refl = refl
+bool-or-31 {true} {true} eq = refl
+bool-or-31 {false} {true} eq = refl
 
 bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
 bool-or-4 {true} = refl
 bool-or-4 {false} = refl
 
 bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
-bool-or-41 {true} {b} refl = refl
+bool-or-41 {true} {b} eq = refl
 
 bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
-bool-and-1 {false} {b} refl = refl
+bool-and-1 {false} {b} eq = refl
 bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
-bool-and-2 {true} {false} refl = refl
-bool-and-2 {false} {false} refl = refl
+bool-and-2 {true} {false} eq = refl
+bool-and-2 {false} {false} eq = refl
+bool-and-2 {true} {true} ()
+bool-and-2 {false} {true} ()
 
 
diff -r a067959c1799 -r 77f01da94c4e src/nat.agda
--- a/src/nat.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/nat.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module nat where
 
 open import Data.Nat 
@@ -12,46 +13,39 @@
 open import Level hiding ( zero ; suc ) 
 
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
-nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+nat-<> {x} {y} x<y y<x with <-cmp x y
+... | tri< a ¬b ¬c = ¬c y<x
+... | tri≈ ¬a refl ¬c = ¬a x<y
+... | tri> ¬a ¬b c = ¬a x<y
 
 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
-nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+nat-≤>  {x} {y} x≤y y<x = ?
 
 nat-<≡ : { x : ℕ } → x < x → ⊥
-nat-<≡  (s≤s lt) = nat-<≡ lt
+nat-<≡  {x} lt = ?
 
 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
 nat-≡< refl lt = nat-<≡ lt
 
 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
-¬a≤a  (s≤s lt) = ¬a≤a  lt
+¬a≤a  lt = ?
 
 a<sa : {la : ℕ} → la < suc la 
 a<sa {zero} = s≤s z≤n
 a<sa {suc la} = s≤s a<sa 
 
 =→¬< : {x : ℕ  } → ¬ ( x < x )
-=→¬< {zero} ()
-=→¬< {suc x} (s≤s lt) = =→¬< lt
+=→¬< {zero} lt = ?
+=→¬< {suc x} lt = ?
 
 >→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
->→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+>→¬< = ?
 
 <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
-<-∨ {zero} {zero} (s≤s z≤n) = case1 refl
-<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
-<-∨ {suc x} {zero} (s≤s ())
-<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
-<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
-<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+<-∨  = ?
 
 ≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) )
-≤-∨ {zero} {zero} z≤n = case1 refl
-≤-∨ {zero} {suc y} z≤n = case2 (s≤s z≤n)
-≤-∨ {suc x} {zero} ()
-≤-∨ {suc x} {suc y} (s≤s lt) with ≤-∨ {x} {y} lt
-≤-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
-≤-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+≤-∨ = ?
 
 max : (x y : ℕ) → ℕ
 max zero zero = zero
@@ -74,13 +68,13 @@
 x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y
 x≤y→max=y zero zero x≤y = refl
 x≤y→max=y zero (suc y) x≤y = refl
-x≤y→max=y (suc x) (suc y) (s≤s x≤y) = cong suc (x≤y→max=y x y x≤y )
+x≤y→max=y = ?
 
 y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x
 y≤x→max=x zero zero y≤x = refl
 y≤x→max=x zero (suc y) ()
 y≤x→max=x (suc x) zero lt = refl
-y≤x→max=x (suc x) (suc y) (s≤s y≤x) = cong suc (y≤x→max=x x y y≤x )
+y≤x→max=x = ?
 
 -- _*_ : ℕ → ℕ → ℕ
 -- _*_ zero _ = zero
@@ -128,8 +122,7 @@
 
 px<py : {x y : ℕ } → pred x  < pred y → x < y
 px<py {zero} {suc y} lt = 0<s
-px<py {suc zero} {suc (suc y)} (s≤s lt) = s≤s 0<s
-px<py {suc (suc x)} {suc (suc y)} (s≤s lt) = s≤s (px<py {suc x} {suc y} lt)
+px<py = ?
 
 minus : (a b : ℕ ) →  ℕ
 minus a zero = a
@@ -139,8 +132,8 @@
 _-_ = minus
 
 sn-m=sn-m : {m n : ℕ } →  m ≤ n → suc n - m ≡ suc ( n - m )
-sn-m=sn-m {0} {n} z≤n = refl
-sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n
+sn-m=sn-m {0} {n} = ?
+sn-m=sn-m {suc m} {suc n} = ?
 
 si-sn=i-n : {i n : ℕ } → n < i  → suc (i - suc n) ≡ (i - n)
 si-sn=i-n {i} {n} n<i = begin
@@ -163,14 +156,14 @@
 n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s
 
 n-n-m=m : {m n : ℕ } → m ≤ n  → m ≡ (n - (n - m))
-n-n-m=m {0} {zero} z≤n = refl
-n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n
-n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin
-   suc n - ( n - m )    ≡⟨ sn-m=sn-m (n-m<n  n m) ⟩
-   suc (n - ( n - m ))  ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩
-   suc m
-   ∎  ) where
-      open ≡-Reasoning
+n-n-m=m {0} {zero} = ?
+n-n-m=m {0} {suc n} = ?
+n-n-m=m {suc m} {suc n} = ?
+--   suc n - ( n - m )    ≡⟨ sn-m=sn-m (n-m<n  n m) ⟩
+--   suc (n - ( n - m ))  ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩
+--   suc m
+--   ∎  ) where
+--      open ≡-Reasoning
 
 m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
 m+= {i} {j} {zero} refl = refl
@@ -180,35 +173,37 @@
 +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
 
 less-1 :  { n m : ℕ } → suc n < m → n < m
-less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
-less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
+less-1 = ?
+-- {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
+-- less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
 
 sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
-sa=b→a<b {0} {suc zero} refl = s≤s z≤n
-sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
+sa=b→a<b = ?
+-- {0} {suc zero} refl = s≤s z≤n
+-- sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)
 
 minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
 minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
-minus+n {zero} {suc y} (s≤s ())
-minus+n {suc x} {suc y} (s≤s lt) = begin
-           minus (suc x) (suc y) + suc y
-        ≡⟨ +-comm _ (suc y)    ⟩
-           suc y + minus x y 
-        ≡⟨ cong ( λ k → suc k ) (
-           begin
-                 y + minus x y 
-              ≡⟨ +-comm y  _ ⟩
-                 minus x y + y
-              ≡⟨ minus+n {x} {y} lt ⟩
-                 x 
-           ∎  
-           ) ⟩
-           suc x
-        ∎  where open ≡-Reasoning
+minus+n {zero} {suc y} = ?
+minus+n {suc x} {suc y} = ?
+--            minus (suc x) (suc y) + suc y
+--        ≡⟨ +-comm _ (suc y)    ⟩
+--           suc y + minus x y 
+--        ≡⟨ cong ( λ k → suc k ) (
+--           begin
+--                 y + minus x y 
+--              ≡⟨ +-comm y  _ ⟩
+--                 minus x y + y
+--              ≡⟨ minus+n {x} {y} lt ⟩
+--                 x 
+--           ∎  
+--           ) ⟩
+--           suc x
+--        ∎  where open ≡-Reasoning
 
 <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
-<-minus-0 {x} {suc _} {zero} lt = lt
-<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
+<-minus-0 {x} = ?
+-- <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
 
 <-minus : {x y z : ℕ } → x + z < y + z → x < y
 <-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )
@@ -228,43 +223,45 @@
         x + suc y ∎  where open ≤-Reasoning
 
 <-plus : {x y z : ℕ } → x < y → x + z < y + z 
-<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
-<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)
+<-plus = ?
+-- (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
+-- <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)
 
 <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
 <-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
 
 ≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
-≤-plus {0} {y} {zero} z≤n = z≤n
-≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y 
-≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )
+≤-plus = ?
+-- ≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y 
+-- ≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )
 
 ≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y 
 ≤-plus-0 {x} {y} {zero} lt = lt
 ≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
 
 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z 
-x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
-x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
+x+y<z→x<z = ?
+-- x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
 
 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
 *≤ lt = *-mono-≤ lt ≤-refl
 
 *< : {x y z : ℕ } → x < y → x * suc z < y * suc z 
-*< {zero} {suc y} lt = s≤s z≤n
-*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
+*< = ?
+-- {zero} {suc y} lt = s≤s z≤n
+-- *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
 
 <to<s : {x y  : ℕ } → x < y → x < suc y
-<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
-<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
+<to<s = ?
+-- <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
 
 <tos<s : {x y  : ℕ } → x < y → suc x < suc y
-<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
-<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
+<tos<s = ?
+-- <tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
 
 <to≤ : {x y  : ℕ } → x < y → x ≤ y 
-<to≤ {zero} {suc y} (s≤s z≤n) = z≤n
-<to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)
+<to≤ = ?
+-- <to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)
 
 <∨≤ : ( x y : ℕ ) →  (x < y ) ∨ (y ≤ x) 
 <∨≤ x y with <-cmp x y
@@ -280,62 +277,73 @@
 refl-≤≡ refl = refl-≤ 
 
 x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
-x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
-x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
+x<y→≤ = ?
+-- {zero} {.(suc _)} (s≤s z≤n) = z≤n
+-- x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
 
 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
-≤→= {0} {0} z≤n z≤n = refl
-≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
+≤→= = ?
+-- {0} {0} z≤n z≤n = refl
+-- ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
 
 px≤x : {x  : ℕ } → pred x ≤ x 
 px≤x {zero} = refl-≤
 px≤x {suc x} = refl-≤s
 
 px≤py : {x y : ℕ } → x ≤ y → pred x  ≤ pred y 
-px≤py {zero} {zero} lt = refl-≤
-px≤py {zero} {suc y} lt = z≤n
-px≤py {suc x} {suc y} (s≤s lt) = lt 
+px≤py = ?
+-- {zero} {zero} lt = refl-≤
+-- px≤py {zero} {suc y} lt = z≤n
+-- px≤py {suc x} {suc y} (s≤s lt) = lt 
 
 sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x  ≤ y 
-sx≤py→x≤y (s≤s lt) = lt
+sx≤py→x≤y = ?
+-- (s≤s lt) = lt
 
 sx<py→x<y : {x y : ℕ } → suc x < suc y → x  < y 
-sx<py→x<y (s≤s lt) = lt
+sx<py→x<y = ?
+-- (s≤s lt) = lt
 
 sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x  ≤ y 
-sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n
-sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le)
+sx≤y→x≤y  = ?
+-- {zero} {suc y} (s≤s le) = z≤n
+-- sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le)
 
 x<sy→x≤y : {x y : ℕ } → x < suc y → x  ≤ y 
-x<sy→x≤y {zero} {suc y} (s≤s le) = z≤n
-x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le)
-x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl
+x<sy→x≤y  = ?
+-- {zero} {suc y} (s≤s le) = z≤n
+-- x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le)
+-- x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl
 
 x≤y→x<sy : {x y : ℕ } → x ≤ y → x < suc y 
 x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n)
 x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le) 
 
 sx≤y→x<y : {x y : ℕ } → suc x ≤ y → x < y 
-sx≤y→x<y {zero} {suc y} (s≤s le) = s≤s z≤n
-sx≤y→x<y {suc x} {suc y} (s≤s le) = s≤s ( sx≤y→x<y {x} {y} le )
+sx≤y→x<y = ?
+-- {zero} {suc y} (s≤s le) = s≤s z≤n
+-- sx≤y→x<y {suc x} {suc y} (s≤s le) = s≤s ( sx≤y→x<y {x} {y} le )
 
 open import Data.Product
 
 i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j
-i-j=0→i=j {zero} {zero} _ refl = refl
-i-j=0→i=j {zero} {suc j} () refl
-i-j=0→i=j {suc i} {zero} z≤n ()
-i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq)
+i-j=0→i=j = ?
+-- {zero} {zero} _ refl = refl
+-- i-j=0→i=j {zero} {suc j} () refl
+-- i-j=0→i=j {suc i} {zero} z≤n ()
+-- i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq)
 
 m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
-m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl
-m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl
+m*n=0⇒m=0∨n=0 = ?
+-- {zero} {j} refl = case1 refl
+-- m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl
 
 
 minus+1 : {x y  : ℕ } → y ≤ x  → suc (minus x y)  ≡ minus (suc x) y 
-minus+1 {zero} {zero} y≤x = refl
-minus+1 {suc x} {zero} y≤x = refl
-minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x 
+minus+1  = ?
+-- {zero} {zero} y≤x = refl
+-- minus+1 {suc x} {zero} y≤x = refl
+-- minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x 
 
 minus+yz : {x y z : ℕ } → z ≤ y  → x + minus y z  ≡ minus (x + y) z
 minus+yz {zero} {y} {z} _ = refl
@@ -345,13 +353,15 @@
          minus (suc x + y) z ∎  where open ≡-Reasoning
 
 minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
-minus<=0 {0} {zero} z≤n = refl
-minus<=0 {0} {suc y} z≤n = refl
-minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
+minus<=0 = ?
+-- {0} {zero} z≤n = refl
+-- minus<=0 {0} {suc y} z≤n = refl
+-- minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
 
 minus>0 : {x y : ℕ } → x < y → 0 < minus y x 
-minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
-minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
+minus>0 = ?
+-- {zero} {suc _} (s≤s z≤n) = s≤s z≤n
+-- minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
 
 minus>0→x<y : {x y : ℕ } → 0 < minus y x  → x < y
 minus>0→x<y {x} {y} lt with <-cmp x y
@@ -374,8 +384,9 @@
 minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z  ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z})
 
 +cancel<l : (x z : ℕ ) {y : ℕ} → y + x < y + z → x < z
-+cancel<l x z {zero} lt = lt
-+cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt
++cancel<l x z = ?
+-- {zero} lt = lt
+-- +cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt
 
 +cancel<r : (x z : ℕ ) {y : ℕ} → x + y < z + y → x < z
 +cancel<r x z {y} lt = +cancel<l x z (subst₂ (λ j k → j < k ) (+-comm x _) (+-comm z _) lt ) 
@@ -476,36 +487,7 @@
            minus (minus k n * 0 ) 0
         ∎  where
         open ≡-Reasoning
-minus-* {suc m} {k} {n} lt with <-cmp k 1
-minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
-minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
-minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
-minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt 
-minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
-minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
-           minus k (suc n) * M
-        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
-           minus (k * M ) ((suc n) * M)
-        ≡⟨⟩
-           minus (k * M ) (M + n * M  )
-        ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
-           minus (k * M ) ((n * M) + M )
-        ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
-           minus (minus (k * M ) (n * M)) M
-        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
-           minus (minus k n * M ) M
-        ∎  where
-             M = suc m
-             lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
-             lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
-             lemma {suc n} {suc k} {m} lt = begin
-                         suc (suc m + suc n * suc m) 
-                      ≡⟨⟩
-                         suc ( suc (suc n) * suc m)
-                      ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
-                         suc (suc k * suc m)
-                      ∎   where open ≤-Reasoning
-             open ≡-Reasoning
+minus-* = ?
 
 x=y+z→x-z=y : {x y z : ℕ } → x ≡ y + z → x - z ≡ y
 x=y+z→x-z=y {x} {zero} {.x} refl = minus<=0 {x} {x} refl-≤ -- x ≡ suc (y + z) → (x ≡ y + z → x - z ≡ y)   → (x - z) ≡ suc y
@@ -564,7 +546,7 @@
     ind : {p : P} → Q (pnext p) → Q p
 
 y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x
-y<sx→y≤x (s≤s lt) = lt 
+y<sx→y≤x = ?
 
 fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
 fi0 .0 z≤n = refl
@@ -580,7 +562,7 @@
    f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p
    f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) 
    f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x)
-   ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a 
+   ... | tri< a ¬b ¬c = ?
    ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where
        f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x
        f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p}
@@ -596,7 +578,7 @@
     ind : {p : P} → Q (pnext p) → Q p
 
 s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j
-s≤s→≤ (s≤s lt) = lt
+s≤s→≤ = ?
 
 n-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
   → (f : P → ℕ) 
@@ -606,7 +588,7 @@
    f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x  →  Q p
    f-induction0 p zero lt = Ninduction.fzero I {p} (fi0 _ lt) 
    f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x) 
-   ... | tri< (s≤s a)  ¬b ¬c = f-induction0 p x a
+   ... | tri< a  ¬b ¬c = ?
    ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (s≤s→≤ nle) ) where
       f>0 :  0 < f (Ninduction.pnext I p)
       f>0 = subst (λ k → 0 < k ) (sym b) ( s≤s z≤n ) 
@@ -672,13 +654,7 @@
         k ∎ ) }  where open ≡-Reasoning
 
 div1 : { k : ℕ } → k > 1 →  ¬  Dividable k 1
-div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin
-    2 ≤⟨ k>1 ⟩
-    k ≡⟨ +-comm 0 _ ⟩
-    k + 0 ≡⟨ refl  ⟩
-    1 * k ≤⟨ *-mono-≤ {1} {suc f} (s≤s z≤n ) ≤-refl ⟩
-    suc f * k ≡⟨ +-comm 0 _ ⟩
-    suc f * k + 0 ∎  )) where open ≤-Reasoning  
+div1 {k} k>1 = ?
 
 div+div : { i j k : ℕ } →  Dividable k i →  Dividable k j → Dividable k (i + j) ∧ Dividable k (j + i)
 div+div {i} {j} {k} di dj = ⟪ div+div1 , subst (λ g → Dividable k g) (+-comm i j) div+div1 ⟫ where
@@ -760,19 +736,20 @@
         decl : {m  : ℕ } → 0 < m → m - k < m
         decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
         ind : (p : ℕ ) → Dec (Dividable k (p - k) ) → Dec (Dividable k p )
-        ind p (yes y) with <-cmp p k
-        ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) 
-        ... | tri> ¬a ¬b k<p  = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) 
-        ... | tri< a ¬b ¬c with <-cmp p 0
-        ... | tri≈ ¬a refl ¬c₁ = yes div0
-        ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where
-            not-div : (p f : ℕ) → p < k  → 0 < p → f * k + 0 ≡ p → ⊥
-            not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k
-              suc (suc p) ≤⟨ p<k ⟩
-              k ≤⟨ x≤x+y  ⟩
-              k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
-              suc f * k + 0 ∎  ) where open ≤-Reasoning  
-        ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=))  ) 
+        ind p (does₁ because proof₁) = ?
+    --    ind p (yes y) with <-cmp p k
+    --    ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) 
+    --    ... | tri> ¬a ¬b k<p  = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) 
+    --    ... | tri< a ¬b ¬c with <-cmp p 0
+    --    ... | tri≈ ¬a refl ¬c₁ = yes div0
+    --    ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where
+    --        not-div : (p f : ℕ) → p < k  → 0 < p → f * k + 0 ≡ p → ⊥
+    --        not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k
+    --          suc (suc p) ≤⟨ p<k ⟩
+    --          k ≤⟨ x≤x+y  ⟩
+    --          k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
+    --          suc f * k + 0 ∎  ) where open ≤-Reasoning  
+    --    ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=))  ) 
         I : Ninduction ℕ  _  F
         I = record {
               pnext = λ p → p - k
diff -r a067959c1799 -r 77f01da94c4e src/sym2.agda
--- a/src/sym2.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym2.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym2 where
diff -r a067959c1799 -r 77f01da94c4e src/sym2n.agda
--- a/src/sym2n.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym2n.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym2n where
diff -r a067959c1799 -r 77f01da94c4e src/sym3.agda
--- a/src/sym3.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym3.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym3 where
diff -r a067959c1799 -r 77f01da94c4e src/sym3n.agda
--- a/src/sym3n.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym3n.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym3n where
diff -r a067959c1799 -r 77f01da94c4e src/sym4.agda
--- a/src/sym4.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym4.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym4 where
diff -r a067959c1799 -r 77f01da94c4e src/sym5.agda
--- a/src/sym5.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym5 where
diff -r a067959c1799 -r 77f01da94c4e src/sym5a.agda
--- a/src/sym5a.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5a.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 --
 -- checking does not terminate, sorry
 --
diff -r a067959c1799 -r 77f01da94c4e src/sym5h.agda
--- a/src/sym5h.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5h.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym5h where
diff -r a067959c1799 -r 77f01da94c4e src/sym5n.agda
--- a/src/sym5n.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5n.agda	Sat Sep 16 17:24:50 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 {-# OPTIONS --guardedness #-}
 
 open import Level hiding ( suc ; zero )