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

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) = {!   !}


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.

• More generally: for any decidable type, you can use recompute to recover a relevant value from an irrelevant one. Assuming EM is but one way to prove a type is decidable. Mar 22, 2022 at 18:02

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

• I am aware. Clearly, it would break the substitution property of equality if it was allowed in the general case. However, when the type in question is _≡_, there is at most one inhabitant (at least, assuming K), so this is not a concern. If the inference performed by thm is not valid, I'd like to see why (e.g. a model of Agda's type theory where it doesn't hold).
– Maya
Feb 28, 2022 at 15:44
• Please include a (brief) summary of the link in case it gets removed / modified. Feb 28, 2022 at 16:36
• @NieDzejkob How should Agda decide whether a type has one inhabitant? Clearly it's undecidable. So would you recommend an ad hoc criterion?
– Trebor
Feb 28, 2022 at 17:44
• @Trebor You could provide a proof that (a b : T) -> a == b. I'm not saying it should be accepted automatically, just that there should be a way to make it work.
– Maya
Feb 28, 2022 at 23:10
• @NieDzejkob Well, that's how Agda's isProp works. It is located in the cubical prelude.
– Trebor
Mar 1, 2022 at 1:34