The fibrational formulation of intuitionistic predicate logic ${\rm I}$: completeness according to Gödel, Kripke, and Läuchli. II.
M. Makkai · Notre Dame Journal of Formal Logic · 1993
This is the second, concluding part of a two-part paper.After the mainly preliminary work of the first part, the present second part contains the treatment of the fibrational versions of the Kripke and the Lauchli completeness theorems.