  This is the first of a series of papers on stack representation of finitely
presented Heyting pretoposes. In this paper, we provide the first step by
constructing a (2, 1)-site, which can be thought of as the site of finite
Kripke frames, such that the (2,1)-category of finitely presented Heyting
pretoposes contravariantly embeds into the (2,1)- topos of stacks on this (2,
1)-site. This provides an entry point to use categorical and higher
sheaf-theoretic tools to study the properties of certain classes of
intuitionistic first-order theories.
