[Agda] commutativity/associativity representation

[Nils Anders Danielsson]

On 2011-02-10 14:04, Permjacov Evgeniy wrote:
> 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.

If you rewrite the code as follows, then you'll see that it's the A
argument of _⟦_⟧_ which isn't inferred:

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

This type is entirely unconstrained, so Agda cannot figure it out for
you. You can fix the problem by giving the type explicitly, for instance
as follows:

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

-- 
/NAD