From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a5d:9d51:: with SMTP id k17mr2291112iok.85.1589055491867; Sat, 09 May 2020 13:18:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:ce4c:: with SMTP id a12ls2270592ilr.8.gmail; Sat, 09 May 2020 13:18:10 -0700 (PDT) X-Received: by 2002:a92:d341:: with SMTP id a1mr9582240ilh.130.1589055490579; Sat, 09 May 2020 13:18:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589055490; cv=none; d=google.com; s=arc-20160816; b=kh6xRzrDI/LTRvhRChLN7FdC76pG1iFXR8DS/LxmbJEybhND7ZzXekXF6VjXOlIL0M 6kBKlh5UL/wHiHi74TtS3OshPHE/5wuye80QIiNQgVnSgb5afsaLIjAWB0WSN1oJKFbB 3OapYCMaaS54wq1J4rpAnavpx9PQt/2VFGxa8N6X7H28RZHJi+4KioJRfqUxkw/DxfxJ tI1q7ZGloNGBR3S5y3DVd/cAAF7kLU34XC+2d8R3dNBJHJ/qOlh0WxZ8435DWORnjLHy 7Aw42iE+joYrkDZ0ffWD5ThtgW63pThzLWoiedjvhO2pwWbybhHWbOXUSlYcY642JqnA C12w== 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:cc:to:from:ironport-sdr; bh=EXy/Eg50s3bS9hHcBxXvKx66JpVu7Xo3kRKg7aheM5c=; b=Fi0N62xeAL8sBoqClMxfqxuddTkcet2V5Tatwg+lt3PrK9qw4Ks/jA/ycpkzzNqKRA bCSbfo95h9tuw2mQF/6Xixclk9iazWAyXdFemt6/aw2Fx7bLmffiy1iC8j0dcZTANNJd kZOgk8FL7e/qQ9EyWoajj7vDA0w+WwpT/ekkj8fEzC4aHazr4IxZKWXJEkZn6HD0UVlC CBsu/6WC8ZkWUpua5PWwLe1XwDw1QWSrL9K4sLvoE1RU+jwxA2CfZVfQHPjg5fhSk7O+ b3akW4TneuzfPd5EMSRrBjMyexTT3sxHTpYRc1jjAsY0FPOHgbestN3HaztZn1fZYav1 MHdQ== 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 t16si347465ilj.3.2020.05.09.13.18.10 for ; Sat, 09 May 2020 13:18: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: Zsy+r5gTy0ARWLoTPNzC3frnx//0DOOYIhW0Y6R3y2RBxDXha3vO63QNaMriR66fLjx75VA2m0 YCFVv9XRIQsD5rMF2gwiEgOzd6WMfN1oSJ4nCK5KWZM9y4r6ZnuFUZLsI3YgAUujY4JkdyALX6 ukFIr57B8ImkjBWy+0YpWZU+b4OKjkes88f8MHRCqDb8wyQh2ZdS422uMSFcwUUmg2FkoqXtK7 aDOKo0Rh0jy9/0YZVmiT6A0UW1vcVKjEGXw1BkkPti4lU0zfKhv61L/9Be5fkPWDF7zVhQwWfl 82U= X-IronPort-AV: E=Sophos;i="5.73,373,1583211600"; d="scan'208";a="11940295" Received: from unknown (HELO Avis.gst.uqam.ca) ([132.208.216.75]) by mail7.uqam.ca with ESMTP; 09 May 2020 16:18:10 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Avis.gst.uqam.ca ([169.254.2.247]) with mapi id 14.03.0439.000; Sat, 9 May 2020 16:18:09 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Thomas Streicher CC: David Roberts , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOFgABhQICAAHDSgIAAmhfJgAEWX4CAAC1BFIAAfoCA///K+0g= Date: Sat, 9 May 2020 20:18:08 +0000 Message-ID: <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> In-Reply-To: <20200509184313.GB28841@mathematik.tu-darmstadt.de> 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 Thomas, You wrote=20 <> Type theory has very nice features. I wish they could be preserved and dev= elopped 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. 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 spac= e). 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; homo= topyt...@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 i= nsist that it should always compute? > The dream of a formal system in which every proof leads to an actual comp= utation 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 applications= . In cubical type theory they sort of live well with cubes not being fibrant... They have them as pretypes. But maybe I misunderstand... Thomas