Simple type theory: equational axioms validated by biCartesian closed categories In this question, we consider only type theories with no ground types and no function symbols.
I want to know whether there exists a model of simple type theory with finite products, finite coproducts, and exponentials which is not a Heyting (pre)algebra, and validates some equational axioms peculiar to that model.
First, for simple type theory with finite products and finite coproducts, its models are categories with finite products and finite coproducts which are not necessarily distributive. (Here, “simple” means “neither polymorphic nor dependent”.) Lacking distributivity of finite products over finite coproducts, the elimination rules for $0$ and $+$ needs to be the following:
$$
\frac{\Gamma \vdash M : 0}{\Gamma \vdash \mathrm{elim}(M) : A}
\\
\frac{\Gamma \vdash M : A + B \hspace{20px} x : A \vdash N_1 : C \hspace{20px} y : B \vdash N_2 : C}{\Gamma \vdash \mathrm{case}(M, x. N_1, y. N_2) : C}
$$
Terms $N_1$ and $N_2$ cannot refer to variables in $\Gamma$.
There are two models for such type theory: the category Set of sets and (total) functions, and the category Pfn of sets and partial functions. The former is a distributive category and the latter is not.
Being distributive implies the second projection $A \times 0 \to 0$ is an isomorphism for any $A$.
Thus, considering equational theory of the type theory, we have an equational axiom:
$$
x : A \times 0 \vdash \mathrm{elim} (\mathrm{snd} (x)) = x : A \times 0
$$
where $\mathrm{elim}$ is an elimination form for $0$ and $\mathrm{snd}$ is the second projection,
which is validated by Set, but not by Pfn.
Now, we add exponentials to the type theory so that its models become BiCartesian Closed Categories (BiCCC). Since BiCCC is always a distributive category, we cannot reproduce the above discussion. (Also, Pfn is not a BiCCC.)
We can see that every Heyting (pre)algebra is a BiCCC, so we have an equational axiom like:
$$
x : A \times A \vdash \mathrm{fst} (x) = \mathrm{snd} (x) : A
$$
where $\mathrm{fst}$ is the first projection, because each Heyting (pre)algebra has Hom propositions rather than Hom sets when viewed as a category. Such an axiom is of course not valid in general models.
Then, my question is whether there exists a model (BiCCC) of simple type theory with finite products, finite coproducts, and exponentials which validates non-theorem equations between terms, and is not a Heyting (pre)algebra.
EDIT: Maybe I should have asked “is there any BiCCC relative to which the equational theory is incomplete with the proviso that it is not a Heyting (pre)algebra?”
 A: Thanks to @SridharRamesh, it turned out that no such model exists so I present a proof sketch. All mistakes are mine.
In the equational theory of our simple type theory, every type is isomorphic to a type of the form 1 + 1 + … + 1, which we call a finite copower. Then imposing a non-theorem equation on terms of any type amounts to imposing one on terms of a finite copower. Any non-theorem equation on a finite copower necessarily identifies 2 distinct inhabitants of that type.
In a model, identifying 2 distinct inhabitants of $\Sigma_n 1$, where $n \ge 3$, gives rise to identifying the 2 distinct inhabitants of 1 + 1, which in turn makes 1 and 1 + 1 isomorphic. So every object denoted by some type becomes isomorphic to 0 or 1, therefore(?) any model validating a non-theorem equation must be either $\{0 \le 1\}$ or $\{\star\}$, up to equivalence of categories.
EDIT: Although not interesting, I believe every full subcategory of Set whose objects are the empty set, the singleton set, an infinite set $X$, $X^X$, $X^{(X^X)}$, $(X^X)^X$, and so on is a BiCCC which is not a Heyting prealgebra.
