On the Setoid Model of Type Theory