constructive mathematics, realizability, computability propositions as types, proofs as programs, computational trinitarianism The “ZX-calculus” is an elaboration for the purpose of qbit-based quantum computation of the string diagram-calculus used in quantum information theory via dagger-compact categories. The basic idea is to formalize the co-existence of the ubiquitous pair of measurement bases of qbits , namely the “computational basis” which consists (by common convention) of the...