[Agda] Stymied by a proof irrelevance requirement

[Wolfram Kahl]

On Mon, Apr 01, 2013 at 05:09:04PM -0400, Jacques Carette wrote:
> [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?

I made it even more precise...  ;-)

You need a dependent variant of cong₂ that is ``missing'' from
Relation.Binary.PropositionalEquality:

=============
module Sing where

open import Level
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 >

cong₂D  :  {a b c : Level} {A : Set a} {B : A → Set b} {C : Set c} (f : (x : A) → B x → C)
          →  {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂}
          →  (x₁≡x₂ : x₁ ≡ x₂) → y₁ ≡ subst B (sym x₁≡x₂) y₂ → f x₁ y₁ ≡ f x₂ y₂
cong₂D f refl refl = refl

irr : singleton {_} {A} {b} {a} p ≡ singleton {_} {A} {b} {c} (sym q)
irr = cong₂D {B = λ x → x ≡ b} (λ x e → singleton {_} {A} {b} {x} e) (trans p q) (proof-irrelevance p _)
=============

Wolfram