\import Algebra.Group
\import Paths

\instance Aut {A : \1-Type} (a : A) : Group (a = a)
  | ide => idp
  | * => *>
  | ide-left {x} => idp_*> x
  | ide-right => idp
  | *-assoc {x} {y} {z} => *>-assoc x y z
  | inverse => inv
  | inverse-left {x} => inv_*> x
  | inverse-right {x} => *>_inv x