3
$\begingroup$
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) = {!   !}
$\endgroup$

2 Answers 2

2
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$
    – gallais
    Mar 22, 2022 at 18:02
1
$\begingroup$

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

$\endgroup$
5
  • $\begingroup$ 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). $\endgroup$
    – Maya
    Feb 28, 2022 at 15:44
  • $\begingroup$ Please include a (brief) summary of the link in case it gets removed / modified. $\endgroup$ Feb 28, 2022 at 16:36
  • $\begingroup$ @NieDzejkob How should Agda decide whether a type has one inhabitant? Clearly it's undecidable. So would you recommend an ad hoc criterion? $\endgroup$
    – Trebor
    Feb 28, 2022 at 17:44
  • $\begingroup$ @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. $\endgroup$
    – Maya
    Feb 28, 2022 at 23:10
  • $\begingroup$ @NieDzejkob Well, that's how Agda's isProp works. It is located in the cubical prelude. $\endgroup$
    – Trebor
    Mar 1, 2022 at 1:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.