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

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

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

On Fri, 9 Nov 2018, at 10:18 AM, Ulrik Buchholtz wrote:
> 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.

Let's say we define a *dependently-sorted algebraic theory* to just be a 
CwF. A model for it is a CwF-morphism into Set (or more generally into a 
CwF). The theory of categories would then be the opposite of Cat_{fp} (I 
mean finitely presentable, *not* locally finitely presentable), or 
alternatively you can define it inductively as the syntax of a type theory 
(but then you have to prove an initiality theorem!).

I'm not sure how this kind of presentation translates to ∞-categories 
though.

> 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?)

Nice question!

I guess by model here you mean a left exact ∞-functor T → Space, where T is 
regarded as an ordinary category with finite limits. I think such models 
are equivalent to Segal spaces, but without completeness. Or at least, I 
don't see where completeness would come from.

I find it quite an illuminating way to look at Segal spaces, by the way. 
You get the space of n-simplices by mapping the iterated pullback of the 
object of arrows in T (i.e. the object that stands for sequences of 
composable arrows). The Segal condition is the preservation of that 
pullback. It's essentially the same idea as in the definition of Γ-Spaces.

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