This is actually in reference to the question posed here
https://stackoverflow.com/posts/66285948/edit
but is more appropriate as a question to be posed on a non-coding site.
I provide a partial answer, but not the full answer, relaying the full question here as an unresolved question. Perhaps others can take the baton.
The question is: what decision procedures are there, for bi-cartesian closed categories? (A secondary question is: what normal order reduction strategies are there for them?)
The following observations will help illustrate why the initial object is being excluded in the reference cited in the original link. Things start to collapse when initial objects are combined with exponentials; or terminal objects with co-exponentials. This collapse becomes complete when both exponentials and co-exponentials are present; in which case, the decideability problem becomes trivial, reducing to provability in a logic, while the "normal form" reduction problem becomes more difficult – ironically.
In a category, an initial object $0$, terminal object $1$, product $A,B ↦ A×B$, co-product $A,B ↦ A+B$, exponential $A,B ↦ B^A$ and co-exponential $A,B ↦ A_B$ (if we may be excused in denoting it like so) correspond respectively to the constants & connectives in logic $⊥$ (false), $⊤$ (true), $A,B ↦ A∧B$ (and), $A,B ↦ A∨B$ (or), $A,B ↦ A⊃B$ (only if) and $A,B ↦ A⊂B$ (unless) (again: if we may be excused in denoting it this way).
This correspondence is made more precise in the following way: if the pre-order $A ≤ B ⇔ ∃f: A → B$ is defined on objects, and if objects are identified up to equivalence ($A ≡ B$ if and only if $A ≤ B$ and $B ≤ A$), then $⊤$, $⊥$, $∧$ and $∨$ are the lattice top, bottom, meet and join respectively, while $⊃$ and $⊂$ are respectively the implication and co-implication operators respectively of a Heyting and co-Heyting lattice.
If all of the following $\{ ∧, ⊃, ⊥ \}$ are present together then so is $⊤$, and then the category practically reduces to a logic. More precisely: it has a negation connective, defined up to equivalence by $¬A ≡ A ⊃ ⊥$ and the full subcategory of the regular objects (i.e. those objects $A$ for which $A$ and $¬¬A$ are equivalent) is a partial order and, in fact, reduces to a Boolean algebra (thus making all such equivalences as also isomorphisms).
That is, if $A$, $B$ are regular objects and $f: A → B$, and $f': A → B$, then $f = f'$; and such $f$ exists if and only if $A ≤ B$. Since $¬¬¬A$ and $¬A$ are isomorphic, then the regular objects comprise all the negations and the negative objects $¬A$ form a subcategory that is actually a Boolean logic.
A categorical algebra that includes either of the full sets of connectives $\{ ∧, ⊃, ⊥ \}$ or $\{ ∨, ⊂, ⊤ \}$ therefore contains a categorical algebra for Boolean algebra, itself, as a subalgebra. One such algebra was, in fact, given by Spencer-Brown in the "Laws of Form" though he did not recognize that it was a categorical algebra; since category theory was virtually unknown at the time and categorical algebras probably weren't even known of at all, at that time. Spencer-Brown actually defined a groupoid for Boolean algebra, not just a category, since his arrows were all reversible and were actually isomorphisms.
It can be described equivalently as a braided monoidal category, whose objects are strings, with the product operator $x,y ↦ xy$ is denoted by juxtaposition, the terminal object by the empty string $λ$. The category is endowed with an extra operator (denoted by circling the operand) which could be denoted here $x ↦ ❨x❩$. The isomorphisms he defined were Position $❨❨x❩x❩ ↔ λ$, Transposition $❨❨xz❩❨yz❩❩ ↔ ❨❨x❩❨y❩❩z$ and an implied isomorphism $xy ↔ yx$ for commutativity – which is already part of the definition for braided monoidal categories. It is coherent (only one morphism per arrow), and a decision procedure was given on Spencer-Brown's Laws of Form. The functor $x ↦ ❨x❩$ is more properly denoted an "anti-functor" since it maps the category to its reverse.
If Transposition is replaced by morphisms for Number $xx ↔ x$, Order $❨❨x❩❩ ↔ x$ and Ortho $❨xy❩❨y❩ ↔ ❨y❩$, then this suffices to characterize orthocomplemented lattices. I don't know how the procedure specified by Spencer-Brown can be adapted to this generalization. Nor am I even sure if it collapses to a coherent category.
The partial "collapse" can be seen directly as follows, where we'll consider the combination $\{ ∧, ⊃, ⊥ \}$ that combines exponentials and initial objects: Cartesian closed categories with initial objects.
Each connective can be defined equivalently as a functor on the category that comes equipped with a natural bijection that provides the categorical algebra for the connective and proof rules for the corresponding logic.
For the following, adopt the following conventions. For a category $𝐗$, let $|𝐗|$ denote its objects and for $A, B ∈ |𝐗|$, let $𝐗(A,B)$ denote the set of morphisms for the arrow $A → B$. Let $𝟭$ denote the unit category with $|𝟭| = \{0\}$ and $𝟭(0,0) = \{1_0\}$.
For a category $𝐗$, let $𝐗^+$ denote the reversal of category $𝐗$; where $|𝐗^+| = |𝐗|$ and for $A, B ∈ |𝐗^+|$,
$$𝐗^+(A,B) = \{ f ¦ A ← B: f \} = \{ f ¦ f: B → A \} = 𝐗(B,A);$$
composition defined in $𝐗^+$ as the reversal of composition in $𝐗$. Finally, for categories $𝐗$ and $𝐘$, let $𝐗×𝐘$ denote the direct their product; where $|𝐗×𝐘| = |𝐗|×|𝐘|$, and for $(A,A'), (B,B') ∈ |𝐗×𝐘|$,
$$𝐗×𝐘((A,A'),(B,B')) = 𝐗(A,B) × 𝐘(A',B'),$$
with composition defined componentwise.
If $𝐋$ is the category in question, then the functors include some or all of $⊤, ⊥: 𝟭 → 𝐋$; $∧, ∨: 𝐋×𝐋 → 𝐋$; $⊃:𝐋^+×𝐋 → 𝐋$; $⊂:𝐋×𝐋^+ → 𝐋$; and the natural bijections corresponding to each one are given, respectively, by
$$\begin{array}{lll}
C ∈ |𝐋^+| &↦ 𝐋(C,⊤) &⇔ 𝟭(0,0),\\
(A,B,C) ∈ |𝐋×𝐋×𝐋^+| &↦ 𝐋(C,A∧B) &⇔ 𝐋(C,A)×𝐋(C,B),\\
(A,B,C) ∈ |𝐋^+×𝐋×𝐋^+| &↦ 𝐋(C,A⊃B) &⇔ 𝐋(C∧A,B),\\
D ∈ |𝐋| &↦ 𝐋(⊤,D) &⇔ 𝟭(0,0),\\
(A,B,D) ∈ |𝐋×𝐋×𝐋| &↦ 𝐋(A∨B,D) &⇔ 𝐋(A,D)×𝐋(B,D),\\
(A,B,D) ∈ |𝐋^+×𝐋×𝐋| &↦ 𝐋(A⊂B,D) &⇔ 𝐋(A,B∨D).
\end{array}$$
In detail, for $∧$, $⊃$, $⊤$ and $⊥$, we can write them as
$$\begin{array}{ll}
\left(\left(\begin{align}f: C → A,\\g: C → B\end{align}\right) ⇔ h: C → A∧B\right) &⇒ \left(⟨f,g⟩ = h ⇔ \left(\begin{array}{ll}⊤h &= f,\\⊥h &= g\end{array}\right)\right),\\
(f: C∧A → B ⇔ h: C → A⊃B) &⇒ (⋀f = h ⇔ ⋁h = f),\\
f: C → ⊤ &⇔ f = ⟨⟩_C,\\
g: ⊥ → D &⇔ g = []_D,
\end{array}$$
(where I'm operator-overloading by also using $⊤$ and $⊥$ as prefix operators to denote the components of the reverse direction of the natural bijection for $∧$).
The last two conditions are where the "collapse" starts to take place.
In the cases of $⊤$ and $⊥$, "naturality" of the bijections is given by the conditions just stated above, while for $∧$, it is given equivalently by the conditions that
$$⊤(h∘m) = ⊤h∘m,\quad ⊥(h∘m) = ⊥h∘m,$$
where $m: C' → C$. So, we could just as well write $⊤h = ⊤1_{A∧B}∘h$ and $⊥h = ⊥1_{A∧B}∘h$ (taking $1_{A∧B}$ and $h$, respectively, in place of $h$ and $m$).
First, $⊥∧A ≤ B$ is always true and there is a unique $f: ⊥∧A → B$, since
$$f: ⊥∧A → B ⇔ ⋀f: ⊥ → A⊃B ⇔ ⋀f = []_{A⊃B} ⇔ f = ⋁[]_{A⊃B}.$$
Second, by this uniqueness, since
$$⊤1_{⊥∧A}: ⊥∧A → ⊥,\quad []_{⊥∧A}: ⊥ → ⊥∧A,$$
and thus
$$[]_{⊥∧A}∘⊤1_{⊥∧A}: ⊥∧A → ⊥∧A;$$
and since
$$1_{⊥∧A}: ⊥∧A → ⊥∧A,$$
then it follows that
$$[]_{⊥∧A}∘⊤1_{⊥∧A} = ⋁[]_{A⊃(⊥∧A)} = 1_{⊥∧A}.$$
Third, since
$$⊥1_{⊥∧A}: ⊥∧A → A,\quad []_{⊥∧A}: ⊥ → ⊥∧A,$$
then
$$⊥1_{⊥∧A}∘[]_{⊥∧A}: ⊥ → A$$
thus
$$⊥1_{⊥∧A}∘[]_{⊥∧A} = []_A.$$
Fourth, suppose $A ≤ ⊥$ and that $f: A → ⊥$. Then
$$\begin{array}{ll}
⊤1_{⊥∧A}∘⟨f,1_A⟩ &= ⊤(1_{⊥∧A}∘⟨f,1_A⟩) &= ⊤⟨f,1_A⟩ = f.\\
⊥1_{⊥∧A}∘⟨f,1_A⟩ &= ⊥(1_{⊥∧A}∘⟨f,1_A⟩) &= ⊥⟨f,1_A⟩ = 1_A.
\end{array}$$
Thus
$$\begin{align}
[]_A∘f
&= ⊥1_{⊥∧A}∘[]_{⊥∧A}∘⊤1_{⊥∧A}∘⟨f,1_A⟩\\
&= ⊥1_{⊥∧A}∘1_{⊥∧A}∘⟨f,1_A⟩\\
&= ⊥1_{⊥∧A}∘⟨f,1_A⟩\\
&= 1_A,
\end{align}$$
while $f∘[]_A: ⊥ → ⊥$ and $1_⊥: ⊥ → ⊥$ therefore $f∘[]_A = []_⊥ = 1_⊥$.
Therefore, $f = {([]_A)}^{-1}$, thus making the morphism $f: A → ⊥$ is unique.
When $A ≤ ¬B ≡ B ⊃ ⊥$, then there is a unique $f: A → ¬B$, since
$$f: A → ¬B = B ⊃ ⊥ ⇔ ⋁f: A∧B → ⊥ ⇔ ⋁f = {([]_{A∧B})}^{-1} ⇔ f = ⋀{([]_{A∧B})}^{-1}.$$
It is therefore also possible to define $⊤ ≡ ⊥ ⊃ ⊥$, thereby making the morphisms $f: A → ⊤$ unique, since
$$f: A → ⊤ = ⊥ ⊃ ⊥ ⇔ ⋁f: A∧⊥ → ⊥ ⇔ ⋁f = {[]_{A∧⊥}}^{-1} = ⊥1_{A∧⊥} ⇔ f = ⋀⊥1_{A∧⊥},$$
and we could therefore define $⟨⟩_A ≡ ⋀⊥1_{A∧⊥} = {[]_{A∧⊥}}^{-1}$. So, it is indeed a Cartesian closed category, as I alluded to above.
Best Answer
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.