Fractional (1.5) fixity for Relation.Nullary.¬_

[Saransh-cpp]

Fixes #1635

This PR adds a fractional (1.5) fixity for Relation.Nullary.¬_, discussed as a possible solution to the issue in the thread.

Following the experiment of @jamesmckinna, I decided to put ¬ at level 1.5, and it did break Data.Fin.Properties.¬∀⟶∃¬-smallest (similar to setting it to 2) and Data.List.Relation.Binary.Sublist.Setoid._⊂_ (I'm not sure why here, _×_ and ¬_ have different fixities).

Adding brackets - (¬ P i) and × (¬ (xs ≋ ys)) - worked and now ¬ is not at the same level as Σ and _×_. Using ¬ ∃[ A ] B without any brackets works for me, but it would be nice if someone could check this on their end too. I'd also be happy to close this PR if everyone decides not to add the fractional fixity.

[MatthewDaggitt]

@Saransh-cpp thanks for the PR! As this is a breaking change, we definitely need a CHANGELOG entry. Otherwise it looks good.

[gallais]

What's the reasoning behind this? It does not seem to be shedding any parens
and actually forces us to introduce more. Is there really a need for this change?

[Saransh-cpp]

After this PR, the users won't need parens with ¬ and ∃-syntax - ¬ ∃[ A ] B would work fine (parens are required right now - ¬ (∃[ A ] B) - should work the same for Σ-syntax as well).

But, changing the fixity of negation brings out some conflicts with ×'s fixity. Its like this PR fixes one parens problem, but adds another minor parens problem, and I am not sure how to deal with that. I'll be happy to make edits to the CHANGELOG or close this.

[MatthewDaggitt]

Thanks for raising it @gallais! Yup, given the discussion in #1635 I think the solution proposed there of adding special syntax for negated existentials is a better way of fixing of the problem.

Therefore I'm closing this PR. Thanks for exploring it @Saransh-cpp !