[HoTT] Re: Precategories, Categories and Univalent categories

[Ulrik Buchholtz <ulrikbuchholtz@gmail.com>]

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

Mine and Paolo's replies crossed, but of course I missed the condition that 
the function be surjective.

On Wednesday, November 7, 2018 at 11:35:11 AM UTC+1, Ulrik Buchholtz wrote:
>
> Hi,
>
> First, there are (at least) three mathematically important and useful 
> types: precategories, strict (or set) categories (precategories with a set 
> of objects), and (univalent) categories.
>
> I take as one main lesson from HoTT/UF that mathematical objects have 
> types, and that the identity types should indicate the relevant notion of 
> identity.
>
> The type of precategories is equivalent to that of type-flagged categories 
> (categories together with a type O and a function from O to the objects of 
> the category). (The equivalence is given by pulling back the category 
> structure to get a precategory structure with O as the type of objects in 
> one way, and taking the Rezk completion together with the object part of 
> unit map in the other.)
>
> Two precategories are identified via an equivalence of the O-types and an 
> equivalence of the categories, together with a witness that the square 
> commutes.
>
> Two strict categories are identified via an isomorphism, and two 
> (univalent) categories are identified via an equivalence.
>
> So I disagree that "precategory" is the usual notion of category: it can't 
> be because the criterion of identity is different. But it's still a useful 
> concept.
>
> I personally prefer to keep “category” for univalent precategory, as most 
> often constructions on categories are meant to be well-defined up to 
> equivalence of categories. In the category theory literature written in a 
> set-theory metatheory where the distinction is not so clear, you can of 
> course find plenty of uses of the word “category” where “strict category” 
> is meant from a HoTT/UF point-of-view. The type of precategories as a 
> common generalization of strict and univalent categories is, I think, a new 
> concept to HoTT/UF. (Although infinity-groupoid flagged 
> (infinity,1)-categories arose independently in homotopy theory; these could 
> also be called (infinity,1)-precategories.)
>
> Cheers,
> Ulrik
>
> On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote:
>>
>> I want to get a general idea of peoples opinions when it comes to naming 
>> categories internal to HoTT.
>>
>> On the one hand I have seen, in the HoTT book for example, precategory 
>> and category being used where the latter has the map idtoiso being an 
>> equivalence.
>>
>> On the other hand I have seen people call these categories and univalent 
>> categories which is also fine.
>>
>> 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 would argue that the HoTT book convention is infact more misleading as 
>> "precategory" there is really just the usual notion of category. And a 
>> univalent category is some nice structure we can add to it because we are 
>> working in HoTT.
>>
>> What are your thoughts and opinions on this?
>>
>

-- 
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: 4068 bytes --]