Extending Homotopy Type Theory With Strict Equality