Mercurial > hg > Members > kono > Proof > galois

changeset 318:fff18d4a063b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use stdlib-2.0 and safe-mode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 18 Sep 2023 13:19:37 +0900
parents a067959c1799
children 8fb16f9a882a
files Galois.agda-lib src/FLComm.agda src/FLutil.agda src/Gutil.agda src/Homomorphism.agda src/NormalSubgroup.agda src/Putil.agda src/Solvable.agda src/Symmetric.agda src/fin.agda src/logic.agda src/nat.agda src/sym2.agda src/sym2n.agda src/sym3.agda src/sym3n.agda src/sym4.agda src/sym5.agda src/sym5a.agda src/sym5h.agda src/sym5n.agda
diffstat 21 files changed, 119 insertions(+), 76 deletions(-) [+]
line wrap: on
line diff
--- a/Galois.agda-lib	Sat Sep 16 13:14:17 2023 +0900
+++ b/Galois.agda-lib	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,6 @@
 name: Galois
-depend: standard-library
+depend: standard-library-2.0
 include: src 
+flags:
+  --warning=noUnsupportedIndexedMatch
+
--- a/src/FLComm.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/FLComm.agda	Mon Sep 18 13:19:37 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
 
--- a/src/FLutil.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/FLutil.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 module FLutil where
 
 open import Level hiding ( suc ; zero )
@@ -33,15 +33,23 @@
 FLpos : {n : ℕ} → FL (suc n) → Fin (suc n)
 FLpos (x :: _) = x
 
+fin-≡< :  {n : ℕ } {x : Fin n } {y : Fin n}  → x ≡ y → y Data.Fin.< x → ⊥
+fin-≡< {n} {x} {y} eq y<x with <-fcmp x y
+... | tri< a ¬b ¬c = ¬b eq
+... | tri≈ ¬a refl ¬c = nat-≡< refl y<x
+... | tri> ¬a ¬b c = ¬b eq
+                                                                
+f-≡< :  {n : ℕ } {x : FL n } {y : FL n}  → x ≡ y → y f< x → ⊥
+f-≡< eq (f<t lt2) = f-≡< (proj₂ (FLeq eq)) lt2
+f-≡< eq (f<n {_} {xn} {yn} xn<yn) = fin-≡< (proj₁ (FLeq eq)) xn<yn
+
 f-<> :  {n : ℕ } {x : FL n } {y : FL n}  → x f< y → y f< x → ⊥
 f-<> (f<n x) (f<n x₁) = nat-<> x x₁
 f-<> (f<n x) (f<t lt2) = nat-≡< refl x
-f-<> (f<t lt) (f<n x) = nat-≡< refl x
-f-<> (f<t lt) (f<t lt2) = f-<> lt lt2
-
-f-≡< :  {n : ℕ } {x : FL n } {y : FL n}  → x ≡ y → y f< x → ⊥
-f-≡< refl (f<n x) = nat-≡< refl x
-f-≡< refl (f<t lt) = f-≡< refl lt 
+f-<> (f<t {m} {xn} {xt} {yt} lt) lt2 = f-<> lt (fl00 refl lt2) where
+    fl00 : {yn : Fin (suc m) } → xn ≡ yn   → (xn :: yt) f< (yn :: xt) → yt f< xt
+    fl00 eq (f<n xn<yn) = ⊥-elim (fin-≡< (sym eq) xn<yn)
+    fl00 eq (f<t lt3) = lt3
 
 FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
 FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
--- a/src/Gutil.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Gutil.agda	Mon Sep 18 13:19:37 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
--- a/src/Homomorphism.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Homomorphism.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 -- fundamental homomorphism theorem
 --
--- a/src/NormalSubgroup.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/NormalSubgroup.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,4 +1,5 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 module NormalSubgroup  where
 
--- a/src/Putil.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Putil.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible --safe #-}
 module Putil where
 
 open import Level hiding ( suc ; zero )
@@ -29,7 +29,7 @@
 -- An inductive construction of permutation
 
 pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
-pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+pprep {n} perm =  permutation p→ p← piso←  piso→ where
    p→ : Fin (suc n) → Fin (suc n)
    p→ zero = zero
    p→ (suc x) = suc ( perm  ⟨$⟩ʳ x)
@@ -47,7 +47,7 @@
    piso→ (suc x) = cong (λ k → suc k ) (inverseˡ perm) 
 
 pswap  : {n : ℕ }  → Permutation n n → Permutation (suc (suc n)) (suc (suc  n ))
-pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+pswap {n} perm = permutation p→ p← piso←  piso→ where
    p→ : Fin (suc (suc n)) → Fin (suc (suc n)) 
    p→ zero = suc zero 
    p→ (suc zero) = zero 
@@ -122,12 +122,12 @@
 --     pins1 zero _ _ = pid
 --     pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  pins1 i j (≤-trans si≤n a≤sa ) 
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 open ≡-Reasoning
 
 pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
 pins {_} {zero} _ = pid
-pins {suc n} {suc m} (s≤s  m≤n) = permutation p← p→  record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
+pins {suc n} {suc m} (s≤s  m≤n) = permutation p← p→ piso→   piso← where
 
    next : Fin (suc (suc n)) → Fin (suc (suc n))
    next zero = suc zero
@@ -197,7 +197,7 @@
             p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
             p11 = begin
                fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
-              ≡⟨ lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )}  ⟩
+              ≡⟨ ? ⟩  -- lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )}  ⟩
                suc (fromℕ< (fin<n {suc n} {x} )) 
               ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
                suc x
@@ -232,7 +232,7 @@
              fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))
           ≡⟨⟩
              fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) 
-          ≡⟨ lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩
+          ≡⟨ ? ⟩  -- lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩
              fromℕ< ( s≤s (fin<n {suc n} {x}) )
           ≡⟨⟩
              suc (fromℕ< (fin<n {suc n} {x} )) 
@@ -278,7 +278,7 @@
           p004 = p003  (fromℕ< (s≤s (s≤s m≤n))) (
              begin
                 fromℕ< (s≤s (s≤s m≤n))
-             ≡⟨  lemma10 {suc (suc n)}  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
+             ≡⟨ ? ⟩ --  lemma10 {suc (suc n)}  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
                 fromℕ< (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) )
              ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
                 suc t
@@ -467,7 +467,7 @@
 
 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] 
 shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
-shrink {n} perm p0=0  = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+shrink {n} perm p0=0  = permutation p→ p← piso← piso→  where
 
    p→ : Fin n → Fin n 
    p→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) 
@@ -496,9 +496,9 @@
           plem1 = begin
                suc t1
             ≡⟨ sym e1 ⟩
-               Inverse.to perm Π.⟨$⟩ suc t
-            ≡⟨ cong (λ k →  Inverse.to perm Π.⟨$⟩ k ) (sym e0) ⟩
-               Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x )
+               Inverse.to perm  _
+            ≡⟨ cong (λ k →  Inverse.to perm k ) (sym e0) ⟩
+               Inverse.to perm ( Inverse.from perm _ )
             ≡⟨ inverseʳ perm   ⟩
                suc x
             ∎ 
@@ -517,14 +517,11 @@
           plem2 refl = refl
           plem3 :  suc t1 ≡ suc x
           plem3 = begin
-               suc t1
-            ≡⟨ sym e1 ⟩
-               Inverse.from perm Π.⟨$⟩ suc t
-            ≡⟨ cong (λ k →  Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩
-               Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x )
-            ≡⟨ inverseˡ perm   ⟩
-               suc x
-            ∎
+               suc t1 ≡⟨ sym e1 ⟩
+               Inverse.from perm (suc t)  ≡⟨ cong (λ k →  Inverse.from perm k ) (sym e0 ) ⟩
+               Inverse.from perm ((Inverse.to perm (suc x)) ) ≡⟨ cong (λ k →  Inverse.from perm (Inverse.to perm (suc x)) ) (sym e0 ) ⟩
+               Inverse.from perm ( Inverse.to perm  _ ) ≡⟨ inverseˡ perm   ⟩
+               suc x ∎
 
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
 shrink-iso {n} {perm} = record { peq = λ q → refl  } 
--- a/src/Solvable.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Solvable.agda	Mon Sep 18 13:19:37 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
--- a/src/Symmetric.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Symmetric.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module Symmetric where
 
 open import Level hiding ( suc ; zero )
@@ -22,11 +24,11 @@
 
 -- Data.Fin.Permutation.id
 pid : {p : ℕ } → Permutation p p
-pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
+pid = permutation fid fid (λ x → refl) (λ x → refl) -- record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl } 
 
 -- Data.Fin.Permutation.flip
 pinv : {p : ℕ } → Permutation p p → Permutation p p
-pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
+pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) (λ x → inverseˡ P ) ( λ x → inverseʳ P) -- record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
 
 record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
     field
@@ -57,7 +59,13 @@
 presp : { p : ℕ } {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
 presp {p} {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
    lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
-   lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
+   lemma4 q = begin
+          ((x ∘ₚ u) ⟨$⟩ʳ q) ≡⟨ peq u=v _ ⟩
+          ((x ∘ₚ v) ⟨$⟩ʳ q) ≡⟨ cong (λ k → Inverse.to v k  ) (peq x=y _) ⟩
+          ((y ∘ₚ v) ⟨$⟩ʳ q) ∎  
+     where 
+       open ≡-Reasoning
+   -- lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
 passoc : { p : ℕ } (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
 passoc x y z = record { peq = λ q → refl }
 p-inv : { p : ℕ } {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
--- a/src/fin.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/fin.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-} 
+{-# OPTIONS --cubical-compatible  --safe #-}
 
 module fin where
 
@@ -33,11 +33,11 @@
 toℕ→from {0} {zero} refl = refl
 toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))
 
-0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
-0≤fmax  = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n
+-- 0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
+-- 0≤fmax {n} = ?
 
-0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
-0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)
+-- 0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
+-- 0<fmax {n} = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< {suc n} {suc (suc n)} a<sa)) (s≤s z≤n)
 
 -- toℕ-injective
 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
@@ -87,23 +87,25 @@
 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  ) 
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- this requires K
+--
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 -- <-irrelevant
-<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
+-- <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+-- <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+-- <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )
 
-lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
-lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
-lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
+-- lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
+-- lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
+-- lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
 
 -- fromℕ<-irrelevant 
-lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
-lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
+-- lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
+-- lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
 
-lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
-lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
+-- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
+-- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
 
 -- toℕ-fromℕ<
 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
@@ -271,9 +273,9 @@
           ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ ))
           ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1)
      fdup-phase0 : FDup-in-list (suc n) qs 
-     fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs
-     ... | true  | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq }
-     ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup)  where
+     fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs in eq 
+     ... | true  = record { dup = fromℕ< a<sa ; is-dup = eq }
+     ... | false = fdup+1 qs (FDup-in-list.dup fdup) eq (FDup-in-list.is-dup fdup)  where
            -- if no dup in the max element, the list without the element is only one length shorter
            fless : (qs : List (Fin (suc n))) → length qs > suc n  → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) 
            fless qs lt p = fl-phase1 n qs lt p where
@@ -295,6 +297,6 @@
                ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p )
            -- if the list without the max element is only one length shorter, we can recurse
            fdup : FDup-in-list n (list-less qs)
-           fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne)
+           fdup = fin-dup-in-list>n (list-less qs) (fless qs lt eq)
 
 --
--- a/src/logic.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/logic.agda	Mon Sep 18 13:19:37 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} ()
 
 
--- 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
--- a/src/sym2.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym2.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym2 where
--- a/src/sym2n.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym2n.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym2n where
--- a/src/sym3.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym3.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym3 where
--- a/src/sym3n.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym3n.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym3n where
--- a/src/sym4.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym4.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym4 where
--- a/src/sym5.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym5 where
--- a/src/sym5a.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5a.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 --
 -- checking does not terminate, sorry
 --
--- a/src/sym5h.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5h.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym5h where
--- a/src/sym5n.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5n.agda	Mon Sep 18 13:19:37 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible  #-}
 {-# OPTIONS --guardedness #-}
 
 open import Level hiding ( suc ; zero )