Re: [HoTT] Re: Precategories, Categories and Univalent categories

[Ulrik Buchholtz <ulrikbuchholtz@gmail.com>]

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

On Friday, November 9, 2018 at 5:43:15 AM UTC+1, Andrew Polonsky wrote:
>
> The intuitive notion of a category is given by the dependently-sorted 
> algebraic theory of categories.
>

Maybe for you! But not for me: I don't even know what a dependently-sorted 
algebraic theory is, where and how such a thing has models, nor what the 
particular theory you're thinking of is.

But that reminds me of a MATHEMATICAL question. Consider the well-known 
essentially algebraic theory T whose models in Set are strict categories. 
What are the models of T in infinity-groupoids? (Or in an arbitrary 
(infinity,1)-topos?)
 

> However, more modern type theories, like HoTT or CubicalTT, have a 
> different, "native" conception of equality, so the "natural" notion of 
> category in these theories will accordingly be different as well.
>

In cubical type theories, the two notions of equality (path types and the 
inductive Id-family) are equivalent, so they give equivalent notions 
wherever they are used.

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