A. M. Pitts in [Pi] proved that $HA^\mathrm{op}_\mathrm{fp}$ is a bi-Heyting category satisfying the Lawrence condition. We show that the embedding $\Phi: HA^\mathrm{op}_\mathrm{fp} \longrightarrow Sh(\mathbf{P_0,J_0})$ into the topos of sheaves, ($\mathbf{P_0}$ is the category of finite rooted posets and open maps, $\mathbf{J_0}$ the canonical topology on $\mathbf{P_0}$) given by $H \longmapsto HA(H,\mathscr{D}(-)) : \mathbf{P_0} \longrightarrow \text{Set}$ preserves the structure mentioned above, finite coproducts, and subobject classifier, it is also conservative. This whole structure on $HA^\mathrm{op}_\mathrm{fp}$ can be derived from that of $Sh(\mathbf{P_0,J_0})$ via the embedding $\Phi$. We also show that the equivalence relations in $HA^\mathrm{op}_\mathrm{fp}$ are not effective in general. On the way to these results we establish a new kind of duality between $HA^\mathrm{op}_\mathrm{fp}$ and a category of sheaves equipped with certain structure defined in terms of Ehrenfeucht games. Our methods are model-theoretic and combinatorial as opposed to proof-theoretic as in [Pi].