From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1f:a844:: with SMTP id r65mr6808964vke.56.1589079851933; Sat, 09 May 2020 20:04:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:b211:: with SMTP id b17ls311439vkf.3.gmail; Sat, 09 May 2020 20:04:10 -0700 (PDT) X-Received: by 2002:a1f:9e17:: with SMTP id h23mr6978302vke.57.1589079850475; Sat, 09 May 2020 20:04:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589079850; cv=none; d=google.com; s=arc-20160816; b=pys1v+DUcfeCEb3ULAmQ1XwRVJeaKdUsLj4/rxgsSFaJZpqX/RFFW/lNQFpAiQOdkQ F41R6x/JbcU6h2V1Taf+ryX1qjDlibeTMGv+KHFZqwaA2SlXfcd0Qpd1iLsgXR7m2OJy Dhu1c4LswTawiXq1dWM9trJIuLlEzkqaI4zne0eYr8/GlFH1ubrd6rvYpWdiY43TQhHn SRCGOn/r6MrGguJs8bnRrjmePDlmAM8g2uwnW/zJSBWRagaDFaHLAfLQfPPwyg8iPqsd iS8RI5h+3Y8+s5XX1tJNk+P6Mr7/jKXJzoAbUrUydz2InSsXlfYAwCN2Me50DyCd0AIR OS4w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=Z4aJvUE0Jn1GRvbDaNZtBjYke3VKq04RWiLeU/gDi58=; b=rZDVLGHr0F+7rdBvkENlAp251UMxLo7lM7tytnLJ9UiQQmR1/9ehQ/zziwrfR/zcp8 ajnEdbvnCXNFrtvotz89iY35tkm50D+Oki0ZND9bzKe9ZOS8m5vw92xJWbjYQiyIBZOt BBMZMln/RP+5/HOO45OoWgZv63x7Hxk5/DBOn40YYUdwHdv6Ahi2iJSVpE1Q9e+g/TZm DMbyw7q1UanI3kNHAphaUigGTadP/i8zfB4JooSAytE6TTsZ5HM68D0ldOyG3dLAO6BN UD9guGTUJV9lC6Gwc4a6oR9fOrAwz0y7vdN5bqq5yQaPo5MmKInlmjIkl5uv9elxIdnO cAkw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=Lc2IIjN+; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Return-Path: Received: from out2-smtp.messagingengine.com (out2-smtp.messagingengine.com. [66.111.4.26]) by gmr-mx.google.com with ESMTPS id y77si330089vky.0.2020.05.09.20.04.10 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 May 2020 20:04:10 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=66.111.4.26; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm2 header.b=Lc2IIjN+; spf=neutral (google.com: 66.111.4.26 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.nyi.internal (Postfix) with ESMTP id 0B8455C00D4; Sat, 9 May 2020 23:04:10 -0400 (EDT) Received: from mailfrontend2 ([10.202.2.163]) by compute7.internal (MEProxy); Sat, 09 May 2020 23:04:10 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc: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=Z4aJvUE0Jn1GRvbDaNZtBjYke3VKq04RWiLeU/gDi 58=; b=Lc2IIjN+TvpP3Frlj6WxxHiZesPA5EqcreiGZlZEPWoIRoGMXBME4RfsF JAOwN5zantxpX9Rxaw2q0o71XrBUd0G8mqn579qaQYeicQwbUgLeS+zWLiEUzl1a NnoQ7uImf1r4c9SVX8d8nmtnpKGFm4IVmhaAtWCZlrLuJGIDDw9Zba2z6gsPF6yr /NlM4fDG/QN10Ko4uqdQVd53LdxoKCifSpiepNAmxq5PqcZXFa3COQFXHSsBvJjP 6rkIykdFUFwY+k1qNr3HnG1ocajudhuyT0W4lLL7NtQEXQhaME6AUWSzAflBaEB0 8F7KNQaD+Om8/U9vWXHxBiKWwVBTQ== X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduhedrkeeigdeifecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenog fuuhhsphgvtghtffhomhgrihhnucdlgeelmdenucfjughrpegtggfuhfgjfffgkfhfvffo sehtqhhmtdhhtdejnecuhfhrohhmpeflohhnucfuthgvrhhlihhnghcuoehjohhnsehjoh hnmhhsthgvrhhlihhnghdrtghomheqnecuggftrfgrthhtvghrnhepgfdugedulefgledv hfduieekfedtuddujeekteekheeigeeuteevieeigeffudevnecuffhomhgrihhnpehgoh hoghhlvgdrtghomhenucfkphepjedurdeiuddrudejjedrudejudenucevlhhushhtvghr ufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhrohhmpehjohhnsehjohhnmhhsthgvrh hlihhnghdrtghomh X-ME-Proxy: Received: from [192.168.0.13] (c-71-61-177-171.hsd1.pa.comcast.net [71.61.177.171]) by mail.messagingengine.com (Postfix) with ESMTPA id 440993066245; Sat, 9 May 2020 23:04:09 -0400 (EDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 13.4 \(3608.80.23.2.2\)) Subject: Re: [HoTT] Identity versus equality From: Jon Sterling In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F5693@Pli.gst.uqam.ca> Date: Sat, 9 May 2020 23:04:08 -0400 Cc: 'Martin Escardo' via Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: 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> <8C57894C7413F04A98DDF5629FEC90B1652F5693@Pli.gst.uqam.ca> To: =?utf-8?B?IkpveWFsLCBBbmRyw6ki?= X-Mailer: Apple Mail (2.3608.80.23.2.2) Dear Andr=C3=A9, I don=E2=80=99t want to accidentally say the wrong thing, I think your intu= ition about the quillen model category is correct. Let me just say that the= strict equality of the type theory is interpreted as the mathematical equa= lity of a 1-categorical presentation of an infinity category, for instance = mathematical equality of cells in a simplicial set. The =E2=80=9Chomotopica= l semantics=E2=80=9D of type theory currently always factor through some 1-= categorical presentation of an infinity category (some may wish to change t= his! I welcome it); judgmental equality is at present always =E2=80=9Cabout= =E2=80=9D the 1-categorical presentation, whereas path equality is intended= to only make distinctions that makes sense at the level of the infinity-ca= tegorical localization. I am somewhat familiar with Vladimir=E2=80=99s HTS (Homotopy Type System) = =E2=80=94 the arrangement is that you have judgmental equality, a =E2=80=9C= strict equality=E2=80=9D type, and a path type. Some types are distinguishe= d as fibrant and others are not =E2=80=94 for instance, the fibrant types a= re closed under path types but not strict equality types. A rule is added t= o ensure that the judgmental equality coincides with the (inhabitedness of = the) strict equality type =E2=80=94 this rule is called =E2=80=9Cequality r= eflection=E2=80=9D by the logicians and type theorists. The rules are arran= ged to ensure that strict equality implies path equality but not the other = way around. This ensured by having a notion of non-fibrant type (rather tha= n having all types be fibrant). This may sound very confusing, but for intuitions it is helpful to think of= what it means in the context of an =E2=80=9Cintended model=E2=80=9D (for i= nstance, Vladimir=E2=80=99s model in simplicial sets). In that case, there = is an object that weakly classifies *all* small simplicial sets, and there = is also an object that weakly classifies just the Kan-fibrant small simplic= ial sets. The HTS formalism is then a (very strict) language to capture the= general-abstract aspects of this semantic situation. Vladimir=E2=80=99s HTS can be thought of as extending Martin-L\=E2=80=9Dof= =E2=80=99s Extensional Type Theory with homotopical notions; this is partic= ularly natural from a mathematical point of view, considering that a quille= n model category usually has finite limits. Other authors have considered r= ealizations of this idea that are more like extending Martin-L\=E2=80=9Dof= =E2=80=99s Intensional Type Theory + Streicher=E2=80=99s Axiom K with homot= opical notions (where Axiom K is something to ensure that there can, up to = identity, be only one proof of a given identity); this style is preferred f= or implementation or computational purposes. The differences between these = points of view are more syntactic than semantic =E2=80=94 I would call them= =E2=80=9Csubjective=E2=80=9D in deference to Thomas. Best, Jon > On May 9, 2020, at 10:19 PM, Joyal, Andr=C3=A9 wrote: >=20 > Dear Jon, >=20 > You wrote: >=20 > <> >=20 > That is interesting. > Is the "strict" equality like the equality relation between the maps of a= Quillen model structure? > I am curious to see the description of such a formal system. >=20 > Is it related to Vladimir's theory with 3 levels of equality (which I nev= er understood)? >=20 > Best, > Andr=C3=A9 >=20 > ________________________________________ > From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on be= half of Jon Sterling [j...@jonmsterling.com] > Sent: Saturday, May 09, 2020 5:27 PM > To: 'Martin Escardo' via Homotopy Type Theory > Subject: Re: [HoTT] Identity versus equality >=20 > Dear Andr=C3=A9, >=20 > The coherence problems involved in formulating everyday notions like simp= licial types (what an amazing world we live in to be able to call this ever= yday!) can be resolved by extending Homotopy Type Theory with a "sub-homoto= pical" layer, a second equality type that is meant to capture the strict ma= thematical equality instead of paths. This is sometimes called Two Level Ty= pe Theory. In this case, it is possible to define simplicial types, using t= he strict equality to sidestep the problem of defining homotopy coherent st= ructures in HoTT. >=20 > There are a number of ways to achieve this, and they have different trade= offs depending on what your goals are. The space of possible realizations o= f this idea corresponds to what Thomas has referred to as the "subjectivity= " of judgmental equality. >=20 > Best, > Jon >=20 >=20 > On Sat, May 9, 2020, at 4:18 PM, Joyal, Andr=C3=A9 wrote: >> Dear Thomas, >>=20 >> You wrote >>=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 >> developped further. >> But I find it frustrating that I cant do my everyday mathematics with >> it. >> For example, I cannot say >>=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 objec= t. >> The category of groups can be defined to be >> a simplicial objects satisfiying the Rezk conditions (a complete Segal s= pace). >>=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; >> 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 >> -- >> 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 HomotopyT...@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98D= DF5629FEC90B1652F563A%40Pli.gst.uqam.ca. >>=20 >=20 > -- > 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 HomotopyT...@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.co= m.