Definitional function extensionality for functions out of $\mathbf{2}$
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