From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yb1-xb3d.google.com (mail-yb1-xb3d.google.com [IPv6:2607:f8b0:4864:20::b3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1360951f for ; Mon, 11 Feb 2019 08:04:59 +0000 (UTC) Received: by mail-yb1-xb3d.google.com with SMTP id r11sf1332243ybm.0 for ; Mon, 11 Feb 2019 00:04:59 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549872297; cv=pass; d=google.com; s=arc-20160816; b=t6UiaNoJ1xB/CfD9zD+PLNyQ6O71X7Tb0q7JxrDYg6oz0SLlBeclQNfuuQ+srXXJkA saTDdLXb3blYGKqIZhU1lBr06pH+zDkHhcrAn0WY9lPcY3g0epu/RUAgvA69skxBLYmF h0yMCmKqO7nN8nsdutfHJ8PlsHqIS4OYluHW1jNj2j5scDbUciGRFeC7wnDTpg5EpfDY wWNPRpQtCG3S6Z5QJYccux/amE6ILZh9MAyU70x4qDLOcnr8UcZAsv6yDKsw/orCseCT H6fzk8sA4AinOzWgtIU0/1LiVquoOiQrbU1eqB9jxzpFtAjNwYI3ufB43qBxu6Hjx4di lwwg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=QGsPwo+xysesR8vVwR9AnUojow//oKaEHZEXUd3FKxo=; b=QkrkaXAKzK1tg7VtVzcsD7Rxm6gS5bRQQOqbLpW1P5/6nIL7urNO34s2bKBtbc8xiN V33Gf3fdTTEKtWyX3CCr4mGQBGxa5hsyv22E3YoXUfqjC4EPSP6mq1Od1OP4MFLxzww8 UuqKjCRogdUJqJDWu1NPDzSd1oxskSY2aXTmqrRL/mj97vVefHI439yt9y5Ds6S4npay U3zapY2t2J0gz3oDvv40CnB9fASwxsNq4SYvGxAYJByGnUEChWOvLSe3B4GCR6sKaFR+ k5/zK9FIlga4W3vmcyJ4fuOBo3WGdJz/LM5jdSJxGN8vYdFeAVAdQ7e0WHcMZNzW1yTZ WarQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=g18thpIX; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12f as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=QGsPwo+xysesR8vVwR9AnUojow//oKaEHZEXUd3FKxo=; b=N7n4t1Q8eL++UolbyhQPRboPPOfzsXYgyjudNkAWGOkk2Q7mRM0jHggl+mZ+xP1g7F 8befWXY8y4xDTHfwyXPWwsTy8cfXtcROjhJfTXUT5iLWCB0p9xbEpr8IEzdenKX76TWs U7yArs7Y7imAkYgxvSE0KMOsiZrerKV5IbKm2KZC/5zOyg1dRiovwpwCHfNNSnCwLb/o lrolUivhPg5dD/1ZcI8jTG9CQAOOMtngIZCxZ+82kx7Au1I0FVVsWQ8bU1IdUGxrC/L8 UyA3YjK5hSEARDfhV/ZRV4+CxltRsp/w69O4ggIlve8jx0CcTKlZDdqT77CXLHXmbkjL sB9A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=QGsPwo+xysesR8vVwR9AnUojow//oKaEHZEXUd3FKxo=; b=DBXMYdCe69SJXQzvADPiW9MqD5FNfW262Z+kxC7T2BhJcqmTbCb+OxohG6l7Ssk6mX oDFRLgYsBugJYB80BF0J2J0hd4gQModAN+v4tzlqpPcvBXu8LxNsq8VruzZAlrjU7HcB i3GPXJtkBI1bqtji6gRwNCBIHEGW2j0Sd1xZQf7XLfcfecYWDRlprX7TskfA54U7ClpU eCvVcXrcYhCua0ClebxhsobfxZiSv1ULtQndBBI8/j0nWHubgZr0Q9g2iZkMkz2hXwVB IrG0KM8tTU+qgGigKCBMEW9du1ZpzW3Dg9FDxHrckc3knoEJnfn+3zIKS3GwrswOOKdj oR9g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=QGsPwo+xysesR8vVwR9AnUojow//oKaEHZEXUd3FKxo=; b=p4pWoCn8Ap8gfZhh8klKMssNJAWlVesLiPsYa5qK/skbx9bCl9DxeVe84kjxZhGHDc qxu7SrOfrsYWXML5uHWn3aTGwZnOnOWnPx5eQwM6y0JieYaSZ4IKy9dfAJNx0m4x/pJf TgrQyv5XHiXBkNEmSt+56U22XDdJ477cD4AAr9gacMeF/KzMoHV4I2ofHWDeq7qARQDg oXtkje3g2LSTcvCyGKcW+kgjZHnhVwfOou8iklEB2yDY7GEJ/7nFvvFMT1DiIMBGxeJO J7Dc0dKIxQlV69zGbraLK+j7NCHlDKNwcDvFFAPt0S0Yg5UXQtgwGKWZwf/+YgQr54IP f6GQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZW6j2bxL6u0uNOmnUrgeTtblfAVNMRJa2Lg0BQj1l9kVEAfcLK r5r7D/8RFsLklSrqHYvNr4M= X-Google-Smtp-Source: AHgI3IbtJHmMaTWLNNTEE7tGS7UrTFFiK/Wg5S1TQzS/3ZxW0xjOpdeGPmdw+MhR5vYt754ZLwN+/g== X-Received: by 2002:a81:8483:: with SMTP id u125mr55281ywf.7.1549872297798; Mon, 11 Feb 2019 00:04:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:b794:: with SMTP id n20ls4017389ybh.3.gmail; Mon, 11 Feb 2019 00:04:57 -0800 (PST) X-Received: by 2002:a25:b9ce:: with SMTP id y14mr14530632ybj.38.1549872297444; Mon, 11 Feb 2019 00:04:57 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549872297; cv=none; d=google.com; s=arc-20160816; b=iikp/nJgFKh9NdyyOhKIKbhZ3i+1X2Geey3tFFggQLMTTfrqLGqpJ9wBdqlQJSWTwp GmGCTw145ECM36qlZaMxeUWYT06BMdo0ebenxXPOJqviE00fofmXLb+PcYMub+fn5T3n jfpKjPUQo3ceoJ/wPI8THTcZW9qLVzky+BfkR4tX9Q1UwbnGjX1ENJ2d/aAid8rtqHoI akIFZm3IKDrQOP8jRC5os4X8HH1UPRB3HcQU3/dFzM6ffXGRLmO336h1W/1yI2qI7J9V HeQiuJl8LIm1s/vKGli6t8xLwmSsRzk0G6VPFGbGeYC8cAPCgcwHI9x3hwsbnAz3v8g5 Xlcg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=iMDaUDc8THRIyZJkJ6DTirm6dipS39A2gPUMkjzjOls=; b=R3PVfU1olLboz0DIwBz9rbMRlyEIbvFvtDK03xURMSHWWdHJ7toF6vLyeaIeTubHJi iDJyqX9tncbX5iC/CdPDENCDDV/qF7l07zGNf3yitzUNOFkjGUayEHF/v4MG0qoDgasb s5kmxiyHfBmhqG3/jl7L1P+LLwjj2j4U0ks5A2HZRvnyrx+baR0uMLOh7j8bGEBeg2k0 OryDWBKaLFI5wHH3phOAbW7rlzdZAnCQhPtVAO2RxRfdi88i8lLXXK5xZlCdVm95xVGz mngFBsqAWth115mpi1SDfRBC2t2O7eWk1I6xVTgHtr5nIlVZdOyJkVfYqdqocBbQAvom LSpw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=g18thpIX; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12f as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x12f.google.com (mail-it1-x12f.google.com. [2607:f8b0:4864:20::12f]) by gmr-mx.google.com with ESMTPS id k132si536222ywa.2.2019.02.11.00.04.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 00:04:57 -0800 (PST) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12f as permitted sender) client-ip=2607:f8b0:4864:20::12f; Received: by mail-it1-x12f.google.com with SMTP id z7so24162168iti.0 for ; Mon, 11 Feb 2019 00:04:57 -0800 (PST) X-Received: by 2002:a6b:6305:: with SMTP id p5mr8734673iog.92.1549872297096; Mon, 11 Feb 2019 00:04:57 -0800 (PST) MIME-Version: 1.0 References: <730FBE36-8E4F-45F5-9DB9-3B3A04E708FA@nottingham.ac.uk> In-Reply-To: From: Valery Isaev Date: Mon, 11 Feb 2019 11:04:20 +0300 Message-ID: Subject: Re: [HoTT] Why do we need judgmental equality? To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000b73a01058199c34c" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=g18thpIX; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12f as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000b73a01058199c34c Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Matt, I should point out that when I say "a type theory" I mean an ordinary dependently typed language, without any strict equalities or 2-levelness. Any such theory has only (dependent) types and terms and usual structural rules. Any "coherence problem" is solved by simply adding an infinite tower of terms. For example, in MLTT, if f : A -> B -> C, you can define function swap(f) =3D \x y -> f y x : B -> A -> C. Then swap \circ swap =3D id definitionally. Of course, you cannot have such a definitional equality in Q(MLTT), but instead you have a propositional equality p : Id(swap \circ swap, id) and also an infinite tower of terms, which assure that p is coherent. Any rule that holds definitionally in MLTT will be true in Q(MLTT) propositionally. Regards, Valery Isaev =D0=BF=D0=BD, 11 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 10:01, Matt = Oliveri : > I think you're right. From discussions about autophagy, it seems like no > one knows how to match judgmental equality using equality types, unless > that equality type family is propositionally truncated in some way. > > Consequently, my guess is that Valery's Q transformation actually yields > something rather like a 2-level system. > > On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch > wrote: >> >> Hi, >> >> >> >> what we need is a strict equality on all types. If we would state the >> laws of type theory just using the equality type we would also need to a= dd >> coherence laws. Since I would include the laws for substitution (never >> understood why substitution is different from application) this would >> include the laws for infinity categories and this would make even basic >> type theory certainly much more complicated if not unusable. Instead one >> introduces a 2-level system with strict equality on one level and weak >> equality on another. For historic and pragmatic reasons this is combined >> with the computational aspects of type theory which is expressed as >> judgemental equality. However, there are reasons to separate these >> concerns, e.g. to work with higher dimensional constructions in type the= ory >> such as semi-simplicial types it is helpful to work with hypothetical >> strict equalities (see our paper ( >> http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). >> >> >> >> I do think that the computational behaviour of type theory is important >> too. However, this can be expressed by demandic a form of computational >> adequacy, that is for every term there is a strictly equal normal form. = It >> is not necessary that strict equality in general is decidable (indeed >> different applications of type theory may demand different decision >> procedures). >> >> >> >> Thorsten >> >> >> >> >> >> *From: * on behalf of Felix Rech < >> s9fe...@gmail.com> >> *Date: *Wednesday, 30 January 2019 at 11:55 >> *To: *Homotopy Type Theory >> *Subject: *[HoTT] Why do we need judgmental equality? >> >> >> >> In section 1.1 of the HoTT book it says "In type theory there is also a >> need for an equality judgment." Currently it seems to me like one could,= in >> principle, replace substitution along judgmental equality with explicit >> transports if one added a few sensible rules to the type theory. Is ther= e a >> fundamental reason why the equality judgment is still necessary? >> >> >> >> Thanks, >> >> Felix Rech >> > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --=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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --000000000000b73a01058199c34c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Matt,

I should point out = that when I say "a type theory" I mean an ordinary dependently ty= ped language, without any strict equalities or 2-levelness. Any such theory= has only (dependent) types and terms and usual structural rules.
Any "coherence problem" is solved by simply adding an infinite t= ower of terms. For example, in MLTT, if f : A -> B -> C, you can defi= ne function swap(f) =3D \x y -> f y x : B -> A -> C. Then swap \ci= rc swap =3D id definitionally. Of course, you cannot have such a definition= al equality in Q(MLTT), but instead you have a propositional equality p : I= d(swap \circ swap, id) and also an infinite tower of terms, which assure th= at p is coherent. Any rule that holds definitionally in MLTT will be true i= n Q(MLTT) propositionally.

=
Regards,
Valery Isaev
=


=D0=BF=D0=BD, 11 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0= =B2 10:01, Matt Oliveri <atmacen@gm= ail.com>:
I think you're right. From discussions about autophag= y, it seems like no one knows how to match judgmental equality using equali= ty types, unless that equality type family is propositionally truncated in = some way.

Consequently, my guess is that Valery's Q transformati= on actually yields something rather like a 2-level system.

On Saturd= ay, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch wrote:

Hi,

=C2=A0

what we need is a strict equality on all types. If w= e would state the laws of type theory just using the equality type we would= also need to add coherence laws. Since I would include the laws for substi= tution (never understood why substitution is different from application) this would include the laws for infinity ca= tegories and this would make even basic type theory certainly much more com= plicated if not unusable. Instead one introduces a 2-level system with stri= ct equality on one level and weak equality on another. For historic and pragmatic reasons this is combined w= ith the computational aspects of type theory which is expressed as judgemen= tal equality. However, there are reasons to separate these concerns, e.g. t= o work with higher dimensional constructions in type theory such as semi-simplicial types it is helpful to work with hy= pothetical strict equalities (see our paper (http://www= .cs.nott.ac.uk/~psztxa/publ/csl16.pdf).

=C2=A0

I do think that the computational behaviour of type = theory is important too. However, this can be expressed by demandic a form = of computational adequacy, that is for every term there is a strictly equal= normal form. It is not necessary that strict equality in general is decidable (indeed different application= s of type theory may demand different decision procedures).

=C2=A0

Thorsten

=C2=A0

=C2=A0

From: <homotopyt...@googlegroups.com> on behalf of Felix Rech <s9fe...@gmail.com>
Date: Wednesday, 30 January 2019 at 11:55
To: Homotopy Type Theory <homotopyt...@google= groups.com>
Subject: [HoTT] Why do we need judgmental equality?

=C2=A0

In section 1.1 of the HoT= T book it says "In type theory there is also a need for an equality ju= dgment." Currently it seems to me like one could, in principle, replac= e substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. = Is there a fundamental reason why the equality judgment is still necessary?=

=C2=A0

Thanks,

Felix Rech

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000b73a01058199c34c--