Bicartesian Coherence Revisited

TL;DR

This paper reviews and updates previous results on coherence in categories with finite products and coproducts, focusing on formalizing proof equality in classical and intuitionistic logic without distribution laws.

Contribution

It corrects, updates, and consolidates earlier results on coherence for categories modeling proof equality in conjunctive-disjunctive logic.

Findings

Corrected and refined formulations and proofs of coherence results.

Updated the scope of categories formalizing proof equality.

Clarified the logical assumptions underlying the categorical models.

Abstract

A survey is given of results about coherence for categories with finite products and coproducts. For these results, which were published previously by the authors in several places, some formulations and proofs are here corrected, and matters are updated. The categories investigated in this paper formalize equality of proofs in classical and intuitionistic conjunctive-disjunctive logic without distribution of conjunction over disjunction.