Mercurial > hg > Members > kono > Proof > galois

changeset 153:d880595eae30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FLinsert-mb
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 14 Sep 2020 15:12:32 +0900
parents be888cb9fe1b
children 61bfb2c5e03d
files FLutil.agda Putil.agda sym3n.agda sym4.agda
diffstat 4 files changed, 174 insertions(+), 71 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Sun Sep 13 10:54:42 2020 +0900
+++ b/FLutil.agda	Mon Sep 14 15:12:32 2020 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module FLutil where
 
 open import Level hiding ( suc ; zero )
@@ -6,7 +7,7 @@
 open import Data.Fin.Permutation
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 open import Relation.Binary.PropositionalEquality 
-open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
+open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
 open import Data.Product
 open import Relation.Nullary
 open import Data.Empty
@@ -132,10 +133,10 @@
 open import Relation.Nary using (⌊_⌋)
 open import Data.List.Fresh
 
-FList : {n : ℕ } → Set
-FList {n} = List# (FL n) ⌊ _f<?_ ⌋
+FList : (n : ℕ ) → Set
+FList n = List# (FL n) ⌊ _f<?_ ⌋
 
-fr1 : FList
+fr1 : FList 3
 fr1 =
    ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
    ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
@@ -158,7 +159,7 @@
 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
 -- ... | no nn = ⊥-elim ( nn x<a )
 
-ttf : {n : ℕ } {x a : FL (suc n)} → x f< a → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
+ttf : {n : ℕ } {x a : FL (suc n)} → x f< a → (y : FList (suc n)) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
 ttf _ [] fr = Level.lift tt
 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where 
        ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
@@ -166,19 +167,16 @@
 
 -- by https://gist.github.com/aristidb/1684202
 
-FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n} 
-FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList {suc n} ) → a f< x
+FLinsert : {n : ℕ } → FL n → FList n  → FList n 
+FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x
      → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
 FLinsert {zero} f0 y = f0 ∷# []
 FLinsert {suc n} x [] = x ∷# []
 FLinsert {suc n} x (cons a y x₁) with FLcmp x a
 ... | tri≈ ¬a b ¬c  = cons a y x₁
 ... | tri< lt ¬b ¬c  = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y  x₁) 
-FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt with FLinsert x [] | inspect ( FLinsert x ) []
-... | [] | ()
-... | cons a₁ t x₂ | e = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
-FLinsert {suc n} x (cons a y yr) |  tri> ¬a ¬b a<x =
-        cons a (FLinsert x y) (FLfresh a x y a<x yr )
+FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt  = cons a ( x  ∷# []  ) ( Level.lift (fromWitness lt) , Level.lift tt )
+FLinsert {suc n} x (cons a y yr)  | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr )
 
 FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt
 FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b
@@ -198,17 +196,31 @@
 -- open import Data.List.Fresh.Relation.Unary.All
 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
 
-Flist1 :  {n : ℕ } (i : ℕ) → i < suc n → FList {n} → FList {n} → FList {suc n} 
+Flist1 :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
 Flist1 zero i<n [] _ = []
 Flist1 zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
 Flist1 (suc i) (s≤s i<n) [] z  = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z 
 Flist1 (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )
 
-Flist : {n : ℕ } → FL n → FList {n}
+Flist : {n : ℕ } → FL n → FList n
 Flist {zero} f0 = f0 ∷# [] 
 Flist {suc n} (x :: y)  = Flist1 n a<sa (Flist y) (Flist y)   
 
-fr8 : FList {4}
+FLall1 : (n : ℕ ) → (x : FL (suc n)) → FList (suc n)
+FLall1 zero (zero :: f0) = (zero :: f0) ∷# []
+FLall1 (suc n) (x :: xp) = FLall2 ( FLall1 n xp ) where
+    FLall2 :  (z : FList (suc n)) → FList (suc (suc n))
+    FLall3 : (a : FL (suc n)) → (y : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y
+       → fresh (FL (suc (suc n))) ⌊ _f<?_ ⌋ (x :: a) (FLall2 y)
+    FLall2 [] = []
+    FLall2 (cons a y x₁) = cons (x :: a) (FLall2 y) (FLall3 a y x₁)
+    FLall3 a y x₁ = {!!}
+
+FLall : {n : ℕ } → FList n
+FLall {zero} = f0 ∷# []
+FLall {suc n} = FLall1 n fmax 
+
+fr8 : FList 4
 fr8 = Flist (fmax {4}) 
 
 -- FLinsert membership
@@ -221,5 +233,15 @@
   open import Data.List.Fresh.Membership.Setoid FL-Setoid
   open import Data.List.Fresh.Relation.Unary.Any 
 
-  FLinsert-mb :  (x : FL n ) → (xs : FList {n})  → x ∈ FLinsert x xs
-  FLinsert-mb x xs = {!!}
+  FLinsert-mb :  (x : FL n ) → (xs : FList n)  → x ∈ FLinsert x xs
+  FLinsert-mb x xs = fl1 {n} x xs where
+     fl1 : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
+     fl1 {zero} f0 [] = here refl
+     fl1 {zero} f0 (cons f0 xs x) = here refl
+     fl1 {suc n} x [] = here refl
+     fl1 {suc n} x (cons a xs x₁) with FLcmp x a
+     ... | tri< x<a ¬b ¬c = here refl
+     ... | tri≈ ¬a b ¬c   = here b
+     fl1 {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
+     fl1 {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( fl1 x (cons a₁ xs x₂) )
+
--- a/Putil.agda	Sun Sep 13 10:54:42 2020 +0900
+++ b/Putil.agda	Mon Sep 14 15:12:32 2020 +0900
@@ -13,7 +13,7 @@
 open import Function.Equality using (Π)
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 open import Data.Nat.Properties -- using (<-trans)
-open import Relation.Binary.PropositionalEquality 
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
 open import nat
 
@@ -424,50 +424,6 @@
    pswap-dist1 (suc zero) = refl
    pswap-dist1 (suc (suc q)) =  cong ( λ k → suc (suc k) ) refl
 
-infixr  100 _::_
-
-data  FL : (n : ℕ )→ Set where
-   f0 :  FL 0 
-   _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
-
-data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
-   f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
-   f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )
-
-_f≤_ : {n : ℕ } (x : FL n ) (y : FL n)  → Set
-_f≤_ x y = (x ≡ y ) ∨  (x f< y )
-
-FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n}  → xn :: x ≡ yn :: y → ( xn ≡ yn ) ∧ (x ≡ y )
-FLeq refl = record { proj1 = refl ; proj2  = refl }
-
-f<> :  {n : ℕ } {x : FL n } {y : FL n}  → x f< y → y f< x → ⊥
-f<> (f<n x) (f<n x₁) = nat-<> x x₁
-f<> (f<n x) (f<t lt2) = nat-≡< refl x
-f<> (f<t lt) (f<n x) = nat-≡< refl x
-f<> (f<t lt) (f<t lt2) = f<> lt lt2
-
-f-≡< :  {n : ℕ } {x : FL n } {y : FL n}  → x ≡ y → y f< x → ⊥
-f-≡< refl (f<n x) = nat-≡< refl x
-f-≡< refl (f<t lt) = f-≡< refl lt 
-
-FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n}  _≡_  _f<_
-FLcmp f0 f0 = tri≈ (λ ()) refl (λ ())
-FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn
-... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj1 (FLeq eq)) ) a) (λ lt  → f<> lt (f<n a) )
-... | tri> ¬a ¬b c = tri> (λ lt  → f<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj1 (FLeq eq)) )) c) (f<n c)
-... | tri≈ ¬a refl ¬c with FLcmp xt yt
-... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj2 (FLeq eq) )) (λ lt  → f<> lt (f<t a) )
-... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt )  refl (λ lt → f-≡< refl lt )
-... | tri> ¬a₁ ¬b c = tri> (λ lt  → f<> lt (f<t c) ) (λ eq → ¬b (proj2 (FLeq eq) )) (f<t c)
-
-infixr 250 _f<?_
-
-_f<?_ : {n  : ℕ} → (x y : FL n ) → Dec (x f< y )
-x f<? y with FLcmp x y
-... | tri< a ¬b ¬c = yes a
-... | tri≈ ¬a refl ¬c = no ( ¬a )
-... | tri> ¬a ¬b c = no ( ¬a )
-
 shlem→ : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
 shlem→ perm p0=0 x px=0 = begin
           x                                  ≡⟨ sym ( inverseʳ perm ) ⟩
@@ -595,6 +551,8 @@
         p003 : suc px ≡ suc py → px ≡ py
         p003 refl = refl
 
+open import FLutil
+
 FL→perm   : {n : ℕ }  → FL n → Permutation n n 
 FL→perm f0 = pid
 FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sym3n.agda	Mon Sep 14 15:12:32 2020 +0900
@@ -0,0 +1,119 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module sym3n 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 
+open import Solvable using (solvable)
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+open import Data.Fin
+open import Data.Fin.Permutation hiding (_∘ₚ_)
+
+infixr  200 _∘ₚ_
+_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
+
+
+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
+
+   t1  : FList 3 →  FList 3
+   t1  x =  tl2 x x [] where
+       tl3 : (FL 3) → ( z : FList 3) → FList 3 → FList 3
+       tl3 h [] w = w
+       tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
+       tl2 : ( x z : FList 3) → FList 3 →  FList 3
+       tl2 [] _ x = x
+       tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
+
+   stage10  :  FList 3
+   stage10  =  t1 (Flist (fmax ))
+
+   p0 =  FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) 
+   p1 =  FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) 
+   p2 =  FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) 
+   p3 =  FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) 
+   p4 =  FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) 
+   p5 =  FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) 
+   t0  =  plist p0 ∷ plist p1 ∷  plist p2 ∷ plist p3 ∷ plist p4 ∷  plist p5 ∷ [] 
+
+   tt4  = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷  plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷  plist [ p5 , p1 ] ∷ 
+          plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷  plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷  plist [ p5 , p1 ] ∷ 
+          plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷  plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷  plist [ p5 , p2 ] ∷ 
+          plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷  plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷  plist [ p5 , p3 ] ∷ 
+          plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷  plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p4 ] ∷ 
+          plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷  plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷  plist [ p5 , p5 ] ∷ 
+          []
+
+   open _=p=_
+   
+   stage1 :  (x : Permutation 3 3) →  Set (Level.suc Level.zero)
+   stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤)  x 
+
+   open import logic
+
+   pFL : ( g : Permutation 3 3) → { x : FL 3 } →  perm→FL g ≡ x → g =p=  FL→perm x
+   pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl ) 
+
+   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))  ]
+
+   
+   stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
+   stage12 = {!!}
+
+
+   solved1 :  (x : Permutation 3 3) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
+   solved1 _ uni = prefl
+   solved1 x (gen {f} {g} d d₁) with solved1 f d | solved1 g d₁
+   ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
+      genlem : ( q : Fin 3 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
+      genlem q = begin
+             g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
+          ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
+             f ⟨$⟩ʳ q 
+          ≡⟨ f=e q ⟩
+             q
+          ∎ 
+   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) = {!!}
+
--- a/sym4.agda	Sun Sep 13 10:54:42 2020 +0900
+++ b/sym4.agda	Mon Sep 14 15:12:32 2020 +0900
@@ -63,6 +63,10 @@
    k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ []
    k3 = plist  (a1  ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3)  ∷ plist (a2 ∘ₚ a1 ) ∷  []
 
+   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
 
@@ -83,17 +87,17 @@
    t0  =  plist (FL→perm p0 ) ∷ plist (FL→perm p1 ) ∷  plist (FL→perm p2 ) ∷ plist (FL→perm p3 ) ∷ plist (FL→perm p4 ) ∷  plist (FL→perm p5 ) ∷ 
           plist (FL→perm p6 ) ∷ plist (FL→perm p7 ) ∷  plist (FL→perm p8 ) ∷ plist (FL→perm p9 ) ∷ plist (FL→perm pa ) ∷  plist (FL→perm pb ) ∷ []
 
-   t1  : List (FL 4) →  List (FL 4) 
+   t1  : FList 4 →  FList 4
    t1  x =  tl2 x x [] where
-       tl3 : (FL 4) → ( z : List (FL 4)) → List (FL 4) → List (FL 4)
+       tl3 : (FL 4) → ( z : FList 4) → FList 4 → FList 4
        tl3 h [] w = w
-       tl3 h (x ∷ z) w = tl3 h z (( perm→FL [ FL→perm h , FL→perm x ] ) ∷ w )
-       tl2 : ( x z : List (FL 4)) → List (FL 4) →  List (FL 4)
+       tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
+       tl2 : ( x z : FList 4) → FList 4 →  FList 4
        tl2 [] _ x = x
-       tl2 (h ∷ x) z w = tl2 x z (tl3 h z w)
+       tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
 
-   stage1  :  List (FL 4)
-   stage1  =  t1 ( ∀-FL 3 ) 
+   stage1  :  FList 4
+   stage1  =  t1 (Flist (fmax ))
 
    -- stage2 ( Kline )
    --  k0  p0  zero :: zero :: zero :: zero :: f0 ∷                                   (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ∷
@@ -103,8 +107,8 @@
 
    tb = plist ( FL→perm p0) ∷ plist ( FL→perm p3) ∷ plist ( FL→perm p8) ∷ plist ( FL→perm pb) ∷ []
 
-   stage2  :   List (FL 4)
-   stage2   =  t1 ( p0 ∷ p1 ∷ p2 ∷ p3 ∷ p4 ∷ p5 ∷ p6 ∷ p7 ∷ p8 ∷ p9 ∷ pa ∷ pb ∷ [] ) 
+   stage2  :   FList 4
+   stage2   =  t1 (t1 (Flist (fmax ))) -- ( p0 ∷# p1 ∷# p2 ∷# p3 ∷# p4 ∷# p5 ∷# p6 ∷# p7 ∷# p8 ∷# p9 ∷# pa ∷# pb ∷# [] ) 
    
    solved1 :  (x : Permutation 4 4) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
    solved1 = {!!}