Mercurial > hg > Members > kono > Proof > galois

comparison src/sym2n.agda @ 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 e9de2bfef88d
children
comparison
equal deleted inserted replaced
330:1ff0b95e437f 331:ee6b8f4cbf4c
1 {-# OPTIONS --safe #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2 open import Level hiding ( suc ; zero ) 2 open import Level hiding ( suc ; zero )
3 open import Algebra
4 module sym2n where 3 module sym2n where
5 4
6 open import Symmetric 5 open import Symmetric
7 open import Data.Unit 6 open import Data.Unit
8 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
9 open import Function
10 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) 7 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
11 open import Relation.Nullary
12 open import Data.Empty
13 open import Data.Product
14 8
15 open import Gutil 9 open import Gutil
16 open import Putil 10 open import Putil
17 open import Solvable using (solvable) 11 open import Solvable using (solvable)
18 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
19 13
20 open import Data.Fin 14 open import Data.Fin
21 open import Data.Fin.Permutation hiding (_∘ₚ_) 15 open import Data.Fin.Permutation
22 16
23 infixr 200 _∘ₚ_ 17 open import FLutil
24 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_ 18 open import Data.List.Fresh
25 19 open import Data.List.Fresh.Relation.Unary.Any
20 open import FLComm
21 open import Data.List
26 22
27 sym2solvable : solvable (Symmetric 2) 23 sym2solvable : solvable (Symmetric 2)
28 solvable.dervied-length sym2solvable = 1 24 solvable.dervied-length sym2solvable = 1
29 solvable.end sym2solvable x d = solved1 x d where 25 solvable.end sym2solvable x d = solved1 x d where
30 26
31 open import Data.List using ( List ; [] ; _∷_ )
32
33 open Solvable (Symmetric 2) 27 open Solvable (Symmetric 2)
34 open import FLutil
35 open import Data.List.Fresh hiding ([_])
36 open import Relation.Nary using (⌊_⌋)
37 28
38 p0id : FL→perm ((# 0) :: ((# 0) :: f0)) =p= pid 29 p0id : FL→perm ((# 0) :: ((# 0) :: f0)) =p= pid
39 p0id = pleq _ _ refl 30 p0id = pleq _ _ refl
40
41 open import Data.List.Fresh.Relation.Unary.Any
42 open import FLComm
43 31
44 stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt) 32 stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt)
45 stage2FList = refl 33 stage2FList = refl
46 34
47 solved1 : (x : Permutation 2 2) → deriving 1 x → x =p= pid 35 solved1 : (x : Permutation 2 2) → deriving 1 x → x =p= pid