  In this paper, we introduce dynamic lifting to a quantum circuit-description
language, following the Proto-Quipper language approach. Dynamic lifting allows
programs to transfer the result of measuring quantum data -- qubits -- into
classical data -- booleans -- . We propose a type system and an operational
semantics for the language and we state safety properties. Next, we introduce a
concrete categorical semantics for the proposed language, basing our approach
on a recent model from Rios\&Selinger for Proto-Quipper-M. Our approach is to
construct on top of a concrete category of circuits with measurements a Kleisli
category, capturing as a side effect the action of retrieving classical content
out of a quantum memory. We then show a soundness result for this semantics.
