Mercurial > hg > Members > kono > Proof > galois

comparison sym3.agda @ 88:405c1f727ffe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 28 Aug 2020 11:05:45 +0900
parents 32004c9a70b1
children d3da6e2c0d90
comparison
equal deleted inserted replaced
87:c68956f6c3ad 88:405c1f727ffe
33 p00 : (q : Fin 3) → (FL→perm ((# 0) :: ((# 0) :: ((# 0) :: f0))) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) 33 p00 : (q : Fin 3) → (FL→perm ((# 0) :: ((# 0) :: ((# 0) :: f0))) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
34 p00 zero = refl 34 p00 zero = refl
35 p00 (suc zero) = refl 35 p00 (suc zero) = refl
36 p00 (suc (suc zero)) = refl 36 p00 (suc (suc zero)) = refl
37 37
38 p1 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))
39
38 open _=p=_ 40 open _=p=_
39 41
40 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid 42 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
41 solved1 = {!!} 43 solved1 = {!!}