From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aa7:de88:: with SMTP id j8mr850007edv.309.1588993824174; Fri, 08 May 2020 20:10:24 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6402:1d83:: with SMTP id dk3ls1503778edb.9.gmail; Fri, 08 May 2020 20:10:22 -0700 (PDT) X-Received: by 2002:a50:cd57:: with SMTP id d23mr203177edj.181.1588993822412; Fri, 08 May 2020 20:10:22 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588993822; cv=none; d=google.com; s=arc-20160816; b=VWQHWfFY6Krj1yAZ74jWkVIcp8Vt5KA1lw+7U7FnJe3V65lkD8vSmpUEXRwLMJjmCM jKX+J3cUeynSvu7u4ZCgLnVwsP/EMP2iznMSwMlU/oN8J89uDTn4VJiTUTPSC/xKnPQN Gduh+d0QuEmC7kAWZAONxPWidr67FGGYks5RlljBgaVsXSmjqVplyaD17sBhGVYrtIKB XFWl/L4GoaHZ0SnJLLsTpzvzfRkFXrWIUKxQnhMLYXAYKjOZyovAOTy12EFOYWcaDJkx qBNxJu7fhek6AM9Q/l0ZMeAk4ZO+kmKocw2ZZ3BfesMlkxpSCfQ7eCcYcrZaUrSceXvU zb1g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:to:from:date:references :in-reply-to:message-id:mime-version:user-agent:dkim-signature; bh=5SKphEiYpb82tV5nPsOvR0w9q3NLsqELTT7Cty1alBI=; b=GZrEupPPzaq01TJIj4GAXWadgFIb561C9i7b7lmFFZbKh+HO84dT3lhSRunQ2EXNAR cn/61C4CAzZhbcXdu0vJCBAs4HK6JK8QXga0V07fVTJNjsRnr684F0UiXpVc5jzF+EZL sowlYBHQ/QMzZLnkSr85BnPmnS+Kyp1HmuIARbU/IWFI+yohfO5r5mL1OuU/tJv2KqvX k9wwCqQWOgPvzWtqEahUd9dQSfb8LYQzQCZo+ktOOEVIzwg/PjdR7pUDPj0iZz5RNws6 7iDCV2gu9/tmUwsq24iKSyOuQ4keKftxvGzW5uDFTc9o+INzZPbMEw1kFaBSJlI8ikAT 9kjQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=oUElHDe3; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Return-Path: Received: from wout2-smtp.messagingengine.com (wout2-smtp.messagingengine.com. [64.147.123.25]) by gmr-mx.google.com with ESMTPS id bt1si198643edb.0.2020.05.08.20.10.21 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 08 May 2020 20:10:22 -0700 (PDT) Received-SPF: neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=64.147.123.25; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=oUElHDe3; spf=neutral (google.com: 64.147.123.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Received: from compute7.internal (compute7.nyi.internal [10.202.2.47]) by mailout.west.internal (Postfix) with ESMTP id 54FB5726 for ; Fri, 8 May 2020 23:10:20 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute7.internal (MEProxy); Fri, 08 May 2020 23:10:20 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-proxy:x-me-proxy:x-me-sender:x-me-sender :x-sasl-enc; s=fm2; bh=5SKphEiYpb82tV5nPsOvR0w9q3NLsqELTT7Cty1al BI=; b=oUElHDe3l4e4ehS+m4DePo3jfzJQQM4cyJXskdKWiU7cVRT7hRlOPLmzX Ifh2A+iZti1mgM3oEwe2BunqDcHiRMokbMGx6MzZHWBn+r+X3lED17ElGMqbAHSG 4iAJA20oA18ooxbQ9J7PUxA0cht7PMc4M84HhwZ4XBMiWt/u/5MzxSRgeLryCmMJ KmgvNkFEHw3mvx7VN/rpYLTR37IXGVihoOpAqRZe+0DV+t/cSSKK23eotsuegR3N nFyRzDMsvFPWsKt9DqCLMhFq5aneL6UP73rN9WiJWbEaPgs9l3TjqA51gRLJjmpK NmA6a9ZpYrtkanS3YAQwd4AoPWOYg== X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduhedrkeeggdeivdcutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenog fuuhhsphgvtghtffhomhgrihhnucdlgeelmdenucfjughrpefofgggkfgjfhffhffvufgt gfesthhqredtreerjeenucfhrhhomhepfdflohhnucfuthgvrhhlihhnghdfuceojhhonh esjhhonhhmshhtvghrlhhinhhgrdgtohhmqeenucggtffrrghtthgvrhhnpeehgfefhedu vefhfeektefhtdffueekfffgheejgeefteffteffvdeuhfdujeeggeenucffohhmrghinh epghhoohhglhgvrdgtohhmnecuvehluhhsthgvrhfuihiivgeptdenucfrrghrrghmpehm rghilhhfrhhomhepjhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhm X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 99F7D5C0099; Fri, 8 May 2020 23:10:19 -0400 (EDT) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.3.0-dev0-413-g750b809-fmstable-20200507v1 Mime-Version: 1.0 Message-Id: <2dd3b058-7f41-49f3-beb9-ded40a2098b2@www.fastmail.com> In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F5565@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <1044A78D-8F16-4856-9B50-9B7FB7EF579A@gmail.com> <8C57894C7413F04A98DDF5629FEC90B1652F5565@Pli.gst.uqam.ca> Date: Fri, 08 May 2020 23:09:46 -0400 From: "Jon Sterling" To: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Identity versus equality Content-Type: text/plain;charset=utf-8 Content-Transfer-Encoding: quoted-printable Dear Andr=C3=A9, To answer your question about what is the abstract theory of term reduction= in type theory, one very beautiful option is rewriting theory, the study o= f abstract rewriting systems; this is perhaps the most venerable and mathem= atically deep tool to study term reduction, but it does not readily support= many of the kinds of "reductions" that occur in dependent type theory, esp= ecially the more exotic cubical type theories. For this and other reasons, some of us (including Steve and myself and many= others) have been lately studying computation in these type theories using= more abstract tools like Artin gluing --- the disadvantage of this approac= h is the gluing has little to say about the efficiency or algorithmic aspec= ts of computation in type theory, but it is enough to prove that existence = proofs do carry algorithms to compute numerals. Simultaneously, we are working on improving the algorithmic / practical asp= ects of cubical type theory so that in the future we may be able to actuall= y execute the algorithm that corresponds to Brunerie's proof. My collaborat= ors and I are currently experimentally programming a new reduction algorith= m for cubical type theory that I designed this fall; I do not know whether = it will help significantly, but we will see. Best, Jon On Fri, May 8, 2020, at 10:46 PM, Joyal, Andr=C3=A9 wrote: > Dear Steve, >=20 > Thank you for stressing the distinction between computing and proving. > I was thinking about the computation of a natural number by reduction of = terms.=20 > I must be confused. >=20 > But in type theory, is it not true that every proof is a computation? >=20 > Best, > Andr=C3=A9 >=20 >=20 >=20 >=20 >=20 > ________________________________________ > From: Steve Awodey [steve...@gmail.com] > Sent: Friday, May 08, 2020 7:44 PM > To: Joyal, Andr=C3=A9 > Cc: Thomas Streicher; David Roberts; Thorsten Altenkirch; Michael=20 > Shulman; Steve Awodey; homotopyt...@googlegroups.com > Subject: Re: [HoTT] Identity versus equality >=20 > Dear Andr=C3=A9, >=20 > I would prefer to say that t current systems of type theory have failed= =20 > to *compute* pi_4(S^3), so as not to diminish the value of Guillaume=E2= =80=99s=20 > beautiful proof, which has even been formally checked in different=20 > proof assistants. > You of course know the difference between proving something in type=20 > theory and computing the value of a term, but some readers may not. >=20 > Best wishes, >=20 > Steve >=20 > Ps: In my opinion, for what it=E2=80=99s worth, making a system that will= =20 > compute the value of Brunerie=E2=80=99s constant is an engineering proble= m, not=20 > a mathematical one. Which is not to say it would not be an important=20 > advance! >=20 > > On May 8, 2020, at 17:06, Joyal, Andr=C3=A9 wrote: > > > > =EF=BB=BFDear Thomas, > > > > You are right, the equality of objects in a Grothendieck fibration is j= udgemental. > > > > Propositional equality of type theory has been studied a lot during the= last decades. > > I feel quite confortable with it, with the homotopy interpretation and = the univalence principle, etc. > > I confess that I am much less at ease with judgmental equality and the = syntax of type theory. > > Until now, type theory has failed to prove that pi_4(S^3)=3DC_2. > > Is it the symptom of a fundamental problem? > > Is it because the reduction algoritms are not optimal? > > Or because computers are not powerful enough? > > What is the abstract theory of terms reduction in type theory? > > I apologise for my ignorance. > > > > Best, > > Andr=C3=A9 > > > > ________________________________________t > > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > > Sent: Friday, May 08, 2020 2:40 AM > > To: David Roberts > > Cc: Joyal, Andr=C3=A9; Thorsten Altenkirch; Michael Shulman; Steve Awod= ey; homotopyt...@googlegroups.com > > Subject: Re: [HoTT] Identity versus equality > > > > Dear Robert, > > > > in what I said I didn't mean set theory literally. I was rather referri= ng > > to all kinds of categorical logic where equality is interpreted as > > (fiberwise) diagonal like (traditional) topos theory in particular. > > These kinds of gadgets all have the advantage that "Set" is not ruled > > out as a model. > > > > Since the diagonal is hardly ever fibrant HoTT rules out Set as a model= . > > > > But this is not my main problem. My main problem is that there is at le= ast > > one area of category theory where one has to speak about equality of > > objects and these are Grothendieck fibrations. And these are intrinsic > > for doing topos theory over general base toposes. > > (That I really like them is, admittedly, also an important reason for m= e > > not being ready to give them up! And for reasons of personal and > > cultural "antagonisms" they are not very popular among the majority of > > category theorists... Thus, there are many people who would not be too > > sad about working in a framework not allowing to speak about them.) > > But I want to emphasize that real masters of infinite dimensional > > categories do not have the faintest problem speaking about equality > > when speaking about infinite dimensional versions of Grothendieck > > fibrations!) > > > > Though (traditional) topos theory can be developed over fairly general > > toposes and this, at least philosophically, is an important aspect one > > cannot deny that most toposes of interest heavily rely on Set, be they > > of the Grothendieck kind or be they of the realizability kind! > > > > Thomas > > > > PS Above I put Set into inverted commas because the logician in me > > finds it amusing to speak about "the" category of sets which is > > nothing but an illusion... Even the nowadays not so little number of > > adherents of the "multiverse" view of set theory would share this view! > > But even the "universe" view is nothing but an ideology because since > > Cohen set theory is mainly a business of constructing different models > > via forcing. > > Thus, since Set is (sort of) an illusion it is important to do toposes > > over arbitrary bases for which purpose one needs Grothendieck fibration= s > > which do not make sense without equality of objects. > > > > PPS Some people might get the impression I am a "crypto set > > theorist". Nothing could be more wrong. I am anti-ideological and > > pluralist and I like "deviating" ideas. But I am interested in > > calibrating what one needs for which goals. What I am allergic at is > > ideological positions which want to forbid someone doing certain > > things because they do not fit to some ideological positions... > > And one has to accept that not all combinations are possible. Thus > > pluralist is better to inegrist! > > > > -- > > You received this message because you are subscribed to the Google Grou= ps "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send = an email to HomotopyT...@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/d/ms= gid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F54CC%40Pli.gst.u= qam.ca. >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send=20 > an email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DD= F5629FEC90B1652F5565%40Pli.gst.uqam.ca. >