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

[Andrea Vezzosi]

is there a way to define SemiG and dual such that dual∘dual≡id
typechecks without pattern matching on squash?

{-# 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