In what intensional type theories can absurdity be made definitionally proof irrelevant?

Question

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

Answer 1

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.

Answer 2

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.