From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:ac2:5f5b:: with SMTP id 27mr8209964lfz.120.1589129490990; Sun, 10 May 2020 09:51:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:b6cc:: with SMTP id m12ls758404ljo.3.gmail; Sun, 10 May 2020 09:51:29 -0700 (PDT) X-Received: by 2002:a2e:9596:: with SMTP id w22mr8249745ljh.9.1589129489023; Sun, 10 May 2020 09:51:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589129489; cv=none; d=google.com; s=arc-20160816; b=D/vKEFfx8rx1r70zJakXUdwxGx5NaLXjnyNpMuyyCiniC+9f4tsRYS9CgqTTr7RuP+ Fs5Ua9Jyt8QoJsLuDnaK+KYFkgqYRDfIV9Qaolq8TwCX841jfZwcpC1IA5w33+HSuiTT sIyjseyA+h9I9eh89X6hIdRYgoUXIcmOKSgEe2aO2yLKygQelBOQvSGPU12kQDlPyib+ wfMQhtrMpi5xNAuHDf5Qwk6QAz7s7rbMK5OLBAM9lxnl5MnGXjAZ6SBq2vFkvS/67DlG V0o9ariSa9rbq1YTqQtpqUa0cmSNew1PYHkuSl7bzw1i/ogtLzjbJ1/oQjUcZBHdlv8H WkvA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:cc:to:subject :dkim-signature; bh=dlg8xdc+AlWwfe5W26Idx9UZIlUlQPsDjrV4vpcrmew=; b=yLZXJSMG+LoNEOeP2CCv+69Mm67bNd4yZVp1CmHT3JWINZHVp/zwrzohv4BSwcjHrE Bzshxy8RdFkD4kuWEJGeguPlInmgXJkBrziZ3lRiwaVJiPt4/L2el/xQTFjdiOjgTCvi GqFttQ6WvY08dUeM24OWoexhE3yRo50qQ0iLLxB+hqlc1/AVNaoO57rxlbVqxcJjZvWt d+MCt2i+UdwY33zVxunvTX7Cd0LcW/M18arouTZspZ+LVsRrKo0NiRm7tK9+LM2qwXML SBrH1Ic4OAYshgxw2BMOLCw76ClA7Q4Kit/eFdFcYftvzqu+N7tFSPIlPy6y6yn5aJ0q lNmw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=CknzzEeb; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wr1-x42a.google.com (mail-wr1-x42a.google.com. [2a00:1450:4864:20::42a]) by gmr-mx.google.com with ESMTPS id v19si74039lfe.3.2020.05.10.09.51.29 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 09:51:29 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) client-ip=2a00:1450:4864:20::42a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=CknzzEeb; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wr1-x42a.google.com with SMTP id e16so7939921wra.7 for ; Sun, 10 May 2020 09:51:28 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding:content-language; bh=dlg8xdc+AlWwfe5W26Idx9UZIlUlQPsDjrV4vpcrmew=; b=CknzzEebd5L38rk5hSopp0SHWyB0wCdz6OKmS8CF6yZKAM2RFAajSKzOL8tcaqiti2 G4jWTCtBtK9QTv0cZIINDugusbxHR0CT1kIYPWaLQUUwYcq45Gfbx2OmLr5F1h0+aY+/ 4CzyIJdDgn7eVlSUHp8y5xaiN/QufTAqmY5QuWn9n5jvp38P8+8zeq+xeDgO3mwMFGoi jcrg+bK0X4gknq8XC7cMcaM2JJ4D0eIcZSQRWz7VHSNsFO6d9CXBlttdDcJv3CWT9qpL zGeCks7WvgWXiG/dJ0NUVVsQJN95oDeoLJ4D8FEP0x4RFYrYWzeXl4jCVTi5H7cIBiFo 7+gQ== X-Gm-Message-State: AGi0PubgPG3juYI/aZDKbflnzvNhgAP/qGGAra2o661niZvvrG57IIHf QzVI4a0gxgaVmNZjsLMHRVRTMFvDgJrp+w== X-Received: by 2002:adf:a389:: with SMTP id l9mr9585713wrb.18.1589129487875; Sun, 10 May 2020 09:51:27 -0700 (PDT) Return-Path: Received: from [192.168.1.67] (37.67.90.146.dyn.plus.net. [146.90.67.37]) by smtp.gmail.com with ESMTPSA id 128sm16376609wme.39.2020.05.10.09.51.26 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 09:51:27 -0700 (PDT) Subject: Re: [HoTT] Identity versus equality To: =?UTF-8?Q?Joyal=2c_Andr=c3=a9?= , Thomas Streicher Cc: David Roberts , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" 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> From: Nicolai Kraus Message-ID: Date: Sun, 10 May 2020 17:51:26 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0 MIME-Version: 1.0 In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US Dear André and everyone, I feel it's worth pointing out that there are two strategies to express "everyday mathematics" in HoTT. In CS-speak, they would probably be called "shallow embedding" and "deep embedding". Shallow embedding is the "HoTT style", deep embedding is the "pre-HoTT type theory style". Shallow means that one uses that the host language shares structure with the object one wants to define, while deep means one doesn't. To explain what I mean, let's look at the type theoretic definition of a group (a 1-group, not a higher group). Definition using deep embedding: A group is a tuple (X,h,e,o,i,assoc,...), where   X : Type     -- carrier   h : is-0-truncated(X)     -- carrier is set   e : X   -- unit   o : X * X -> X     -- composition   i : X -> X     -- inverses   assoc : (h o g) o f = h o (g o f)   ... [and so on] Definition using shallow embedding: A group is a pointed connected 1-type. Fortunately, these definitions are equivalent (via the Eilenberg-McLan spaces construction). But they behave differently when we want to work with them or change them. It's easy to change the second definition to define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 , arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there is a nice way for the first definition. The second definition has better computational properties than the first. When you say this: > 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; You are referring to shallow embedding. In everyday mathematics, you don't say (1) either. You probably say (1) with "Type" replaced by "Set" or by "simplicial set". Both of these can be expressed straightforwardly in type theory using only (h-)sets (i.e. embedding deeply). We strive to use shallow embedding as often as possible for the reasons in the above example. But let's assume that we *can* say (1) in HoTT, using "Type", because we find some encoding that we're reasonably happy with; there's a question which I've asked myself before: Will we not destroy the advantages of deep (over shallow) embedding if we fall back to encodings (and thus destroy the main selling point of HoTT)? For me, the justification of still using deep embedding is that statements using encodings (e.g. "the universe is a higher category) might still imply statements which don't use encodings and are interesting. However, if we want to develop a theory of certain higher structures for it's own sake, then it's not so clear to me whether it's really better to use the HoTT-style deep embedding. Kind regards, Nicolai On 09/05/2020 21:18, Joyal, André 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 space). > > Is there some aspects of type theory that we may give up as a price > for solving these problems ? > > > Best, > André > > ________________________________________ > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > Sent: Saturday, May 09, 2020 2:43 PM > To: Joyal, André > 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 computation 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 >