Guarded Computational Type Theory