[Agda] commutativity/associativity representation

[Permjacov Evgeniy]

On 02/10/2011 04:41 PM, Dominique Devriese wrote:
> 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
Yep. This restriction must be encoded as well, so I expect many plays
with associativity -) yet I'm a beginner, so [sarcasm mode] it will be
much fun [/sarcasm mode]

> , 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?
I'm afraid not.  So, the trick is very useful. Thanks.
> Dominique