Mercurial > hg > Members > kono > Proof > galois

annotate src/sym3.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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
331
ee6b8f4cbf4c safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 328
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
318
fff18d4a063b use stdlib-2.0 and safe-mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 255
diff changeset
2
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level hiding ( suc ; zero )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Algebra
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
5 module sym3 where
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Symmetric
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Data.Unit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Function
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Nullary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Data.Empty
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Data.Product
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import Gutil
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Putil
162
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
18 open import FLutil
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 open import Solvable using (solvable)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 open import Relation.Binary.PropositionalEquality hiding ( [_] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open import Data.Fin
121
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
23 open import Data.Fin.Permutation hiding (_∘ₚ_)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
24
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
25 infixr 200 _∘ₚ_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
26 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
27
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
29 sym3solvable : solvable (Symmetric 3)
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
30 solvable.dervied-length sym3solvable = 2
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
31 solvable.end sym3solvable x d = solved1 x d where
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
33 open import Data.List using ( List ; [] ; _∷_ )
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
34
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
35 open Solvable (Symmetric 3)
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
36
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
37 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
38 p0id = pleq _ _ refl
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
40 p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
41 p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
42 p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
43 p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
44 p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
45 p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
46 t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ []
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
47
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
48 t1 = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷ plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷ plist [ p5 , p1 ] ∷
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
49 plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷ plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷ plist [ p5 , p1 ] ∷
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
50 plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷ plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷ plist [ p5 , p2 ] ∷
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
51 plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷ plist [ p5 , p3 ] ∷
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
52 plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p4 ] ∷
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
53 plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p5 ] ∷
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
54 []
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
55
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
56 open _=p=_
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
57
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
58 stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
59 stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
60
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
61 open import logic
121
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
62
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
63 p33=4 : ( p3 ∘ₚ p3 ) =p= p4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
64 p33=4 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
66 p44=3 : ( p4 ∘ₚ p4 ) =p= p3
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
67 p44=3 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
69 p34=0 : ( p3 ∘ₚ p4 ) =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
70 p34=0 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
71
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
72 p43=0 : ( p4 ∘ₚ p3 ) =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
73 p43=0 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
74
123
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
75 com33 : [ p3 , p3 ] =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
76 com33 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
77
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
78 com44 : [ p4 , p4 ] =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
79 com44 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
80
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
81 com34 : [ p3 , p4 ] =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
82 com34 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
83
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
84 com43 : [ p4 , p3 ] =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
85 com43 = pleq _ _ refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
86
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
87
122
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 121
diff changeset
88 pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 121
diff changeset
89 pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 121
diff changeset
90
121
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
91 open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
92
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
93 st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) ]
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
94
121
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 120
diff changeset
95 st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
96 st02 g h with perm→FL g in ge | perm→FL h in he
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
97 ... | (zero :: (zero :: (zero :: f0))) | t = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
98 ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) =
124
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
99 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
100 ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) =
124
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
101 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
102 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) =
124
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
103 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
104 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) =
124
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
105 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
106 ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) =
124
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 123
diff changeset
107 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
108
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
109 ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
110 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
111 ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
112 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
113 ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 ))=
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
114 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
115 ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))=
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
116 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
117 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) =
162
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 125
diff changeset
118 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
119 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
120 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
121 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))=
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
122 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
123 ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
124 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
125 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
126 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
127 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
128 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
129 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (zero :: (zero :: f0 ))) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
130 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
131 ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
132 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
133 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
134 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
135 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
136 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
137 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (suc zero :: (zero :: f0 ))) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
138 case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
139 ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
140 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
141 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
142 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
143 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
144 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
145 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 ))) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
146 case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
328
e9de2bfef88d fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
147 ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 )) =
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
148 case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
149
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
150 stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
331
ee6b8f4cbf4c safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 328
diff changeset
151 stage12 x (comm {g} {h} x1 y1 eq ) = st02 g h
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
152
70
32004c9a70b1 sym2 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
153 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
331
ee6b8f4cbf4c safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 328
diff changeset
154 solved1 _ (comm {g} {h} x y eq) with stage12 g x | stage12 h y
125
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
155 ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
156 ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
157 ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g)
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
158 ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com33 q) }
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
159 ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com44 q) }
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
160 ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com34 q) }
11ccc9fe91c3 sym3 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 124
diff changeset
161 ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com43 q) }
123
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 122
diff changeset
162