I want to show that the law of the excluded middle do not hold in a bicartesian closed category (BCCC), interpreted as follows:
In general, there need not be a morphism $1 \to A + 0^A$ for $A \in \text{Obj}(\mathcal{C})$ in a BCCC $\mathcal{C}$.
Well, this is obviously true, because we can see Heyting algebras as BCCCs (in fact, I guess they are indeed equivalent as categories). And if there exists one such a morphism for each object $A$, then each Heyting algebras would be a Boolean algebra.
But is there a more direct proof of this statement?