Inner Model of ZF(C) within Type Theory

[praeclarum]

Is it possible to develop inner model theory within Type Theory instead of ZF? And then, could you create an inner model of ZF within this?