Hybrids of the ×-translation for CZFωCZFω

In [W. Burr, Functional interpretation of Aczel's constructive set theory, Annals of Pure and Applied Logic 104 (2000) 31–73] Wolfgang Burr presents a functional interpretation of constructive set theory in all finite types, CZFωCZFω, in a theory TεTε of constructive set functionals. TεTε is a subtheory of CZFωCZFω, containing bounded quantifiers only. His interpretation theorem reduces the consistency problem of CZFωCZFω (and certain extensions thereof) to the consistency problem of TεTε.We want to study admissible rules in CZFωCZFω, i.e. rules under which CZFωCZFω is closed. To do so, we study a Troelstra-style q-hybrid of, in fact, a modification × of Burr's translation. We introduce this modification in order to close a minor gap in Burr's proof of the functional interpretation of the schema of (Strong Collection).First of all, but surely after a short introduction, we analyse the less complex translation of modified realisation mr and its hybrids mq and mrt.