[Agda] commutativity/associativity representation

[Dominique Devriese]

Permjacov,

2011/2/10 Nils Anders Danielsson <nad at chalmers.se>:
> 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

Note by the way that without Nils' type restrictions on a and b (that
they be of TF A for a single A), your definition is non-sensical,
since the type of a ⟦ op ⟧ b is not necessarily the same as that of b
⟦ op ⟧ a, so in that case, the proof type of the equality does not
exist and your definition is non-sensical. I think you could first
require that the types be identical and then use a form of casting, as
follows:

cast : {ℓ : Level} → {A : Set ℓ} → {B : Set ℓ} → A ≡ B → A → B
cast refl v = v

f₁commutative : ∀ {ℓ} {TF : Set ℓ → Set ℓ} → op₂f₁ {ℓ} TF → Set (suc ℓ)
f₁commutative {ℓ} {TF} op = ∀ {A} {B} {a : TF A} {b : TF B} →
              Σ[ res-comm ∶ TF (op₂f₁.result op B A) ≡ TF
(op₂f₁.result op A B) ]
              a ⟦ op ⟧ b ≡ cast res-comm (b ⟦ op ⟧ a)

but that doesn't seem so clean. Maybe you should recheck that your
op2f1 definition really does what you want it to. Shouldn't TF be TF :
Type -> Set l for Type some type universe?

Dominique