[HoTT] Re: Precategories, Categories and Univalent categories

[Paolo Capriotti <p.capriotti@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1204 bytes --]

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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 1430 bytes --]