A coherent sequent is an implication between coherent formulas in a common context. Its semantics is inclusion of the two interpreted subobjects of that context. The context is universally quantified outside the formulas.
New to topics? Read the docs here!