# Contents

## Idea

In type theory, a split context is a context $\Gamma \vert \Delta$, where the judgments in $\Gamma$ are required to be separated from the judgments in $\Delta$, so that while it is possible for those in $\Delta$ to depend on those in $\Gamma$, the judgments in $\Gamma$ are not allowed to depend on the judgments in $\Delta$.

Split contexts are frequently used in modal type theories such as spatial type theory and cohesive homotopy type theory in order to make comonadic modalities work. Specifically Shulman’s real-cohesive homotopy type theory and Riley’s linear homotopy type theory use split contexts.