Redefine ⊥ to make its proofs irrelevant?

[gallais]

@tomjack has this definition of ⊥. It comes with a big advantage: because all
the proofs of a given Prop are definitionally equal, we get for free that all
proofs of a negative statement are equal (cf. unique).

{-# OPTIONS --prop #-}

open import Agda.Builtin.Equality

record Truth (P : Prop) : Set where
  constructor [_]
  field
    truth : P
open Truth public

data ⊥' : Prop where

⊥ = Truth ⊥'

¬ : Set → Set
¬ A = A → ⊥

unique : {A : Set} (x y : ¬ A) → x ≡ y
unique x y = refl

This would in particular allow us to change ≢-≟-identity's type from the
cumbersome ∀ {b} → a ≢ b → ∃ λ ¬eq → a ≟ b ≡ no ¬eq to the nicer
∀ {b} (¬eq : a ≢ b) → a ≟ b ≡ no ¬eq

[MatthewDaggitt]

Hmm interesting suggestion. The problem is that pattern matching on ⊥ is then results in [ () ] rather than () right?

Regardless of whether we adopt it or not, I'd prefer to hold off introducing it for a while until Prop has been in use for a bit. I'm sure there's probably not, but if there is a bug in the implementation then using it for the empty set seems the best possible way of breaking as much as the standard library as possible!

[gallais]

The problem is that pattern matching on ⊥ then results in [ () ] rather than () right?

Splitting a value of type ⊥ indeed yields [ truth ] rather than (). However ()
is accepted in 2.6.0 for a record with at least one absurd field so the change would
be backwards compatible.

Just like agda/agda#3533 improves case-splitting to take into account the fact that
Agda is now more clever, we could probably also get it to generate the expected ()
pattern.

[MatthewDaggitt]

If you think we can make it entirely backwards compatible then it definitely sounds worthwhile.

[gallais]

I am currently writing a patch to fix case splitting for this work. ;)

[nad]

One thing to consider is that some people might not want to use all features that Agda has to offer. If someone wants to work in the fragment of Agda that does not include Prop, then this change would presumably make large parts of the standard library useless.

[MatthewDaggitt]

I think @nad is probably right about this one. At the very least, let's see how @JacquesCarette gets on using it in the category theory portion of the library first...

I'm going to close this for now but feel free to re-open in the future.

[JacquesCarette]

Hoping to work on that in May, the rest of April is kind of booked pretty solid.

[gallais]

Note that we can use irrelevance instead of Prop. But I suppose the same
reasoning applies: not everyone is willing to accept irrelevance.

private data empty : Set where

record ⊥ : Set where
  field .absurd : empty

[JacquesCarette]

I should comment that we abandoned using both Prop and irrelevance in the new library. Both seemed to cause various headaches, and not using them turned out to be not difficult. In fact, not using them was quite illustrative. In other words, it seems that "proof relevant Category Theory" works fine in MLTT.

[gallais]

Now that #1565 uses irrelevant arguments, is it time to revisit this question
and potentially opt for an irrelevant Data.Empty?

[JacquesCarette]

Note that I have not seen much use of Prop "out in the wild", so I don't know if it has in effect gotten much testing. What would be the advantages of making this change?

My bias: I've been thinking about linear logic and evidence-for-falsity, which work really (really!) well together. Agda's Set-based proofs are, to me, one of its really appealing features. If linearity ever makes it in too, then all sorts of fun stuff (see Edward Kmett's work on linear logic in Haskell) can be immediately ported. But that's serious "what if" reasoning.

[I'm all for revisiting the question; I'm just slightly leaning on the 'no' side at this point.]

[gallais]

Sorry I should have been clearer given the title of the issue: I'm proposing to use irrelevance
(that we now use widely for NonZero arguments), not Prop.

[JacquesCarette]

Ah. Well, my bias still holds, but I don't think I have active reasons to object. And it would be a coherent choice to make.

[MatthewDaggitt]

Hmm so are you proposing a) to update the definition of ⊥ to a record with an irrelevant field or b) mark all arguments of type ⊥ to be irrelevant?

I'd be more on board with b), as the number of such arguments is very low and it doesn't involve altering crucial definitions for reasons that would be non-obvious to users.

[gallais]

mark all arguments of type ⊥ to be irrelevant?

The use case is having proofs of negations be trivially equal to each other. In which case there is no
"argument of type ⊥": ⊥ is the return type of the function.

[JacquesCarette]

Note that I've been successfully nudged to the positive side of this by this code which is now smooth but used to need a postulate. [It goes all the way to Prop, but I think that irrelevance could have been enough.]

[jespercockx]

If all you want is a proof irrelevant empty type, then just a record type with an irrelevant field is indeed enough. (Though I am still a bit sad that Prop is hidden under a flag).

[MatthewDaggitt]

As long as it's well documented why the definition is a little odd then I'm not averse to making the change.