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