Ways to think formally about Satisfiability Modulo Theories
It's actually surprisingly hard to relate SMT to type-theoretic/categorical approaches to logic -- the results in this area are very recent! This is because categorical logic is primarily conceived of as a semantics of proofs, and SMT arises from the model-theoretic view of logic, which is a semantics of provability. 

A formula in SMT is a boolean combination of primitive assertions over some theory. For example, for linear arithmetic you might have the following terms and primitive formulas.

$$
\newcommand{\bnfalt}{\;\;|\;\;}
\array{
\mbox{Terms} &amp; t &amp; ::= &amp; x \bnfalt n \bnfalt t + t \bnfalt -t \\
\mbox{Primitive Formulas} &amp; p &amp; ::= &amp; t \leq t \bnfalt t = t \bnfalt t &lt; t \\
\mbox{SMT Formulas} &amp; \phi &amp; ::= &amp; p \bnfalt \top \bnfalt \phi \land \phi' \bnfalt \lnot \phi \\
}$$

Given a formula $\phi$, an SMT solver will either give you a satisfying assignment for the variables -- i.e., it will give you a number for each variable, such that substituting that number for each variable gives you a true boolean formula -- or it will tell you that the formula $\phi$ is unsatisfiable.

The fact that this is all happening in classical logic is quite important; the architecture of SMT solvers relies upon this fact. Basically, SMT solvers are built as a combination of an DPLL-based SAT solver, which communicates with a theory solver, which deduces equalities from pure conjunctions of theory formulas. There are also various conditions under which you can combine solvers for different theories, which is important because it gives researchers a good "API" for figuring out if particular theories will fit together nicely. 

A good reference to the standard view of SMT is Clark Barrett and Cesare Tinelli's handbook chapter on Satisfiability Modulo Theories.  

Work on how to interpret SMT in terms of proof theory is much newer. The basic idea is to relate DPLL(T) with "focused" or "polarized" calculi for proof search. Focused calculi are variants of the sequent calculus originally designed to optimize proof search, but which turned out to work because they expose fundamental ideas in proof theory. 

Two good references to this are 
Mahfuza Farooque's PhD thesis, Automated reasoning techniques
as proof-search in sequent calculus, in which she relates the actions of a DPLL(T) algorithm to search in a particular focused calculus, and Stéphane Graham-Lengrand's habilitation thesis Polarities &amp; Focussing: a journey from Realisability to Automated Reasoning, in which he gives a broader perspective on this work (eg, by connecting it to work on biorthogonality).