[Agda] Trying to use irrelevant arguments to get a nicer equality for algebraic structures

[Andreas Abel]

Did you get my recent message that I implemented irrelevant fields in  
records today? You could try this...

On Sep 24, 2010, at 3:38 PM, Andreas Abel wrote:

> Hi,
>
> I just pushed a patch that allows now irrelevant fields in records.   
> They work similar as discussed with Dan Doel on a recent thread.   
> Irrelevant fields cannot be projected, internally they have been  
> erased.
>
> One can define a projection into the Squash type manually, whether  
> Agda will do this for you in the future remains to be seen.  If in  
> practice this should emerge as a convenient way to work with  
> irrelevant fields, it might be added.
>
> This is all very experimental, the printing of irrelevant things is  
> still broken (there are dots all over the place).  Bug and  
> experience reports welcome.
>
> Andrea's example:
>
> {-# OPTIONS --universe-polymorphism #-}
> module AndreaVezzosi where
>
> data Squash {a} (A : Set a) : Set a where
> squash : .A -> Squash A
>
> open import Level
> open import Relation.Binary.PropositionalEquality
>
> module IrrRecord where
>
>  record SemiG : Set1 where
>   constructor _,_,_,_,_,_
>   field
>     M    : Set
>     unit : M
>     _+_  : M -> M -> M
>     .assoc     : ∀ {x y z} ->  x + (y + z) ≡ (x + y) + z
>     .leftUnit  : ∀ {x} -> unit + x ≡ x
>     .rightUnit : ∀ {x} -> x + unit ≡ x
>
>  dual : SemiG -> SemiG
>  dual (M , e , _+_ , assoc , leftUnit , rightUnit) =
>    M , e , (λ x y -> y + x) , sym assoc , rightUnit , leftUnit
>
>  -- note: needed to match, since projections assoc, rightUnit,  
> leftUnit are not available
>
>  dual∘dual≡id : ∀ {M} -> dual (dual M) ≡ M
>  dual∘dual≡id = refl
>
> Cheers,
> Andreas

On Sep 25, 2010, at 12:34 AM, Andrea Vezzosi wrote:

> On Fri, Sep 24, 2010 at 12:54 AM, Andreas Abel <andreas.abel at ifi.lmu.de 
> > wrote:
>> Hi Andrea,
>>
>> since records do not support irrelevant fields yet, I suggest to  
>> use data
>> instead:
>>
>>  data SemiG : Set1 where
>>    _,_,_ : (M     : Set) ->
>>            (_+_   : M -> M -> M) ->
>>            .(∀ {x y z} ->  x + (y + z) ≡ (x + y) + z) ->
>>            SemiG
>>
>>  dual : SemiG -> SemiG
>>  dual (M , _+_ , assoc) = M , (λ x y -> y + x) , sym assoc
>>
>>  dual∘dual≡id : ∀ {M} -> dual (dual M) ≡ M
>>  dual∘dual≡id {_ , _ , _} = refl
>
> this doesn't help much because now we don't have eta expansion on
> SemiG, so "dual (dual M)" and "M" are still not obviously equal.
> I should have explained that the intent is to avoid the need to use
> coercions like dual∘dual≡id explicitly.
> Another example is if one has a definition of functors in a similar
> style, then "(F . G) . H" and "F . (G . H)" won't normalize to the
> same term (with F G and H being variables) so composing natural
> transformations gets akward.
>
>> Cheers,
>> Andreas
>>
>> On Sep 23, 2010, at 5:58 PM, Andrea Vezzosi wrote:
>>
>>>
>>> {-# OPTIONS --universe-polymorphism #-}
>>> module Monoid where
>>>
>>> data Squash {a} (A : Set a) : Set a where
>>>  squash : .A -> Squash A
>>>
>>> open import Relation.Binary.PropositionalEquality
>>>
>>> record SemiG : Set1 where
>>>  constructor _,_,_
>>>  field
>>>   M : Set
>>>   _+_ : M -> M -> M
>>>   assoc : Squash (∀ {x y z} ->  x + (y + z) ≡ (x + y) + z)
>>>
>>>
>>>
>>> dual : SemiG -> SemiG
>>> dual (M , _+_ , assoc) = M , (λ x y -> y + x) , lemma where
>>>    lemma : Squash ({x y z : M} → (z + y) + x ≡ z + (y + x))
>>>    lemma with assoc
>>>    lemma | squash y = squash (\ {_} {_} {_} -> sym y)
>>>
>>>
>>> dual∘dual≡id : ∀ {M} -> dual (dual M) ≡ M
>>> dual∘dual≡id {_ , _ , squash _} = refl

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/