Mercurial > hg > Members > kono > Proof > galois

changeset 331:ee6b8f4cbf4c default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe mode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2024 16:48:09 +0900
parents 1ff0b95e437f
children
files src/Solvable.agda src/sym2.agda src/sym2n.agda src/sym3.agda src/sym3n.agda src/sym4.agda src/sym5.agda src/sym5h.agda src/sym5n.agda
diffstat 9 files changed, 59 insertions(+), 139 deletions(-) [+]
line wrap: on
line diff
--- a/src/Solvable.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/Solvable.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -23,6 +23,9 @@
 data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
   comm  : {g h i : Carrier} → P g → P h  → i ≈ [ g , h ] → Commutator P  i
 
+ccong : (P : Carrier → Set (Level.suc n ⊔ m)) {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
+ccong P {f} {g} f=g (comm {g1} {h} {i} pg  ph f=gh ) = comm pg ph (gtrans (gsym f=g) f=gh)
+
 deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
 deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
 deriving (suc i) x = Commutator (deriving i) x 
--- a/src/sym2.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym2.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -29,8 +29,6 @@
    open import Data.List using ( List ; [] ; _∷_ )
 
    open Solvable (Symmetric 2)
-   -- open Group (Symmetric 2) using (_⁻¹)
-
 
    p0 :  FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
    p0 = pleq _ _ refl
@@ -44,10 +42,6 @@
    p1r :  perm→FL (pswap pid) ≡  ((# 1) :: ((# 0 ) :: f0)) 
    p1r = refl
 
-   -- FL→iso : (fl : FL 2 )  → perm→FL ( FL→perm fl ) ≡ fl
-   -- FL→iso  (zero :: (zero :: f0)) = refl
-   -- FL→iso ((suc zero) :: (zero :: f0)) = refl
-
    open _=p=_
    open ≡-Reasoning
 
@@ -55,55 +49,34 @@
    --   because of Panic: uncaught pattern violation 
 
    sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-   sym2lem0 g h q with perm→FL g in g=00 | perm→FL h in h=00 
-   ... | s | t = ?
-
---  sym2lem0 g h q | zero :: (zero :: f0) | _ = begin
---            [ g , h ]  ⟨$⟩ʳ q
---          ≡⟨⟩
---             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
---          ≡⟨ cong (λ k → h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ  k))) ((peqˡ sym2lem1 _ )) ⟩
---             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) 
---          ≡⟨ cong (λ k →  h ⟨$⟩ʳ k ) (peq sym2lem1 _ )  ⟩
---             h ⟨$⟩ʳ  (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) 
---          ≡⟨⟩
---            [ pid , h ]  ⟨$⟩ʳ q
---          ≡⟨ peq (idcomtl h) q ⟩
---            q
---          ∎ where
---            sym2lem1 :  g =p= pid
---            sym2lem1 = FL-inject  g=00
---  sym2lem0 g h q | t | zero :: (zero :: f0) = begin
---            [ g , h ]  ⟨$⟩ʳ q
---          ≡⟨⟩
---             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
---          ≡⟨ peq sym2lem2 _   ⟩
---             pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
---          ≡⟨ cong (λ k → pid ⟨$⟩ʳ  (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩
---             pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
---          ≡⟨⟩
---            [ g , pid ]  ⟨$⟩ʳ q
---          ≡⟨ peq (idcomtr g) q ⟩
---            q
---          ∎ where
---            sym2lem2 :  h =p= pid
---            sym2lem2 = FL-inject h=00
---  sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = begin
---            [ g , h ]  ⟨$⟩ʳ q
---          ≡⟨⟩
---             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
---          ≡⟨ peq (psym g=h ) _  ⟩
---             g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
---          ≡⟨ cong (λ k →   g ⟨$⟩ʳ  (g ⟨$⟩ʳ  k) ) (peqˡ (psym g=h) _)  ⟩
---             g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
---          ≡⟨ cong (λ k → g  ⟨$⟩ʳ k) ( inverseʳ g )  ⟩
---             g ⟨$⟩ʳ  ( g ⟨$⟩ˡ q ) 
---          ≡⟨ inverseʳ g   ⟩
---            q
---          ∎ where
---             g=h :  g =p= h
---             g=h =  FL-inject (trans g=00 (sym h=00))
---  sym2lem0 g h q | s | t = ?
+   sym2lem0 g h q = s00 (perm→FL g) ( perm→FL h) refl refl  where
+       s00 : (pg : FL 2) (ph : FL 2 ) → pg ≡ perm→FL g → ph ≡ perm→FL h → [ g , h ]  ⟨$⟩ʳ q ≡ (pid ⟨$⟩ʳ q)
+       s00 (zero :: zero :: f0) _ ge he = begin
+            [ g , h ]  ⟨$⟩ʳ q ≡⟨⟩
+             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+                 ≡⟨ cong (λ k → h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ  k))) ((peqˡ {2} {g} {pid} (FL-inject (sym ge)) _ )) ⟩
+             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) ≡⟨ cong (λ k →  h ⟨$⟩ʳ k ) (peq {2} {g} {pid} (FL-inject (sym ge)) _ )  ⟩
+             h ⟨$⟩ʳ  (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) ≡⟨⟩
+            [ pid , h ]  ⟨$⟩ʳ q ≡⟨ peq (idcomtl h) q ⟩
+            q ∎ 
+       s00 (suc zero :: zero :: f0) (zero :: zero :: f0) ge he = begin
+            [ g , h ]  ⟨$⟩ʳ q ≡⟨⟩
+             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) ≡⟨ peq sym2lem2 _   ⟩
+             pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) ≡⟨ cong (λ k → pid ⟨$⟩ʳ  (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩
+             pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) ≡⟨⟩
+            [ g , pid ]  ⟨$⟩ʳ q ≡⟨ peq (idcomtr g) q ⟩
+            q ∎ where
+                sym2lem2 :  h =p= pid
+                sym2lem2 = FL-inject (sym he)
+       s00 (suc zero :: zero :: f0) (suc zero :: zero :: f0) ge he = begin
+            [ g , h ]  ⟨$⟩ʳ q ≡⟨⟩
+             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) ≡⟨ peq (psym g=h ) _  ⟩
+             g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) ≡⟨ cong (λ k →   g ⟨$⟩ʳ  (g ⟨$⟩ʳ  k) ) (peqˡ (psym g=h) _)  ⟩
+             g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) ≡⟨ cong (λ k → g  ⟨$⟩ʳ k) ( inverseʳ g )  ⟩
+             g ⟨$⟩ʳ  ( g ⟨$⟩ˡ q ) ≡⟨ inverseʳ g   ⟩
+            q ∎ where
+             g=h :  g =p= h
+             g=h =  FL-inject (trans (sym ge) he)
 
    solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
    solved x (comm {f} {g} _ _ eq ) = record { peq = cc }  where
@@ -113,17 +86,3 @@
              [ f , g ] ⟨$⟩ʳ q ≡⟨ sym2lem0 f g q ⟩
              q ∎ where open ≡-Reasoning
 
-   -- solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
---   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
---      cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
---      cc q = begin
---             x ⟨$⟩ʳ q
---          ≡⟨ sym (f=g q) ⟩
---             f ⟨$⟩ʳ q
---          ≡⟨ f=e q ⟩
---             q
---          ∎ where open ≡-Reasoning
--- 
-
-
-
--- a/src/sym2n.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym2n.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -1,16 +1,10 @@
-{-# OPTIONS  --safe #-}
+{-# OPTIONS --cubical-compatible  --safe #-}
 open import Level hiding ( suc ; zero )
-open import Algebra
 module sym2n where
 
 open import Symmetric 
 open import Data.Unit
-open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
-open import Function
 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
-open import Relation.Nullary
-open import Data.Empty
-open import Data.Product
 
 open import Gutil 
 open import Putil 
@@ -18,29 +12,23 @@
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
 open import Data.Fin
-open import Data.Fin.Permutation hiding (_∘ₚ_)
+open import Data.Fin.Permutation 
 
-infixr  200 _∘ₚ_
-_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
-
+open import FLutil
+open import Data.List.Fresh 
+open import Data.List.Fresh.Relation.Unary.Any
+open import FLComm
+open import Data.List 
 
 sym2solvable : solvable (Symmetric 2)
 solvable.dervied-length sym2solvable = 1
 solvable.end sym2solvable x d = solved1 x d where
 
-   open import Data.List using ( List ; [] ; _∷_ )
-
    open Solvable (Symmetric 2)
-   open import FLutil
-   open import Data.List.Fresh hiding ([_])
-   open import Relation.Nary using (⌊_⌋)
 
    p0id :  FL→perm ((# 0) :: ((# 0) :: f0)) =p= pid
    p0id = pleq _ _ refl
 
-   open import Data.List.Fresh.Relation.Unary.Any
-   open import FLComm
-
    stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt)
    stage2FList = refl
 
--- a/src/sym3.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym3.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS  --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -90,21 +90,11 @@
 
    open ≡-Reasoning
 
---   st01 : ( x y : Permutation 3 3) →   x =p= p3 →  y =p= p3 → x ∘ₚ  y =p= p4 
---   st01 x y s t = record { peq = λ q → ( begin
---         (x ∘ₚ y) ⟨$⟩ʳ q
---       ≡⟨ peq ( presp s t ) q ⟩
---          ( p3  ∘ₚ p3 ) ⟨$⟩ʳ q
---       ≡⟨ peq  p33=4 q  ⟩
---         p4 ⟨$⟩ʳ q
---       ∎ ) }
-
    st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm  ((suc (suc zero)) :: (suc zero) :: (zero :: f0))  ]
 
    st02 :  ( g h : Permutation 3 3) →  ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
    st02 g h with perm→FL g in ge | perm→FL h in he 
    ... | (zero :: (zero :: (zero :: f0))) | t = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
-   ... | s | (zero :: (zero :: (zero :: f0))) | se = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
    ... | (zero :: (suc zero) :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) =
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
    ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) = 
@@ -158,22 +148,10 @@
           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
    
    stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
-   stage12 x (comm {g} {h} x1 y1 ) = st02 g h
-   stage12 _ (ccong {y} x=y sx) with stage12 y sx
-   ... | case1 id = case1 ( ptrans (psym x=y ) id )
-   ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ ))
-   ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ ))
-
+   stage12 x (comm {g} {h} x1 y1 eq ) = st02 g h
 
    solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
-   solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d
-   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
-      cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q
-      cc q = begin
-             x ⟨$⟩ʳ q ≡⟨ sym (f=g q) ⟩
-             f ⟨$⟩ʳ q ≡⟨ f=e q ⟩
-             q ∎ 
-   solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
+   solved1 _ (comm {g} {h} x y eq) with stage12 g x | stage12 h y
    ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
    ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
    ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
--- a/src/sym3n.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym3n.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS  --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -6,12 +6,8 @@
 
 open import Symmetric 
 open import Data.Unit
-open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
 open import Function
 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
-open import Relation.Nullary
-open import Data.Empty
-open import Data.Product
 
 open import Gutil 
 open import Putil 
@@ -19,29 +15,24 @@
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
 open import Data.Fin
-open import Data.Fin.Permutation hiding (_∘ₚ_)
-
-infixr  200 _∘ₚ_
-_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
-
+open import Data.Fin.Permutation 
+open import Data.List 
+open import FLutil
+open import Data.List.Fresh 
+open import Relation.Nary 
+open import Data.List.Fresh.Relation.Unary.Any
+open import FLComm
 
 sym3solvable : solvable (Symmetric 3)
 solvable.dervied-length sym3solvable = 2
 solvable.end sym3solvable x d = solved1 x d where
 
-   open import Data.List using ( List ; [] ; _∷_ )
 
    open Solvable (Symmetric 3)
-   open import FLutil
-   open import Data.List.Fresh hiding ([_])
-   open import Relation.Nary using (⌊_⌋)
 
    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
    p0id = pleq _ _ refl
 
-   open import Data.List.Fresh.Relation.Unary.Any
-   open import FLComm
-
    stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt)
    stage3FList = refl
 
--- a/src/sym4.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym4.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -58,10 +58,8 @@
    stage3FList = refl
 
    st3 = proj₁ (toList ( CommFListN 4 2 ))
-   -- st4 = {!!}
  
    solved1 :  (x : Permutation 4 4) → deriving 3 x → x =p= pid 
    solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList p0id solved2 where
-      --    p0id :  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
       solved2 : Any (perm→FL x ≡_) ( CommFListN 4 3 )
       solved2 = CommStage→ 4 3 x dr 
--- a/src/sym5.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym5.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS  --safe #-}
+{-# OPTIONS --cubical-compatible  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -194,10 +194,10 @@
            →  deriving n f
            →  deriving n g
            → Commutator (deriving n) [ f , g ]
-     commd {n} f g df dg =  comm {deriving n} {f} {g} df dg
+     commd {n} f g df dg =  comm {deriving n} {f} {g} df dg prefl
 
      dervie-any-3rot0 0 i<3 j<4 = lift tt 
-     dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where
+     dervie-any-3rot0 (suc i) i<3 j<4 = ccong _  (psym ceq) (commd dba0 aec0 df dg )where
         tc = triple i<3 j<4
         dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
         aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
@@ -207,7 +207,7 @@
         dg =  dervie-any-3rot1 i  (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) 
 
      dervie-any-3rot1 0 i<3 j<4 = lift tt 
-     dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong {deriving n} ( psym ceq )  (commd aec0 abc0 df dg ) where
+     dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong _  ( psym ceq )  (commd aec0 abc0 df dg ) where
         tdba = dba-triple i<3 j<4
         aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))
         abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))
--- a/src/sym5h.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym5h.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS  --safe #-}
+{-# OPTIONS --cubical-compatible  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -101,9 +101,9 @@
            s12 : abc ≡ perm→FL [ dba , aec ]  
            s12 = refl
            s11 : FL→perm abc =p= [ dba , aec ]  
-           s11 = ptrans (pcong-Fp s12 ) ? -- (FL←iso _)
+           s11 = ptrans (pcong-Fp s12 ) ? -- (FL←iso _)    -- this takes a long time
            s17 : deriving  (suc i) ( FL→perm abc )
-           s17 = ccong (psym s11) (comm (Pcomm {_} {FL→perm dc} i (deriving-inv s10)) (Pcomm {_} {FL→perm be} i s10) )
+           s17 = ccong _ (psym s11) (comm (Pcomm {_} {FL→perm dc} i (deriving-inv s10)) (Pcomm {_} {FL→perm be} i s10) prefl )
 
 
      -- open Solvable ( Symmetric 5) 
--- a/src/sym5n.agda	Thu Oct 12 10:12:16 2023 +0900
+++ b/src/sym5n.agda	Mon Jul 08 16:48:09 2024 +0900
@@ -1,4 +1,7 @@
 {-# OPTIONS --guardedness #-}
+-- compile cannot use in safe
+-- {-# OPTIONS --cubical-compatible --safe #-}
+
 
 open import Level hiding ( suc ; zero )
 open import Algebra