8
$\begingroup$

In Agda, irrelevance is an annotation which marks a parameter, record field, or definition which "will only be typechecked but never evaluated", with the consequence that irrelevant arguments and record fields are ignored when checking equality.

You can define records with irrelevant fields, e.g. this "Squash" type whose elements are definitionally equal:

record Squash {ℓ} (A : Set ℓ) : Set ℓ where
  constructor squash
  field
    .unsquash : A
open Squash

and these fields are counted in absurd patterns, e.g.

foo : Squash ⊥ → ⊥
foo ()

but by default the projection .unsquash : Squash A → A doesn't actually exist, meaning you can't directly use irrelevant fields, even in an irrelevant context!

There is an option --irrelevant-projections which adds irrelevant projections for irrelevant record fields, but it's incompatible with --safe. Being able to use an irrelevant field in an irrelevant context seems pretty innocuous, so why is --irrelevant-projections unsafe?

$\endgroup$
2
  • $\begingroup$ Hmm, are --irrelevant-projections related to type-in-type assumptions? If so, do you have any input on this question? $\endgroup$
    – user21820
    Apr 13 at 18:34
  • $\begingroup$ @user21820 Not that I know of. It is related to the axiom of choice, though, so it's unsafe because it's not constructive. $\endgroup$ Apr 15 at 14:58

1 Answer 1

8
$\begingroup$

--irrelevant-projections can be used to prove the irrelevance axiom mentioned in the Agda manual:

.irrAx : ∀ {ℓ} {A : Set ℓ} → .A → A
irrAx x = unsquash (squash x)

and conversely, irrelevant projections are justified by the irrelevance axiom:

.unsquash' : ∀ {ℓ} {A : Set ℓ} → Squash A → A
unsquash' (squash x) = irrAx x

Irrelevant projections and the irrelevance axiom do not compute (so e.g. unsquash (squash x) does not reduce to x). In a previous version of Agda, irrelevant projections computed, which made them inconsistent.

According to Jespr Cockx, although irrelevant projections are no longer inconsistent, the irrelevance axiom is still non-conservative and implies some form of non-constructive choice.

For example, this function looks like a formulation of the axiom of choice:

choice : ∀ {ℓ₁ ℓ₂} {X : Set ℓ₁} {Y : X → Set ℓ₂}
       → (∀ x → Squash (Y x)) → Squash (∀ x → Y x)
choice f = squash λ x → unsquash (f x)

The introduction of a non-conservative, non-constructive axiom which does not compute by necessity is, to the best of my knowledge, why --irrelevant-projections remains unsafe despite no longer being inconsistent.

See "Why does it matter if canonicity holds for irrelevant types?" for more information on the potential implications of an irrelevant non-constructive axiom.

Anyone interested in definitional proof-irrelevance may wish to consider using Prop instead, which can be used for the same purpose as irrelevance, but without so many caveats.

Some of the information in this answer has since been included in the Agda manual.

$\endgroup$
2
  • $\begingroup$ If a mathematician could check my conjecture about choice or an Agda developer could confirm that my reason is correct, then we could edit out the hedging and I'd feel more comfortable accepting my answer. $\endgroup$ Mar 4 at 22:31
  • 1
    $\begingroup$ If you read Squash as propositional truncation, then it is indeed equivalent to the axiom of choice. See e.g. page 155 of the HoTT book, lemma 3.8.2. In that scenario, it is actually too broad, too, because $X$ is not restricted to being a homotopy set. Here is a proof that irrelevant projections are inconsistent with cubical. $\endgroup$
    – Dan Doel
    Mar 7 at 19:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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