Relational semantics for flat Heyting-Lewis Logic

We introduce relational semantics for "flat Heyting-Lewis logic" $\mathsf{HLC}^{\flat}$. This logic arises as the extension of intuitionistic logic with a Lewis-style strict implication modality that, contrary to its "sharp" counterpart $\mathsf{HLC}^{\sharp}$, does not turn meets into joins in its first argument. We prove completeness and the finite model property for $\mathsf{HLC}^{\flat}$ and for several extensions with additional axioms.