Models of Type Theory With Strict Equality