From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:bf46:: with SMTP id u6-v6mr429434pls.3.1527952073500; Sat, 02 Jun 2018 08:07:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:5d4e:: with SMTP id e14-v6ls168171pgt.23.gmail; Sat, 02 Jun 2018 08:07:52 -0700 (PDT) X-Received: by 2002:a63:7048:: with SMTP id a8-v6mr1599421pgn.1.1527952072573; Sat, 02 Jun 2018 08:07:52 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527952072; cv=none; d=google.com; s=arc-20160816; b=lNB67vNOXvXVdiob1sXie6Sv31ietxhOI2KQdT8XZQBq9T0m8Spb34V0VTJ7cVoqs0 v5CT0K3Il8KO8X9spF8dTOAtlf2Ttm5PeC2RuoZESeIVoEKELEzj4ACcvLJOEgSEf3ad h0inqm3jhGqN7r0F30NRTPZzf5z9QlAODBULosrIjbZmGVqsIe6wfzqn/vETz8UxcqA2 it4KnSutGZtPcA40znFf6wexeLLW7qaz3te4ONCHO0JALKUoTegjVKQ4TyrrR4XE+deP j4lKBKh1522UG2HANh9OQZGnJysf+BeAD0MeLfuCSyUCqem3fN8ztTc2ohUhn0XhbDGG Yeqg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=gTG0xTWHxfICVRcWEh7VHI2Q99s6RirF4a2/BNHJhaw=; b=ntKXmlXW8EVjlQmQwQmqiNn8X1LMIzvvX5BoZAp/QugHbihMJGnqspf15OzUm0JwNd K/NVcdwHw41/pJCsiUNDGdETpuCOoltb9GkZlUZVVRkjX56dGIQiOVTpYSEeZtX/IpLH SkV9xDYxr4m0LfJ7bHGwPptm7NQF55TH47Kq3hEkRy1w6JnkxA9r+Zd6e9fIxSBlyqBZ +McX89i1Jh9qvoAGhmdCH2S3E5ZOEBGC42S97uHVsVUax/lQixi9ZVfFWbq3PNiBZO8B 4SPiwR/9rs+KSbYkK7ODoA1PqfxvQwfpqa9E3AB1xz0Ipk0sr0bKrF1mCmMxB4nAevS2 H+bA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uC78/hYt; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::22e as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x22e.google.com (mail-vk0-x22e.google.com. [2607:f8b0:400c:c05::22e]) by gmr-mx.google.com with ESMTPS id o5-v6si319214pgv.5.2018.06.02.08.07.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 02 Jun 2018 08:07:52 -0700 (PDT) Received-SPF: pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::22e as permitted sender) client-ip=2607:f8b0:400c:c05::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uC78/hYt; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::22e as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-vk0-x22e.google.com with SMTP id 128-v6so12003605vkf.8 for ; Sat, 02 Jun 2018 08:07:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=gTG0xTWHxfICVRcWEh7VHI2Q99s6RirF4a2/BNHJhaw=; b=uC78/hYtfZYE93LrJT6hoISuT7Dv55uKldIY4YNiaINv2Rvh3lUog907oOaYlO9yKe N4EiXL0t2P+Xoj1UR5dBzUbloQjxlOPIHvKgpkrT6SsTamXcC0/sqnRWzDEffw5ZvJXo IH6+JfhzW8O/9Irsd80Lzg9TL45WFWX+NBfEpnt21o+ffgVbeH5KOnfcZiencG8K7UeC D1SwnGNUA2aKBLBu0J82aIbu3L5YcuSyCwKLe5xds6m+wgfTs6VOhdDB3/kxi+tJMpjA ZXD9/67hBWtoD02XE1eSosffc0F72jtOFAY9CZZOkmxNqMEeurnoUeUTJCnHz04Tl+pS llGQ== X-Gm-Message-State: ALKqPwdAnkBLsg2YLkEfhCe+nzIhwAzyxroacCgG+D8o5zyYBaoCjV8U 9L80+rzIR2lDFK9JwjLZyfG+2PozHdrcSuJ320o= X-Received: by 2002:a1f:97d7:: with SMTP id z206-v6mr9024446vkd.183.1527952072127; Sat, 02 Jun 2018 08:07:52 -0700 (PDT) MIME-Version: 1.0 References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk> <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com> <1efa5fe9-cdc9-4714-ae2a-953ac59cfdf4@googlegroups.com> In-Reply-To: From: Eric Finster Date: Sat, 2 Jun 2018 17:06:00 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Michael Shulman Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000007e3b6d056daa10cd" --0000000000007e3b6d056daa10cd Content-Type: text/plain; charset="UTF-8" > 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. > > Yes, and there are of course other examples. Like finite sets and bijections being the free symmetric monoidal category on an object. And Delta as the free monoidal category with a monoid. Both of these statements are true whether I consider their higher versions or not. So I am aware of this phenomenon, which is why I believe the conjecture. > 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. > Hmmm. But isn't this situation different from the previous one? 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. For example, if this really were the case, wouldn't it rule out effectivity of (even finite) colimits? You'll have to remind me, but I think epis are still regular in an elementary 1-topos.... So in the infinity case, wouldn't this be making kind of a big concession? 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"? Right, completely agreed. 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. :) 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. --0000000000007e3b6d056daa10cd Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=C2=A0
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.=C2=A0 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.=C2=A0 This is essentially cut-elimination for
unary simple type theory.


Yes, and there are of course other exa= mples.
Like finite sets and bijections being the free symmetric m= onoidal category on an object.
And Delta as the free monoidal cat= egory with a monoid.
Both of these statements are true whether I = consider their higher versions or not.
So I am aware of this phen= omenon, which is why I believe the conjecture.
=C2=A0
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.=C2=A0 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.=C2=A0 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&qu= ot;
(in the model-categorical sense) not sets.

<= div>Hmmm.=C2=A0 But isn't this situation different from the previous on= e?
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 si= milar statement or not.
For example, if this really were the case= , wouldn't it rule out effectivity of (even finite) colimits?=C2=A0
You'll have to remind me, but I think epis are still regular in = an elementary 1-topos....
So in the infinity case, wouldn't t= his be making kind of a big concession?

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.=C2=A0 Does a HIIT initial
infinity-categorical structure that is not decidable count as
"syntax"?=C2=A0 Is it "syntax with a heavy flavor of semanti= cs", or is it
"semantics with a heavy flavor of syntax"?=C2=A0

Right, completely agreed.=C2=A0
I guess my posit= ion would be that, if we don't allow ourselves to think of a HIT presen= tation 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 li= st seems to be that we have found ways to manipulate them syntactically.=C2= =A0 :)
=C2=A0
Moreover, there's another reason that= this would be strange:
I mean, after all, kind of the whole poin= t of introducing higher algebraic objects is that these objects carry expli= cit witnesses for all of the relations they satisfy.
And our usua= l way of equipping objects with this kind of witness is to invent syntax fo= r it.
So shouldn't it somehow be exactly the opposite: should= n't we think of higher objects as *more* syntactic than their set theor= etic counterparts?

Whate= ver we call them,
such things are certainly interesting!=C2=A0 But I'm dubious that we co= uld
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.=C2=A0 Interesting and puzzling.
And I get= your point here.

E.

--0000000000007e3b6d056daa10cd--