On the semantics of the universal quantifier Original Research Article

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.