Naive Cubical Type Theory