Context in Type Theory

Question

I am reading a book on type theory. On page 105, the author says that

If one views valid contexts as theories (in the sense of ordinary logics) a consistent context corresponds to a consistent theory in the traditional sense.

Then the author gives the following definition:

Definition (Consistent Contexts) A valid context $\Gamma$ is consistent if and only if not very $\Gamma$-formula is provable in $\Gamma$, or equivalently, if and only if $\perp$ is not provable in $\Gamma$.

If I understand correctly, this implies that (a) not every context ($\Gamma$ : ctx) is consistent in type theory, and (b) if $\Gamma$ is consistent, then we won't be able to have both $x_1:A$ and $x_2:\neg A$ as assumptions, as they result in $\perp$?

Answer 1

(a) not every context $(Γ : \text{ctx})$ is consistent in type theory

Indeed, the context $x : \bot$ is inconsistent.

(b) if $\Gamma$ is consistent, then we won't be able to have both $x_1:A$ and $x_2:\neg A$ as assumptions, as they result in $\bot$

Yes, but this is just a trivial example. Inconsistencies can be sneakier. To level up, try to think of a context with 3 assumed propositions that is inconsistent, but removing any one of them results in a consistent context.