Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman <shu...@sandiego.edu>]

On Sat, Jun 2, 2018 at 8:06 AM, Eric Finster <ericf...@gmail.com> wrote:
> Assuming there is an infinity category of elementary infinity-topoi, then I
> can ask the same question as before: is the initial such guy a 1-category.
> This is what, to me, the previous conjecture about categories with families
> was about.
> But now this time you use the word "presented", so I'm not sure if you are
> making a similar statement or not.

Right, presentation is the crucial point.  Let me try to say the same
thing again.

There are three kinds of structures under discussion:

1. 1-categories with families / fibration 1-categories
2. oo-categories with families / fibration oo-categories
3. oo-categories

There is an evident inclusion of (1) into (2), and also an "inclusion"
of (3) into (2) by taking the families to be arbitrary objects in
slices.  And there is also a sort of "reflection" operation from (2)
back into (3) that creates new higher cells out of arrows into path
objects, which I would expect to be some kind of left adjoint to the
"inclusion".  I'm not being precise about what extra structure these
things have, and what the functors between them are, so this is really
just a heuristic that I would expect to be true for any well-behaved
"doctrine" of extra structure that we could add to them.

If the doctrine in question includes things like effective oo-colimits
or univalent universes, then the initial object of (3) will not be a
1-category.  However, the initial object of (1) will always be a
1-category by definition.  The big conjecture is that the inclusion of
(1) into (2) preserves this initial object.  The "reflection", being a
"left adjoint", ought then to preserve initial objects, and therefore
take this initial structured 1-CwF (regarded as a structured oo-CwF)
to the initial structured oo-category -- in particular, making it no
longer a 1-category by adding higher cells coming from arrows into
path objects.

Of course, there will also be *other* objects of (2) that are also
reflected onto the inital object of (3), such as for instance the
inclusion of that initial object itself into (2).  The point is that
the initial object of (3) *can be presented by* the initial object of
(2), which *happens to coincide with* the initial object of (1).

Does that help?

> I guess my position would be that, if we don't allow ourselves to think of a
> HIT presentation as syntax for a higher object, if we insist that the word
> syntax be reserved for set level objects, then higher objects *don't have
> syntax by definition*!
> That seems surprising, since the point of this list seems to be that we have
> found ways to manipulate them syntactically.  :)

Right -- the way that we manipulate them syntactically is by
*presenting* free/initial ones with set-level objects.

> Moreover, there's another reason that this would be strange:
> I mean, after all, kind of the whole point of introducing higher algebraic
> objects is that these objects carry explicit witnesses for all of the
> relations they satisfy.
> And our usual way of equipping objects with this kind of witness is to
> invent syntax for it.
> So shouldn't it somehow be exactly the opposite: shouldn't we think of
> higher objects as *more* syntactic than their set theoretic counterparts?
>
>> Whatever we call them,
>> such things are certainly interesting!  But I'm dubious that we could
>> use them as a foundation for mathematics unless there is also an
>> untyped extrinsic syntax that can be typechecked into them (which
>> might or might not require them to be decidable).
>
>
> Yes, indeed.  Interesting and puzzling.
> And I get your point here.
>
> E.
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.