There are (at least) two different sort of things you can do, roughly corresponding to syntax and semantics.
You can study the internal logic of a category, which lets you use a logical language as a convenient tool for doing calculations with in a category. e.g. objects are types, propositions are subobjects, et cetera.
Conversely, given a suitable language, we can construct its syntactic category consisting of all the types you can construct in the language and the functions you can define between them, and satisfying all of the relations you can prove hold between them. And thus we can use category theory to help us think of type theories.
On the semantic side we can think of a category $T$ (possibly with extra structure; e.g. a sketch) as being a theory. Then models of this theory in a category $C$ will be functors $F : T \to C$ of a certain type.
Of course, these aren't unrelated; if we have the theory of a group, we might then construct $T$ to be its syntactic category, and require the functors defining models of $T$ to be of the sort that preserves the logic used.
Conversely, if we're in the habit of studying functors out of some category $T$, it may be worth considering the theory given by internal language of $T$ and view functors as being models of that theory.
A common type of this construction is one we can do with universal algebra (e.g. the theory of groups, given as operations and equations). If we have some variety of universal algebra, we can take $T$ to be the opposite category of the category of finitely presented algebras, and then models will be functors from $T$ that preserve finite limits.
The Wikipedia page on Cartesian closed categories has a subsection on bi-Cartesian closed categories which asserts that (1) the equational algebra cannot be axiomatized by a finite set of equational identities and (2) the word problem is still open. It cites the following reference, which should be worth a look
Remarks on Isomorphism for Typed Lambda Calculus with Coproducts
https://www.dicosmo.org/Papers/lics02.pdf
It is dated (2001) so it may be superseded by Ryan Wisnesky's link. If so, then the Wikipedia page needs to be updated. (Any volunteers, Ryan? :) )
A comment on "finite axiomatizability" - take this with a grain of salt because of an important detail that it leaves out. Kleene algebras, for instance, were proven by Conway in the 1960's to not be finitely axiomatizable by equational identities and this prematurely put a stop on the whole algebraization programme for formal language and automata theory ... on much the same way that Minsky's "no go" result put a premature stop on neural net research in the 1960's and 1970's. One of our colleagues revived the whole algebraization programme in the mid 1990's by showing that Kleene algebras are finitely axiomatizable - in terms of a small set of equational identities and one conditional equational identity (a least fixed point property).
Since then, the whole field of has taken off culminating in (among other things) the successful lifting of the algebraic framework of regular expressions to context-free expressions, as we've brought to completion the early attempt by Chomsky and Schuetzenberger in the early 1960's to algebraize the "type 2" tier in the Chomsky hierarchy, grandfathering in the older early 1970's formalism that was based on a fixed-point calculus formalism.
I expect that a similar result will emerge for bi-Cartesian closed categories and that one might be able to provide a small finite set of equational identities with a few conditional equational identities as an axiomatization.
As for embedding the "regular" objects of a bi-Cartesian closed category into Spencer-Brown's Laws of Form categorical algebra, the latter needs to be extended first, since it is (after all) only a groupoid, so it can't handle arrows that are not reversible. I conjecture that it suffices to just include the arrows for the terminal object, and that this should be enough to produce the other irreversible arrows.
Since we already have an extension of the Curry-Howard correspondence to classical logic - involving continuations - then it would be interesting to see how this can be related to Spencer-Brown's categorical algebra ... and also interesting to see whether and how it can be hybridized with a categorical algebra for bi-Cartesian closed categories.
Best Answer
We can define Boolean bicartesian closed categories : for each object $A$, the canonical morphism from A to its bidual is an isomorphism. Then we can prove that such categories are necessarily thin.
If you accept the product not to be Cartesian, then you can consider star-autonomous categories: there are such categories that are not thin.