[Agda] Trying to use irrelevant arguments to get a nicer equality
for algebraic structures
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Sep 24 00:54:10 CEST 2010
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
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