Is the decision problem for the free bi-cartesian closed category (BCCC) decidable? Equivalently, is equality decidable for the simply-typed lambda calculus extended with strong n-ary products and sums? The decision problem for the free almost BCCC is decidable:
http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf
But this work does not include an initial object, or empty type in lambda-calulus terms, although they speculate their method can extend to BCCCs.
I will give a partial answer that will help illustrate why the initial object is being excluded. 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.
I've posted more details here. I can't answer it here, because the "Improperly formatted code" false positive bug in StackOverflow makes its interface broken beyond repair. (I get it even for an empty display window and there's no computer programming in my answer, since this isn't even a computer question!)
https://math.stackexchange.com/questions/4032422/decidability-of-bi-cartesian-closed-categories
