Strong eta-rules for functions on sum types

Question

I am wondering whether a rule like the following is consistent with decidable conversion and type-checking for dependent type theory:

$$ \frac{f\, g : (x:\mathsf{bool}) \to C~x\quad f~\mathsf{tt} \equiv g~\mathsf{tt} \quad f~\mathsf{ff} \equiv g~\mathsf{ff}}{f\equiv g} $$

That is, if two functions with domain $\mathsf{bool}$ agree definitionally on $\mathsf{tt}$ and $\mathsf{ff}$, then they are convertible. An analogous rule for functions on general inductive types like $\mathbb{N}$ is certainly bad, but it seems not too ridiculous to me to wonder whether the special case of $\mathsf{bool}$ (and other non-recursive inductive types, like sum-types and enumerated types) might be possible.

One thing that makes me somewhat hopeful is that this rule would make $(x:\mathsf{bool}) \to C~x$ behave very much like $C~\mathsf{tt} \times C~\mathsf{ff}$, and indeed be definitionally isomorphic to it if the latter also has an $\eta$-rule. Since such a rule for products is possible, I thought maybe it could also be possible for the function-type. And implementation-wise, I could imagine a bidirectional conversion-checking algorithm noticing when the type is a function with domain $\mathsf{bool}$ and deciding to apply this rule instead of the ordinary $\eta$-rule for functions.

Answer 1

If we have $\eta$ for functions and also your pointwise conversion rule, that implies the full $\eta$ rule for the (finite) domain type. When checking conversion of arbitrary $t,u$, we can abstract over an arbitrary $\mathsf{bool}$ subterm $v$ to get an equivalent conversion problem

$$(\lambda~(x:\mathsf{bool}).~ t')~v\equiv(\lambda~(x:\mathsf{bool}).~ u')~v$$

For instance

$$\mathsf{if}~b~\mathsf{then}~t~\mathsf{else}~t \equiv (\lambda~x.~\mathsf{if}~x~\mathsf{then}~t~\mathsf{else}~t)~b \equiv (\lambda~x.t)~b \equiv t$$

The full $\eta$-rules for finite sums are rather complicated and expensive to check. There's a reference for STLC with finite sums and products. However, I do not know any reference for deciding finite sum $\eta$ in richer systems.

I expect that $\eta$ for non-empty finite sums remains decidable even in the fully dependent type theories. $\eta$ for the empty type is decidable only when consistency of typing contexts is decidable.

More specifically for our current case, let's assume that $\bot \to A$ is definitionally irrelevant. Then, if we have $p : \bot$ and $t,~u : A$, then

$$t \equiv (\lambda~x.~t)~p \equiv (\lambda~x.~u)~p \equiv u$$

Therefore, if $\bot$ is provable then all terms are convertible. This is undecidable for the usual $\bot$ in type theories, but it might be decidable in other settings. For example, in ABCFHL cubical type theory all judgments hold when the empty cofibration is implied by the context. This is still decidable because cofibrations are decidable. This is implemented in cooltt.

Alternatively, we can drop the function $\eta$ rule. Then, we recover the finite product types as $(x : A) \to C~x$ for finite $A$, and everything is decidable. I don't think this configuration is useful for anything though.