Maximality of -Equality with Finite Sums

Extend simply typed lambda calculus with finite product and finite sum types. Let $=_\beta$ be beta equality and let $=_{\beta\eta}$ be the equality induced by all interpretations in bicartesian closed categories. A typed congruence $\sim$ is typically ambiguous if $s\sim t:\sigma$ is preserved by every substitution of types for atomic types. Is $=_{\beta\eta}$ maximal among the consistent typically ambiguous congruences containing $=_\beta$? Equivalently, is every proper typically ambiguous extension of $=_{\beta\eta}$ inconsistent?