Reflection into models of finite decidable FP-sketches in an arithmetic universe

We consider finite decidable FP-sketches within an arithmetic universe. By an FP-sketch we mean a sketch with terminal and binary product cones. By an arithmetic universe we mean a list-arithmetic pretopos, which is the general categorical definition we give to the concept of arithmetic universe introduced by Andrè Joyal to prove Gödel incompleteness theorems. Then, for finite decidable FP-sketches we prove a constructive version of Ehresmann-Kennison's theorem stating that the category of models of finite decidable FP-sketches in an arithmetic universe is reflective in the corresponding category of graph morphisms. The proof is done by employing the internal dependent type theory of an arithmetic universe.