Naming higher order associators and inverse laws

[fredrik-bakke]

Hey! So I'm looking to define second-order associators and inverse laws for identification and homotopy concatenation. Currently, I have the following definitions for inverse laws:

module _
  {l : Level} {A : UU l} {x y z : A}
  where

  right-right-inv : (p : x ＝ y) (q : y ＝ z) → (p ∙ q) ∙ inv q ＝ p
  right-right-inv p q = assoc p q (inv q) ∙ ap (p ∙_) (right-inv q) ∙ right-unit

  left-right-inv : (p : x ＝ y) (q : x ＝ y) → p ∙ (inv p ∙ q) ＝ q
  left-right-inv p q = inv (assoc p (inv p) q) ∙ ap (_∙ q) (right-inv p)

  right-left-inv : (p : x ＝ y) (q : z ＝ y) → (p ∙ inv q) ∙ q ＝ p
  right-left-inv p q = assoc p (inv q) q ∙ ap (p ∙_) (left-inv q) ∙ right-unit

  left-left-inv : (p : x ＝ y) (q : y ＝ z) → inv p ∙ (p ∙ q) ＝ q
  left-left-inv p q = inv (assoc (inv p) p q) ∙ ap (_∙ q) (left-inv p)

However, I recall that some opinions were floating about this naming scheme being bad, so I'm wondering what a better naming scheme would be. Likewise, I want to define the second-order associators, but again there's a question about how to name them. The following are the ones that are not just a single application of assoc:

module _
  {l : Level} {A : UU l} {x y z u v : A}
  (p : x ＝ y) (q : y ＝ z) (r : z ＝ u) (s : u ＝ v)
  where

  assoc?² : ((p ∙ q) ∙ r) ∙ s ＝ p ∙ ((q ∙ r) ∙ s)
  assoc?² = ap (_∙ s) (assoc p q r) ∙ assoc p (q ∙ r) s

  assoc??² : (p ∙ (q ∙ r)) ∙ s ＝ p ∙ (q ∙ (r ∙ s))
  assoc??² = assoc p (q ∙ r) s ∙ ap (p ∙_) (assoc q r s)

  assoc???² : ((p ∙ q) ∙ r) ∙ s ＝ p ∙ (q ∙ (r ∙ s))
  assoc???² = assoc (p ∙ q) r s ∙ assoc p q (r ∙ s)

  assoc????² : (p ∙ q) ∙ (r ∙ s) ＝ p ∙ ((q ∙ r) ∙ s)
  assoc????² = assoc p q (r ∙ s) ∙ ap (p ∙_) (inv (assoc q r s))

  assoc?????² : (p ∙ q) ∙ (r ∙ s) ＝ (p ∙ (q ∙ r)) ∙ s
  assoc?????² = inv (assoc (p ∙ q) r s) ∙ ap (_∙ s) (assoc p q r)