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

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

My intuition is that the conjecture should be true for any categorical
structure whose corresponding type theory satisfies normalization /
cut-elimination.  With my suggested approach the idea is that if there
is normalization, then you can define the initial 1-structure using
*only* the normal forms, so that there is no need to add
path-constructors at all.  Then instead of a HIIT/QIIT you have just a
normal IIT, which will be a set as long as all its parameters are
(this being necessary, as Jasper pointed out); and you can
nevertheless define maps out of it into higher types using its
induction principle.

In essence the situation is similar to how the free oo-group on one
generator (the integers) happens to be a set, because we can define
"normal forms" for integers as positive or negative unary natural
numbers.  This sort of thing is also known to happen elsewhere in
higher category theory; for instance, the free bicategory on a
directed graph happens to be a 1-category, because instead of
constructing it by throwing in all binary composites, associativity
isomorphisms, and so on, we can normalize all bracketed composites to
be (say) left-associated.  This is essentially cut-elimination for
unary simple type theory.

So, if we have a type theory for elementary infinity-toposes that has
normalization (perhaps some form of cubical type theory), then I would
believe the conjecture should hold fo them too.  Note that this
doesn't mean that the *objects* of the free elementary infinity-topos
are *internally* sets -- that would certainly be false since it
contains universes.  Instead, it means that the free elementary
infinity-topos can be *presented* by a structure (e.g. a CwF) that is
*externally* a set, just as the model category of simplicial sets is
itself a 1-category despite containing objects that are "internally"
(in the model-categorical sense) not sets.

It seems to me that the question of whether syntax should be decidable
seems to be just a question of definition as to where you draw the
line separating syntax from semantics.  Does a HIIT initial
infinity-categorical structure that is not decidable count as
"syntax"?  Is it "syntax with a heavy flavor of semantics", or is it
"semantics with a heavy flavor of syntax"?  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).


On Fri, Jun 1, 2018 at 2:53 PM, Eric Finster <ericf...@gmail.com> wrote:
>
>>
>> > I don't think the initial model is a set. Is it?
>>
>> This is the big conjecture that Thorsten and I actually agree on: that
>> the initial infinity-CwF in fact happens to be a 1-CwF.  Thorsten
>> wants to prove this by explicitly constructing the initial
>> infinity-CwF and then proving that it is a 1-CwF; my preference would
>> be to construct the initial 1-CwF in a careful way (e.g. with only
>> normal forms and hereditary substitution) so that one can prove that
>> it is in fact the initial infinity-CwF as well.  But in both cases the
>> conjectured result is the same, and even the important ingredient in
>> the expected proof is roughly the same: the existence of normal forms
>> and normalization.
>>
>
> Right, and I think I'm more or less on board with the conjecture.
> Although as you start adding more structure to your CwF, things get a bit
> murkier...
> Is it still okay with dependent products ... umm ... and what about if I add
> a class of HIT's?
> To take things really far: if there is such a thing as the free elementary
> infty-topos, is it a 1-category?
> This somehow seems dubious, no?
>
> So it seems to me at some point, something has to break in our notion of
> what syntax for higher algebraic objects *is* in the first place.
> Which is why I would not want to make the assumption from the outset that
> syntax must necessarily be decidable.
>
>
> --
> 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.