Yes :) My interest in homotopy type theory is only auxiliary to my research. Designing dependent type systems in a way that balances tractability with expressiveness is a pretty hard thing to do. SMT solvers are nice because you can treat them as oracles and "see what happens". I'm not an expert on decision procedures, and I'd characterize myself more as a user of solvers than a developer of them, though of course once you get deep enough in, that line blurs.
