On Wed, 7 Nov 2018, at 10:03 AM, Ali Caglayan wrote:
> Now because we have Rezk completion every precategory is yearning to become
> a category, so some might argue that a distinction isn't necessery.

I wouldn't say that. Yes, there is an adjunction between categories and precategories, but it's not an equivalence even in an ∞-categorical sense. In fact, following Ayala and Francis, you can think of a precategory as a category C equipped with the extra structure of a type X, and a surjective (i.e. -1-connected) morphism X → obj C.

> What are your thoughts and opinions on this?

Whatever notion ends up being called *category*, I would say it ought to at least be mapped to something that is (Quillen) equivalent to the usual notion of category through the simplicial set interpretation. That suggests categories should be univalent by default.

Best,
Paolo