Double negation translations in DTT

Stream: Type theory

[Horațiu Cheval]

In proof theory we have what is known as a double negation translation, or a negative translation, which assigns to each formula $A$ (of some first-order logic let's say) a formula $A^N$ such that $A$ and $A^N$ are classically equivalent and $A^N$ is intuitionistically (i.e. without excludded middle) provable whenever $A$ is classically provable. It is a way of removing excludded middle, in some sense. Is anyone aware of an analogous result for dependent type theory?

[Horațiu Cheval]

My reason for asking this is that if such a construction existed, I think carrying out this translation by metaprogramming and automatically producing an excludded middle-free proof for the translated proposition might constitute a very nice Lean project.

[Mario Carneiro]

I think it basically works just the same for pure MLTT. I am less sure about inductive types

[Horațiu Cheval]

Indeed, I imagine that if you only have product types etc. you can adapt it in a straightforward manner. General inductive types make me more curious

[Mario Carneiro]

Aha, here's a reference: Type‐Preserving CPS Translation of Σ and Π Types is Not Not Possible

[Mario Carneiro]

It's not as easy as I thought; the issue is that when you get to types that are not propositions like bool it is no longer classically equivalent to double negate them

[Mario Carneiro]

As I suspected, you need to use what amount to church encoding all the inductive types, but this has some issues in DTT because you have to add assumptions that the function obeys some parametricity properties ("free theorems"), and moreover this puts universe restrictions on the whole setup because you need a type quantifier \forall A : Type, (X -> A) -> A

[Mario Carneiro]

This answer goes into more detail on the issues that church encoding has in DTT

[Horațiu Cheval]

I'll check out those references, thank you!