Computational Higher Type Theory I: Abstract Cubical Realizability