[Agda] Trying to use irrelevant arguments to get a nicer equality
for algebraic structures
Andrea Vezzosi
sanzhiyan at gmail.com
Sat Sep 25 00:34:22 CEST 2010
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/
>
>
More information about the Agda
mailing list