|
68
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
70
|
3 module sym3 where
|
|
68
|
4
|
|
|
5 open import Symmetric
|
|
|
6 open import Data.Unit
|
|
|
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
|
8 open import Function
|
|
|
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
|
|
|
10 open import Relation.Nullary
|
|
|
11 open import Data.Empty
|
|
|
12 open import Data.Product
|
|
|
13
|
|
|
14 open import Gutil
|
|
|
15 open import Putil
|
|
|
16 open import Solvable using (solvable)
|
|
|
17 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
18
|
|
|
19 open import Data.Fin
|
|
|
20 open import Data.Fin.Permutation
|
|
|
21
|
|
70
|
22 sym3solvable : solvable (Symmetric 3)
|
|
|
23 solvable.dervied-length sym3solvable = 2
|
|
|
24 solvable.end sym3solvable x d = solved1 x d where
|
|
68
|
25
|
|
70
|
26 open import Data.List using ( List ; [] ; _∷_ )
|
|
|
27
|
|
|
28 open Solvable (Symmetric 3)
|
|
68
|
29 -- open Group (Symmetric 2) using (_⁻¹)
|
|
|
30
|
|
70
|
31 p0 : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
|
|
|
32 p0 = record { peq = p00 } where
|
|
|
33 p00 : (q : Fin 3) → (FL→perm ((# 0) :: ((# 0) :: ((# 0) :: f0))) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
|
|
|
34 p00 zero = refl
|
|
|
35 p00 (suc zero) = refl
|
|
|
36 p00 (suc (suc zero)) = refl
|
|
68
|
37
|
|
70
|
38 open _=p=_
|
|
|
39
|
|
|
40 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
|
|
|
41 solved1 = {!!}
|
