[ refactor ] make contradiction and friends entirely definitionally proof-irrelevant

[jamesmckinna]

The inevitable breaking consequence of #2785 , designed as a 'cleaning of the stables'.
Cf. #2346 whose intention it follows.
Currently duplicates functionality from #2803 ; will tidy up once that is merged.

Downstream consequence:

• some uses of contradiction internally need eta-expansion (and this may be regarded as a UX failure...?)
• consequently, so too may some client uses of this definition elsewhere (but no others in stdlib that I can find)

TODO:

• revert all uses of contradiction-irr introduced as consequences of [ refactor ] weaken type of Relation.Nullary.Negation.Core.contradiction-irr #2785
• ...

Consider also:

• refactoring Relation.Nullary.Reflects to make its various arguments definitionally proof-irrelevant
• deprecating/removing Relation.Nullary.Negation.Core._¬-⊎_ in favour of contradiction₂, or else change its type as well; its one use in stdlib is inReflects, so could be refactored in any case via ¬-recompute and inlining...
• ...

[JacquesCarette]

perhaps don't roll in such pure, non-breaking style changes in to something breaking and make a separate (if tiny) PR?

[jamesmckinna]

Not a style change; it's yet another 'feature' of irrelevant function spaces: _$_ is no longer well-typed!

[JacquesCarette]

So do we need a new variant for _$_ that would be?

[jamesmckinna]

Thanks @JacquesCarette for the speedy feedback (on a DRAFT PR for v3.0!).

For most of your queries, eta-expansion is needed because there's no (contravariant) subtyping between .A → B and A → B.

As for the ones which seemingly contradict #2653 , see #2803 : don't use contradiction where simple application will do instead! (Ie use of negation sometimes happens in the minimal logic fragment, without needing ex falso at all)

[jamesmckinna]

It's still DRAFT, and in any case v3.0, but it'll need to wait for any dust to settle from #2797 #2803 and #2805 etc. before proceeding!

[jamesmckinna]

Reconsidering whether this is even worthwhile: logically it makes sense, but ergonomically, it's such a pain.

[JacquesCarette]

Reading this code, I get the same impression: ergonomically, agda's proof irrelevance leaves much to be desired. Is there any conclusion from here that can be up-streamed?

[jamesmckinna]

Reading this code, I get the same impression: ergonomically, agda's proof irrelevance leaves much to be desired. Is there any conclusion from here that can be up-streamed?

Perhaps, but in the interests of cleaning up my own cluttered brain, I'd probably rather punt this. I conjecture/suspect that much of the current effort being expended on modalities in Agda more generally might hint that the . modality may one day end up deprecated?

In any case, I think that I myself may have misconstrued how best to deploy these ideas (re: ¬-recompute and the Harrop fragment more generally): if we have an irrelevant negated argument in scope, and from which we wish to derive a contradiction, then it can be promoted via ¬-recompute and then appeal to contradiction.

Whereas, if we have an irrelevant positive assumption a : A, and seek a contradiction that and ¬ A, then... we already have contradiction-irr for that. We could insist on replacing each of contradiction and contradiction′ with these irrelevant versions, but then the UX problems bite again... whereas the current status quo gives us eta-contractible version of those functions, nevertheless with each being given by delegation to the irrelevant version...

... conclusion: closing for now.