From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aa7:85c4:: with SMTP id z4-v6mr22775pfn.36.1528229065862; Tue, 05 Jun 2018 13:04:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:304:: with SMTP id 4-v6ls455066pld.9.gmail; Tue, 05 Jun 2018 13:04:25 -0700 (PDT) X-Received: by 2002:a17:902:147:: with SMTP id 65-v6mr19313plb.41.1528229064997; Tue, 05 Jun 2018 13:04:24 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528229064; cv=none; d=google.com; s=arc-20160816; b=fHBGSAxxf3VR6zLkOJzTJi5+VxxgTbZITxrXokM1wCcDPHvLZjMOyo1sTG43oGWf6w 9Swj/rfrXqTv3LZDgJhSm5KNRYWj4EgEKtMFElgxVbIDXyqyH+t6YCwAg2Cn1I2k3uPM 5FHuuly6PGxQwpFwCKBGoH6pPht0dGpFS2qi/1/j1InXVK8YiPfKw5RK7R5aZnauW/VD 9NVGeymN24PiLwOfgToZTFenhVJj88Qa7u021ci75c+YcXTqD3STHBoDLAk9hkngmbx2 5DS8EKZbVZnAxZoB53neqpAe30CgwR35ezCcSRPcE+YTLGjz5erEWyFZKv1jq9rvQrPv Y7Xg== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=SIduXrAqJILNCH9edpAmiXOaqhFPy4cUQ5R0ri0N1L4=; b=pCb5oYjZML5fAk71QIbqb/0am6uOA72Jwrpmt9rD0oESv7Ozazd/nQy58ImHI9h9b7 FTn955Q2Ba0X3NE0rnO8cbGG6xkgWK3xUaYWATQUKq18tY2JBVJ/2cGKpgRl67XVyFaQ N7V6CJbEUaqzuNTrj4kLpj6G/18LoO9pDAMpjAkv2jQhVdDdo4XK9SAsBnLF1zCfHkN/ RKHSH1tZIYRvUpETKXI3vimPoagk6eMEC4ypQu6JnxF7EBrPIE2Ff9R9Qig7Sa/tcM5l 668UNkSeP4Nocf5NXK1SwnsswrtgQwFIqsIm63QHx3RVgbTCCTQbvDW7sxvcF9Ry7StO oDYA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=PKYQH2Rj; spf=neutral (google.com: 2607:f8b0:4002:c05::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x22d.google.com (mail-yw0-x22d.google.com. [2607:f8b0:4002:c05::22d]) by gmr-mx.google.com with ESMTPS id t63-v6si1444224pgd.2.2018.06.05.13.04.24 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Jun 2018 13:04:24 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22d is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=PKYQH2Rj; spf=neutral (google.com: 2607:f8b0:4002:c05::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22d.google.com with SMTP id v197-v6so1144643ywc.13 for ; Tue, 05 Jun 2018 13:04:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=SIduXrAqJILNCH9edpAmiXOaqhFPy4cUQ5R0ri0N1L4=; b=PKYQH2RjHxF/pmBfG3LslF9ssEKfNLsWuaf5NCriDFcgTioWhh0SIjmCGglYbnf3NR qf9mIZfL9cRYiiqNZv5KwMMGJFoCMIzexidTgl1GavhFkoTpmImlfRbrPFs0Duhk5sTh pEYEnJqnsCLANORtQQzF5i7rZCy2leq0lTVyr0JUh//e9dhfwCohp503qo6FGYYqHdFq 3RKOu8P71pADubvr7LYXFwJIKEgC+R8wME133yhe2DZ8JGsiayqFYEip8qQHnYMi85WF iPp7FIdLl3sSLF3QTYpgs4MI/SyU2Kl43rGSuwuZLE9edNfgMS9wwOsEVRPwAMsB/ZBd SBYw== X-Gm-Message-State: APt69E2ODeKXLVRfTduZWSe4nVLWUKvRF2DzQ/FIJ8atMReCbmUe5okg utK3rGcYPhgMIWfXSaGuufGDP8AZ X-Received: by 2002:a81:5590:: with SMTP id j138-v6mr42015ywb.310.1528229064273; Tue, 05 Jun 2018 13:04:24 -0700 (PDT) Return-Path: Received: from mail-yw0-f179.google.com (mail-yw0-f179.google.com. [209.85.161.179]) by smtp.gmail.com with ESMTPSA id m13-v6sm4869123ywh.102.2018.06.05.13.04.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Jun 2018 13:04:23 -0700 (PDT) Received: by mail-yw0-f179.google.com with SMTP id s201-v6so1147780ywg.8 for ; Tue, 05 Jun 2018 13:04:23 -0700 (PDT) X-Received: by 2002:a0d:eec2:: with SMTP id x185-v6mr21468ywe.477.1528229063313; Tue, 05 Jun 2018 13:04:23 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Tue, 5 Jun 2018 13:04:02 -0700 (PDT) In-Reply-To: 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> From: Michael Shulman Date: Tue, 5 Jun 2018 13:04:02 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Eric Finster Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" On Sat, Jun 2, 2018 at 8:06 AM, Eric Finster 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.