 Despite first appearances, there are close connections between the approaches of (d)–(f). Constructive set theory can be interpreted in Martin-Löf type theory (due to Aczel 1978) and explicit mathematics can be interpreted in constructive set theory (see Rathjen 1993b, in Other Internet Resources). Perhaps the closest fit between (e) and (f), giving back and forth interpretations, is provided by Rathjen &amp; Tupailo 2006. Some concrete mathematical results are found at the end of  section 5.3.