For an example involving covert discontinuity, consider quantifier scope construal.  DL provides a uniform type assignment to generalized quantifier expressions such as ‘everyone’, ‘someone’: (s ↑ np) ↓ s.  In the syntactic source calculus, this type assignment allows a quantifier phrase QP to occupy any position that could be occupied by a regular non-quantificational noun phrase. Semantically, the image of the ↑ Introduction rule at the level of the semantic target calculus LP binds an np type hypothesis at the position that was occupied by the QP (the a − x : np premise, with a and x structural and semantic variables for the np hypothesis).  The image of the ↓ Elimination rule applies the term representing the QP meaning to this abstract.  Scope ambiguities arise from derivational ambiguity in the source calculus DL. The derivation below results in a non-local reading ‘there is a particular x such that Mary thinks x left’.  Looking upward from the conclusion, the last rule applied is ↓ Elimination, which means the QP takes scope at the main clause level.  An alternative derivation, producing the local scope reading, would have the / Elimination rule for ‘thinks’: (np\s)/s as the last step.