[Agda] Stymied by a proof irrelevance requirement

[Jacques Carette]

[Cut down example from something bigger]

open import Relation.Binary.PropositionalEquality

postulate
A : Set
a b c : A
p : a ≡ b
q : b ≡ c

data <_> {a : Level} {A : Set a} (x : A) : Set a where
singleton : {y : A} → y ≡ x -> < x >

irr : singleton {_} {A} {b} p ≡ singleton {_} {A} {b} (sym q)
irr = {!!}

=============

I made irr's type extra-precise, just to try to be helpful. Hints?

Jacques