Functional Representability in Local Set Theories

In general local set theories (LST), there is an incomplete representability as (x↦τ) for syntactic functions, i.e. those given by descriptions of the form ∀ x∃!yγ, for some formula γ. The well-known equivalence theorem establishes among other things that it is possible to produce a well-termed local set theory that extends any given LST. However, the natural translation between the corresponding languages still does not guarantee strict functional representability, but only up to isomorphisms. In this report, natural isomorphisms that are compatible with reasoning internally in the original LST are made explicit and explored in more generality. The internal translation along them is exhibited to be compatible with all logical operations; syntactic functions naturally represent themselves in a robust way as described in the main results.