A Quillen Model Structure in Type Theory