Computational adequacy for recursive types in models of intuitionistic set theory