# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1694788603 -32400
# Node ID 12fe7875133132cee8cadf2a39ad20138fec46bd
# Parent  e6e8fc55b1bf2649eea1153d88aa0ed000063526
...

diff -r e6e8fc55b1bf -r 12fe78751331 src/sym5h.agda
--- a/src/sym5h.agda	Fri Sep 15 22:00:32 2023 +0900
+++ b/src/sym5h.agda	Fri Sep 15 23:36:43 2023 +0900
@@ -148,9 +148,9 @@
               aec : Permutation 5 5
               aec = ?
               Cdba : deriving (Symmetric 5) i ?
-              Cdba = Pcomm _ {dba} {?} i ?
+              Cdba = Pcomm _ {pprep (pprep abc)} {?} i ?
               Caec : deriving (Symmetric 5) i ?
-              Caec = Pcomm _ {aec} {?} i ?
+              Caec = Pcomm _ {pinv (pprep (pprep abc))} {?} i ?
               s18 :  iCommutator (Symmetric 5) (suc i) (pprep (pprep abc))
               s18 = iunit (ccong ? ( comm Cdba Caec ))
            s17 : (abc : Permutation 3 3 ) →  s15 (s16 abc) =p= abc