I have a (hopefully) quick question about the interpretation of the Boolean type $\mathbf{2}$ (consisting of two objects $\mathbf{True}$ and $\mathbf{False}$) in a categorical model $\mathscr{C}$ of Martin-Löf dependent type theory. A natural guess to me is that this should be interpreted as the coproduct $$1\coprod 1$$ where $1$ denotes the terminal object in $\mathscr{C}$.
Is this correct?