22
$\begingroup$

Various type theories have, over the years, explored extending the definitional equality with a variety of eta-laws and various forms of proof irrelevance.

Quite a lot of systems manage eta for functions, because (as Thierry Coquand observed), you can eta-expand on a tit-for-tat basis, even if your equality test is not type directed. Whenever you are checking f = \ x -> t, you may readily test \ y -> f y = \ x -> t instead (choosing y fresh), if f is not already eta-expanded. Crucially, if neither side is already of the form \ x -> t, then eta-expansion makes no difference to the problem.

Agda certainly manages eta for records, because its equality is type-directed. Two records are equal exactly if they are equal fieldwise, which makes it a delight to define the unit type as the record type with no fields. (You can do syntactic eta-expansion tit-for-tat for pairs, but not for unit. For unit, if neither side is already canonical, eta-expansion makes a big difference to the problem!)

Are there any systems (in a good state of repair) which identify all terms in the empty type? That's a little trickier to manage, but I know some systems (because I built them) which did it. It's nice to have, because it means you can form the set of things which are not bad as dependent pairs of a thing and a proof that it's not bad: to prove that two such pairs are equal, you need only prove that the things are equal, because all inhabitants of Bad thing -> False are equal by eta for functions then falsity.

If you're working on a type theory for a proof assistant, have you got definitional equality for an absurd type? If so, I'd like to know (and I'm guessing Lean steps up, here). If not, what's stopping you? (I seem to remember that there was some sort of snag in Agda, but I can't for the life of me remember what it was.)

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ In Agda you can use at least either Prop or irrelevance. We discussed adopting it in the standard library but didn't because not everyone may be willing to rely on these features: github.com/agda/agda-stdlib/issues/645 $\endgroup$
    – gallais
    Commented Feb 24, 2022 at 13:37
  • 1
    $\begingroup$ Certainly non-trivial. My various readings around Chu and linear logic (see Shulman's various papers) makes me think that one could easily have systems where there is quite different evidence for being empty. In other words, my instinct is that justifying the opposite of what you wants is easier! So this could end up being UIP-like? $\endgroup$
    – Jacques Carette
    Commented Feb 24, 2022 at 13:45
  • 1
    $\begingroup$ There is a paper that addresses Normalization be Evaluation with coproducts. It achieves much more than irrelevant empty types: It can show that judgementally $f^3=f$ for any $f: 2 \to 2$, just by normalizing them! It does this by making a full eta-expansion rule for coproducts (which can include 0 without much effort), and deriving a NbE program for it. $\endgroup$
    – Trebor ♦
    Commented Feb 24, 2022 at 16:23
  • 1
    $\begingroup$ Welcome, Conor! $\endgroup$
    – Andrej Bauer
    Commented Feb 25, 2022 at 8:09

2 Answers 2

Reset to default
13
$\begingroup$

If you are happy to have your False live in a separate sort, then you can do this with strict propositions in Coq (and any other system that have those, which I guess includes quite a lot of them nowadays). Here is a small rough example:

Inductive False : SProp := .

Variable Bad : nat -> SProp.

Inductive ok_nat : Type :=
  | c (n : nat) (p : Bad n -> False) : ok_nat.

Variable (o1 o2 : Bad 0 -> False).

Goal (c 0 o1 = c 0 o2).
Proof.
  reflexivity.
Qed.
Improve this answer
$\endgroup$
8
$\begingroup$

I think the paper you're looking for is Definitional Proof Irrelevance Without K

(I seem to remember that there was some sort of snag in Agda, but I can't for the life of me remember what it was.)

Agda now has a proof-irrelevant predicative Prop, where if Ty : Prop then all members of Ty are definitionally equal. Indeed it's main use is showing that types are uninhabited, and the one example they show is a proof-irrelevant empty type.

In my few uses of Agda's Prop, the biggest snag is that there's no subtyping. So I had trouble with things where, I wanted to show that the product of two decidable types in Prop was decidable, which you can do, but it was a pain.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.