On the Setoid Model of Type Theory - Erik Palmgren