Reflection Into Models of Finite Decidable FP-sketches in an Arithmetic Universe
Maria Emilia Maietti · Electronic Notes in Theoretical Computer Science · 2005
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.