We use type-theoretic concepts to describe and prove properties of quantum computations, in particular those denoted by so-called quantum circuits. Our proposal combines several components, which are all represented using dependent and polymorphic types in Coq: lenses, finite functions, currying, polymorphism, and subtypes. Using these components, we provide a full account of pure quantum circuits, proving properties from the ground on.