  We propose a type-theoretic framework for describing and proving properties
of quantum computations, in particular those presented as quantum circuits. Our
proposal is based on an observation that, in the polymorphic type system of
Coq, currying on quantum states allows us to apply quantum gates directly
inside a complex circuit. By introducing a discrete notion of lens to control
this currying, we are further able to separate the combinatorics of the circuit
structure from the computational content of gates. We apply our development to
define quantum circuits recursively from the bottom up, and prove their
correctness compositionally.
