On the proof-theoretic side, a cut-elimination theorem for a sequent presentation of DL establishes decidability. The DL sequent rules are shown to be sound with respect to the intended interpretation; a completeness result so far has not been obtained.  For the mapping from the syntactic source calculus DL to the semantic target calculus LP, the unary type-forming operations are considered inert: the inference rules for these connectives, consequently, leave no trace in the LP proof term associated with a derivation in the syntactic source calculus. The continuous and discontinuous families, for the rest, are treated exactly alike.  Specifically, the infixation and extraction operations are mapped to LP function types, like the slashes.