
In categorical proof theory, propositions and proofs are presented as objects and arrows in a category. It thus embodies the strong constructivist paradigms of propositionsastypes and proofsasconstructions, which lie in the foundation of computational logic. Moreover, in the categorical setting, a third paradigm arises, not available elsewhere: logicaloperationsasadjunctions. It offers an answer to the notorious question of the equality of proofs. So we chase diagrams in algebra of proofs.