On the semantics of the universal quantifier (Q1371430)

The author studies the proof theory and categorical semantics of the \((\top,\wedge,\to,\forall)\) fragment of intuitionistic logic, using a class of fibrations which he calls \(\forall\)-fibrations to provide the models. The key observation which makes it easy to prove completeness theorems for this fragment is that the above connectives are precisely those whose interpretations are preserved by the Yoneda embedding (when they exist).