A development of the quantum lambda calculus as a higher inductive type

The main file is HIT.v, while Monad.v contains some type classes, and MyNotations.v is adapted from AUGER_Notations.