Definitional function extensionality for functions out of $\mathbf{2}$

Question

Denote by $a$ and $b$ the canonical terms of $\mathbf{2}$.

For any map $f:\mathbf{2}\to \mathcal{U}$ we have the eliminator$$\mathrm{ind}_{\mathbf{2}}(f) : \big(f(a) \times f(b)\big) \to \prod_{x:\mathbf{2}} f(x).$$

Can we add the rule that for any $f:\mathbf{2}\to \mathcal{U}$ and any $g:\prod_{x:\mathbf{2}} f(x)$ we have a definitional equality $$g=\mathrm{ind}_{\mathbf{2}}(f)(g(a)\times g(b))$$and have decidable equality checking and decidable type checking?

So for example take $f=\lambda x:\mathbf{2}.\mathbf{2}$. Then this rule would imply a definitional equality $$\lambda x:\mathbf{2}.x=\mathrm{ind}_2(f)(b\times a)\circ \mathrm{ind}_2(f)(b\times a).$$

Answer 1

Yes, you can. However:

The complexity issue is bad -- testing whether two $2^n \to 2$ functions are equal is NP-complete, and to make it bearable in practice would require some clever integration with a SAT solver or BDD engine in the implementation of definitional equality.

Moreover, you can potentially defeat such smartness by asking questions about Boolean functions which are free variables. For example, for any $f : 2 \to 2$, it is extensionally the case that $f(f(f(x))) = f(x)$, which you establish by exhaustive enumeration.

You can find some links to papers with algorithms for coproduct in this link:

Programming languages with canonical functions