  The capture calculus is an extension of System F<: that tracks free variables
of terms in their type, allowing one to represent capabilities while limiting
their scope. While previous calculi had mechanized soundness proofs -- notably
System CF<: -- the latest version, namely the box calculus (System CC<:box),
only had a paper proof. We present here our work on mechanizing the theory of
the box calculus in Coq, and the challenges encountered along the way. While
doing so, we motivate the current design of capture calculus, in particular the
concept of boxes, from both user and metatheoretical standpoints. Our
mechanization is complete and available on GitHub.
