[ add/DRY ] Ex falso-type eliminator for irrelevant instances of irreflexive 'equality'

[jamesmckinna]

Having turned my focus to making certain relational arguments irrelevant in eg. Data.Fin.Base (#2783 #2790 cf. #2787 ), I observe a frequently-occurring pattern of reasoning, usually at the base case, where an 'irreflexive' argument of type 0 ≢ 0 ends up being eliminated via contradiction refl.

In order to make such arguments valid when such arguments are marked as irrelevant then requires such proofs to be modified, in-place, to use the new contradiction-irr introduced in #2785 .

This is all a bit annoying, esp. from a DRY point of view, when it seems as though we could add once and for all,

• ¬[x≢x] : ∀ {w} {Whatever : Set w} →.(x ≢ x) → Whatever in Relation.Binary.PropositionalEquality.Core, encapsulating the use of contradiction-irr in a single place
• (optional) ¬[x≉x] : ∀ {w} {Whatever : Set w} → .(x ≉ x) → Whatever in Relation.Binary.Properties.Setoid by delegation to the above, via reflexive

and hence replace all the existing contradiction refl-like arguments with appeals to ¬[x≢x] instead.

Cons:

• bikeshedding/Fairbairn threshold, trading off against DRY
• seems to go against the spirit, at least, of Prefer contradiction over ⊥-elim when it makes sense? #2653, by re-introducing an implicit appeal to ⊥-elim, esp. wrt the Whatever boilerplate...
• what else?

Pros:

• subtle/slight streamlining of the dependency graph wrt import of Relation.Nullary.Negation.Core
• slight/subtle improvement in the abstraction wrt proofs, esp. being agnostic wrt relevance/irrelevance
• what else?

Suggestions as to names might also be welcome ;-)

[JacquesCarette]

I quite like the ¬[x≢x] name.

I'm still not entirely convinced that we should spread irrelevance around. Conceptually, it is great. But in practice, those irrelevant proofs still contain information and not having access to that information when debugging is a huge pain (i.e. Agda prints irrelevant arguments as _). Just because it's unique, and Agda knows what it is (modulo a recomputation) doesn't mean that I know what it is. But that doesn't seem like a particular strong point.

In any case: if we make certain relational arguments irrelevant, then I think adding this function makes sense, as it better captures the pattern-of-reasoning than contradiction-irr refl does.

[jamesmckinna]

Thanks @JacquesCarette re: name.

Interesting re: exploiting irrelevance vs. cognitive load/information 'loss'. That suggests that an alternative to this proposal (and any use of it in #2783 #2790 etc.) might better be finessed via:

• OOPS the existing defining a property Relation.Binary.PropositionalEquality.Core.≢-irrefl by analogy with Relation.Binary.Setoid.Properties.≉-irrefl
• an explicit appeal to recompute for the equalities concerned

but I think that's perhaps too 'narrow' an approach given that ¬[x≢x] is directly definable.

Also useful to explicitly draw attention to potential sequencing of related PRs.

Good I didn't already raise a PR against this issue!

UPDATED: I have now, without any commitment to relevance/irrelevance at call-sites (subtyping wrt irrelevance works in our favour!)