Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic

In a recent article the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure. Such structures are parametric models of the equational theory PILLY, a polymorphic intuitionistic / linear type theory with fixed points, in which one can reason using parametricity and, for example, solve a large class of domain equations.
Based on recent work by Simpson and Rosolini we construct a family of parametric LAPL-structures using synthetic domain theory and use the results of Simpson and Rosolini and results about LAPL-structures to prove operational consequences of parametricity for a strict version of the Lily programming language.
In particular we can show that one can solve domain equations in the strict version of Lily up to ground contextual equivalence.