Observational Type Theory