[Agda] commutativity/associativity representation

[Permjacov Evgeniy]

let assume following representation of binary operator defined on
indexed type family

record op₂f₁ {ℓ} (TF : Set ℓ → Set ℓ) : Set (suc ℓ) where
 field
   result : Set ℓ → Set ℓ → Set ℓ
   impl   : {A : Set ℓ} {B : Set ℓ} → TF A → TF B → TF (result A B)

and following sugar for it application

_⟦_⟧_ : ∀ {ℓ} {TF : Set ℓ → Set ℓ} {A B : Set ℓ} → TF A → (op : op₂f₁
TF) → TF B → TF (op₂f₁.result op A B)
a ⟦ op ⟧ b = op₂f₁.impl op a b

what term of what type will represent this operator's associativity and
commutativity ? this definition


f₁commutative : ∀ {ℓ} {TF : Set ℓ → Set ℓ} → op₂f₁ {ℓ} TF → Set ℓ
f₁commutative op = ∀ a b → a ⟦ op ⟧ b ≡ b ⟦ op ⟧ a

fails due unsolved meta.