From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:600c:da:: with SMTP id u26mr23583569wmm.48.1589059686138; Sat, 09 May 2020 14:28:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:8d:: with SMTP id m13ls4815654wrx.4.gmail; Sat, 09 May 2020 14:28:04 -0700 (PDT) X-Received: by 2002:adf:ee86:: with SMTP id b6mr10700417wro.419.1589059684420; Sat, 09 May 2020 14:28:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589059684; cv=none; d=google.com; s=arc-20160816; b=0ua6mVGo7UhLvJbfWVJdQmm/TaySFesksguTwWVsN8g1AcFmzBo04yGsi9TjVoxMqF WKy08UAvZdepWn4mY15wUHZggr3L2RZ+tUt8/qNtkoRPtkpLcgXcbCZY54rcZVY2UKeW Eu0VbUUB2myYrT0gC6X3uMh01YcSScp74NV3ptzh4/h3D62L95PIw++hOFi+s6NmnXbD cQAnuz6Elb9Ha4CfJpwsw49R4GjtxB2uCrbvJWN83Dx6J6PQKSMoMBI9zf8U8GFqjVlp n7dlqyyCuTE1qRxqckfMHUJTOZfHeLSNGXCmp6BIV9oQlGKg8N3NawyFkKk7cGlgF+ac xTIg== 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=gMBdkzwtxNMwBdEWnhWAbOYkTflHy+E+pABOShb8Vwc=; b=ypPFTRPM2X/HueSMj4hT+bg6D20VW+wRHvo02kRmWwRiH25W+wfHhzwGdnG9jeSzaJ 0W5dTPRwEOKq8o0Tq9BmiakRuLZxTvWatPd5t9+RmsCxkCwd7e4lsbh7GfzW5Al0+PXX JZEh2TtisMvdiguebH6sCL0C4gXdqvftZBragYomCpRwYOD7uiG+wEmaFOYwWvISLkJ+ aro05UCKo1aMJOL9L7AO7btZuElV7vEO7zFMwsN+1BPmAnA2gr0t7vnPEoGd148hbL4F ieVqEuZxvd9GK9wNL2OPLKkoZrSq5JTlTgrpPr/9YKQbnRLmLIQw36i7744l4agqm66f qzYQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=ELp66qeu; spf=neutral (google.com: 64.147.123.24 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Return-Path: Received: from wout1-smtp.messagingengine.com (wout1-smtp.messagingengine.com. [64.147.123.24]) by gmr-mx.google.com with ESMTPS id d133si267586wmc.2.2020.05.09.14.28.03 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 May 2020 14:28:04 -0700 (PDT) Received-SPF: neutral (google.com: 64.147.123.24 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=64.147.123.24; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=ELp66qeu; spf=neutral (google.com: 64.147.123.24 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 7D7E642A for ; Sat, 9 May 2020 17:28:02 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute7.internal (MEProxy); Sat, 09 May 2020 17:28:02 -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=gMBdkzwtxNMwBdEWnhWAbOYkTflHy+E+pABOShb8V wc=; b=ELp66qeuUNZ0T/NDt4YMg41b3Xv5mLPGi5QIN4c9h1VmS4DTX6BYjO+dr qUU7XVY/HgV3B9b/kTlKNjjVMKsAWm+5ubi9oJQaTDXxC8/r9NjPxFOsEp17Ls0C Oo7gytItTBoo9AMkRc77FV2MxTVtg7SnrajVTBGzX5t/1vvyXm/J9uXbIQTAVAGs +y7sb+gpmvHPMTe9UngCjdtgHMGxp7TEryPA36e8fYJCG3SJkG9mFS4g7OW7ErMC s/gECXrG57fgaZ/xwVGgJfeRpsP7HwDDANolOemeLTmZNtJZXuQLwWOI3lVkW78c Qhb0y+RTcQR1T6jOus+U6b6s8wG4A== X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduhedrkeehgdduiedtucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne goufhushhpvggtthffohhmrghinhculdegledmnecujfgurhepofgfggfkjghffffhvffu tgfgsehtqhertderreejnecuhfhrohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjoh hnsehjohhnmhhsthgvrhhlihhnghdrtghomheqnecuggftrfgrthhtvghrnhephefgfeeh udevhfefkeethfdtffeukeffgfehjeegfeetffetffdvuefhudejgeegnecuffhomhgrih hnpehgohhoghhlvgdrtghomhenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhep mhgrihhlfhhrohhmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id C56825C0099; Sat, 9 May 2020 17:28:01 -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: In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> Date: Sat, 09 May 2020 17:27:16 -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, The coherence problems involved in formulating everyday notions like simpli= cial types (what an amazing world we live in to be able to call this everyd= ay!) can be resolved by extending Homotopy Type Theory with a "sub-homotopi= cal" layer, a second equality type that is meant to capture the strict math= ematical equality instead of paths. This is sometimes called Two Level Type= Theory. In this case, it is possible to define simplicial types, using the= strict equality to sidestep the problem of defining homotopy coherent stru= ctures in HoTT. There are a number of ways to achieve this, and they have different tradeof= fs depending on what your goals are. The space of possible realizations of = this idea corresponds to what Thomas has referred to as the "subjectivity" = of judgmental equality. Best, Jon On Sat, May 9, 2020, at 4:18 PM, Joyal, Andr=C3=A9 wrote: > Dear Thomas, >=20 > You wrote=20 >=20 > < for proving and not for computing. > But if you haven't mechanized PART of equational reasoning it would be > much much more painful than it still is. > But that is "only" a pragmatic issue.>> >=20 > Type theory has very nice features. I wish they could be preserved and= =20 > developped further. > But I find it frustrating that I cant do my everyday mathematics with=20 > it. > For example, I cannot say=20 >=20 > (1) Let X:\Delta^{op}---->Type be a simplicial type; > (2) Let G be a type equipped with a group structure; > (3) Let BG be the classifying space of a group G; > (4) Let Gr be the category of groups; > (5) Let SType be the category of simplical types. > (6) Let Map(X,Y) be the simplicial types of maps X--->Y > between two simplicial types X and Y. >=20 > It is crucial to have (1) > For example, a group could be defined to > be a simplicial object satisfying the Segal conditions. > The classifying space of a group is the colimit of this simplicial object= . > The category of groups can be defined to be > a simplicial objects satisfiying the Rezk conditions (a complete Segal sp= ace). >=20 > Is there some aspects of type theory that we may give up as a price > for solving these problems ? >=20 >=20 > Best, > Andr=C3=A9 >=20 > ________________________________________ > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > Sent: Saturday, May 09, 2020 2:43 PM > To: Joyal, Andr=C3=A9 > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;=20 > homotopyt...@googlegroups.com > Subject: Re: [HoTT] Identity versus equality >=20 > Dear Andr'e, >=20 > > By the way, if type theory is not very effective in practice, why do we= insist that it should always compute? > > The dream of a formal system in which every proof leads to an actual co= mputation may be far off. > > Not that we should abandon it, new discoveries are always possible. > > Is there a version of type theory for proving and verifying, less > > for computing? >=20 > In my opinion the currenrly implemented type theories are essentially > for proving and not for computing. > But if you haven't mechanized PART of equational reasoning it would be > much much more painful than it still is. > But that is "only" a pragmatic issue. >=20 > > The notations of type theory are very useful in homotopy theory. > > But the absence of simplicial types is a serious obstacle to applicatio= ns. >=20 > In cubical type theory they sort of live well with cubes not being > fibrant... They have them as pretypes. But maybe I misunderstand... >=20 > Thomas >=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= F5629FEC90B1652F563A%40Pli.gst.uqam.ca. >