Kan Simplicial Set Model of Type Theory