How do I make use of an irrelevant equality in a proof?

Question

open import Agda.Primitive
import Relation.Binary.PropositionalEquality as Eq
open Eq public
open Eq.≡-Reasoning

Suppose I have a dependent pair whose second element is irrelevant:

record ∃' {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,,_
  field
    fst : A
    .snd : B fst

open ∃' public

syntax ∃' A (λ x → B) = ∃'[ x ∈ A ] B
infix 2 ∃'
infixr 4 _,,_

Let's say I happen to use it on a subsingleton, such as _≡_:

module _ (X Y : Set) (f g : X → Y) where
  K : Set
  K = ∃'[ x ∈ X ] f x ≡ g x

How can I make use of this equality in a relevant context? For example, how can I prove this?

  thm : ∀ (k : K) → f (fst k) ≡ g (fst k)
  thm (x ,, eq) = {!   !}

Answer 1

You can turn an irrelevant proof into a relevant one if you assume excluded middle:

open import Axiom.ExcludedMiddle
open import Relation.Nullary
open import Data.Empty

postulate
  decide : ∀ {ℓ} → ExcludedMiddle ℓ

lift : ∀ {ℓ} {P : Set ℓ} → .P → P
lift {P = P} irr-p with decide {P = P}
...                | yes p = p
...                | no ¬p = ⊥-elim (⊥-lift (¬p irr-p))
  where
  ⊥-lift : .⊥ → ⊥
  ⊥-lift ()

Of course, if you use lift on a type with more than one inhabitant, one will be chosen arbitrarily — it won't recover the actual value of .P.

Answer 2

The Agda documentation says you can't use an irrelevant value in a relevant context.