We investigate the universal fragment of intuitionistic logic focussing on equality of proofs. We give categorical models for that and prove several completeness results. One of them is a generalization of the well known Yoneda lemma and the other is an extension of Harvey Friedman's completeness result for typed lambda calculus.

We investigate the universal fragment of intuitionistic logic focussing on equality of proofs. We give categorical models for that and prove several completeness results. One of them is a generalization of the well known Yoneda lemma and the other is an extension of Harvey Friedman's completeness result for typed lambda calculus.

In categorical proof theory, propositions and proofs are presented as objects and arrows in a category. It thus embodies the strong constructivist paradigms of propositions-as-types and proofs-as-construtions, which lie in the foundation of computational logic. Moreover, in the categorical setting, a third paradigrn arises, not available elsewhere: logical-operations-as-adjunctions. It offers an answer to the notorious question of the equality of proofs. So we chase diagrams in algebra of proofs.On the basis of these ideas, the present paper investigates proof theory of (...) regular logic: the {∧, ∃}-fragment of the first order logic with equality. The corresponding categorical structure is regular fibralion. The examples include stable factorisations, sites, triposes. Regular logic is exactly what is needed to talk about maps, as total and single-valued relations. However, when enriched with proofs-as-arrows, this familiar concept must be supplied with an additional conversion rule, connecting the proof of the totality with the proof of the single-valuedness. We explain the logical meaning of this rule, and then determine precise conditions under which a regular fibration supports the principle of function comprehension , thus lifting a basic theorem from regular categories , recently relativized to factorisation systems [22, 42]. The obtained results bring us a step closer to extending the P-set construction [20] from triposes to non-posetal fibrations, and thus closer to “toposes” accommodating categorical proof theory. (shrink)