  Categorical Universal Logic is a theory of monad-relativised hyperdoctrines
(or fibred universal algebras), which in particular encompasses categorical
forms of both first-order and higher-order quantum logics as well as classical,
intuitionistic, and diverse substructural logics. Here we show there are those
dual adjunctions that have inherent hyperdoctrine structures in their predicate
functor parts. We systematically investigate into the categorical logics of
dual adjunctions by utilising Johnstone-Dimov-Tholen's duality-theoretic
framework. Our set-theoretical duality-based hyperdoctrines for quantum logic
have both universal and existential quantifiers (and higher-order structures),
giving rise to a universe of Takeuti-Ozawa's quantum sets via the
tripos-to-topos construction by Hyland-Johnstone-Pitts. The set-theoretical
hyperdoctrinal models of quantum logic, as well as all quantum hyperdoctrines
with cartesian base categories, turn out to give sound and complete semantics
for Faggian-Sambin's first-order quantum sequent calculus over cartesian type
theory; in addition, quantum hyperdoctrines with monoidal base categories are
sound and complete for the calculus over linear type theory. We finally
consider how to reconcile Birkhoff-von Neumann's quantum logic and
Abramsky-Coecke's categorical quantum mechanics (which is modernised quantum
logic as an antithesis to the traditional one) via categorical universal logic.
