Post #3002042

The setoid model translation takes a model of type theory and returns a new model which validates function extensionality and propositional extensionality for SProp. Has anyone already worked out something like this for unique choice? I guess something like replacing functions with functional relations should work, right? I'm asking because I understand unique choice to be the reason why the definition of the effective topos is so complicated and doesn't just use plain setoids (see the last page of https://arxiv.org/pdf/1307.3832).