Agda-stdlib: Redefine Bottom to make use of Prop?

[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.