From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a65:6799:: with SMTP id e25mr582788pgr.9.1589077151782; Sat, 09 May 2020 19:19:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:224f:: with SMTP id c73ls14440864pje.3.canary-gmail; Sat, 09 May 2020 19:19:10 -0700 (PDT) X-Received: by 2002:a17:902:bd81:: with SMTP id q1mr9382774pls.46.1589077150310; Sat, 09 May 2020 19:19:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589077150; cv=none; d=google.com; s=arc-20160816; b=L1K8zs5avg4/tTnnvpKG1AZbvNuwiuyWoznIJ6UE/jNWe9uzMq+nKPKM2Mt7+Etnsn sj413C5rlDEBtwCjajSO7tUeSo1RBhbb+M6d2SqzXXlIhmzTnrUDT2yVtiFuDLfLTh3n zCFl18GP2PNZ3Gg8CYKn3Xl+mMZW+wDtY2sNZfARTpS/frK1GnqrSeFhCj4fkn/DG0a7 ucj/Gk/Yx5bsX1hS54gvsLARzzR2SGzzCFj27vbTmmSg6IH5w4PcT5SL3HgkuRMegSsz PwuBWxQA06QKwaK0J5PAKC8n1KPYpzhoqiQlTFhtAowZ3mvabr7C6sMxqk9WTu4WFuLQ G5sg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:ironport-sdr; bh=5OZWqTHwLHjXW14Nj7zyNVMbdnfGiuv5xsm+jEE8X9g=; b=aVzjwWYyDnIBwjsPuU52n7U4aw+b2FFkJFsfDo4epk/Xwa3oT3dH6Iz3OTVtt/xyH4 jW5REDrOkvh5sywJhXtOE8yeU7nC1BfdAwrjHrPW7ETRU5lUFigITomx/gDMCQCiRa6P QUxdSypPkMdbbiYJfHrVWJIlYexGEyMANI11X/vAKx8RpzBoV52QyxqqsXHkfi3ZaO9K qY7/nbI3rkWYQH8etxXtk1r8u+SElyXZ+TLWaA8qDBoLINVW5aRyO3+b6pNnIcSj3i97 nW+R6iqjSb/0rjfAvn6evtS3mHrh9gJoORuQ6BAeX8cFV/8LlVcFKHXd9ooxYPq3HfFz ltYA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail5.uqam.ca (mail5.uqam.ca. [132.208.246.108]) by gmr-mx.google.com with ESMTP id u18si345532plq.0.2020.05.09.19.19.09 for ; Sat, 09 May 2020 19:19:10 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) client-ip=132.208.246.108; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: KY7qd3FXAjTXD/5UxtjRHp/5IY8Dim6koQjrfml8gF+H4+ZwvlJe5fy4lWs5v1S5+6MPlCSqCR ApKjZxPBfxqkGQy+cj+UmIpNQQo6vy85iU5AwzEIhRMUCNzKvi78LTPmKV83Ka/rqESbTfJq2K IB1ueVtTjTid1GNMqFdTAE5Y7t4RVo0vjoRJVlBczftPoUAf2ukqZVRs8wEhMhYBTuDuFcqrQW 7LCcDAxrCc9FI02hLnCkYUo6gCWOiLrmjma5SDenPfUfoZFITtSUudA5EAH4k5WUImk/AxXB9i rC8= X-IronPort-AV: E=Sophos;i="5.73,374,1583211600"; d="scan'208";a="11955790" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.216.70]) by mail7.uqam.ca with ESMTP; 09 May 2020 22:19:09 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Message.gst.uqam.ca ([169.254.1.218]) with mapi id 14.03.0439.000; Sat, 9 May 2020 22:19:08 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Jon Sterling , "'Martin Escardo' via Homotopy Type Theory" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOFgABhQICAAHDSgIAAmhfJgAEWX4CAAC1BFIAAfoCA///K+0gADFtsAAABNScH Date: Sun, 10 May 2020 02:19:07 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F5693@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>, In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Dear Jon, You wrote: <> That is interesting. Is the "strict" equality like the equality relation between the maps of a Q= uillen model structure? I am curious to see the description of such a formal system. Is it related to Vladimir's theory with 3 levels of equality (which I never= understood)? Best, Andr=E9 ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf 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 Dear Andr=E9, 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=E9 wrote: > Dear Thomas, > > You wrote > > < 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.>> > > 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 > > (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. > > 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). > > Is there some aspects of type theory that we may give up as a price > for solving these problems ? > > > Best, > Andr=E9 > > ________________________________________ > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > Sent: Saturday, May 09, 2020 2:43 PM > To: Joyal, Andr=E9 > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; > homotopyt...@googlegroups.com > Subject: Re: [HoTT] Identity versus equality > > Dear Andr'e, > > > 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? > > 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. > > > The notations of type theory are very useful in homotopy theory. > > But the absence of simplicial types is a serious obstacle to applicatio= ns. > > In cubical type theory they sort of live well with cubes not being > fibrant... They have them as pretypes. But maybe I misunderstand... > > Thomas > > -- > 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/8C57894C7413F04A98DD= F5629FEC90B1652F563A%40Pli.gst.uqam.ca. > -- 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 e= mail to HomotopyT...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.