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-ot1-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id bc9aa8ca for ; Mon, 11 Feb 2019 08:28:55 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id g4sf10405458otl.14 for ; Mon, 11 Feb 2019 00:28:55 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=kFlEyYI4+z+Lekae/lZIQwx4esyG9u/lOYNHYMv+5Ko=; b=UyywkCRRtptkfWqqdxzL/bt1qYMuaEM9MpK31JX2cdFXE4eqdEl9F0Kygvq/6+cE+M W7LkuAiaqPsesiVIrNYHGvnJkBkCogQ6P9Dg/BQiNCNjbjfrYUS5RgdSV1s3hFAhQmXp meqk1n93qZFfiv5uttV0yP1zYv/PNeUiMBqAst686MKmN7XOy1XlCVAZX2YtJSQuey+J y0of8m+4L+vG61+ru2CMMW1I/PatDl5GH+gnjWFO0Jq9AHYtT4jnFaip6Eug6szas2Sc WY6HSH3iEj+9YMCdRnq/GBAuGZiOLtuDWPSh/bD09wbfd16Ok646Y+OTCoqhvWcJRYg0 qrcw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=kFlEyYI4+z+Lekae/lZIQwx4esyG9u/lOYNHYMv+5Ko=; b=W+34UHH1W9e8pP56PoY2pc7R0f+WnbBey6SXmQ4EfSBHfhpton76cTd2K70/2Q9Dme aEo5t7t6kPS/48JX10iLfQw/ayo/W0q59Sp90er6x93Hs28uLY+luKKZw2iPoibHGKs/ /YRoUZNkhm6aJl2MCWg+/Xdm7/LXSHOdzXG/QduNnKSSEAvYaMR323750GDW/rO0rH3k 0KhaF65Lo7P/ZYZqDvIqkV2jZUL/PayGFHn8zSY6jWqfUez2BlQcTaa7QQ7HVNHVcGZZ vGCJuX0lxWON2nHPZPpRBOKeSKjte11lXiXqEDb4peAPDsMrMCErEbL2k5EBjOBRDBKN dKpQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=kFlEyYI4+z+Lekae/lZIQwx4esyG9u/lOYNHYMv+5Ko=; b=GXW8DiAdzLW3DlxZow4rxdjJlAwKGe9GttXlihQBRsMhC17DeU8LvSnXe6O5/HvxKp Ro25sCHDBmyLV4Y98D9tXo0FBEwJnBowmapawwrezGK/K/2np8EC2p09MbX3kV7eb5sh aK8B61JzqBAW4jeMq+Rv5LsCgY5neDZj/uFzlOQKJJfHnvmiTBji6KpA0aohAZeZQvYd 82t3u/7RRwjKQSYcy/816lg8kXtWuYedULk9dUrcwF9dyiH2YRgtpCck3UPN3RRJiNV3 u4ovnRivcX9cJBWvrZ+oLacvwH5ee8D9vUtW//w3ENAZW6j1O05k2UUyn1TLh6eKjG/b mMZQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZgnbO5/w5GbgA/RLapjqL5ALTrDJosO0RvthhCeIMq1D911HMY PwPHP3N/IKEDLyF5P81z2PA= X-Google-Smtp-Source: AHgI3IY9hSIdyDGzFtNudBw57ID3MJuugoeviTWEHpu64IaYpXdbXHUaHgy7z1mG6FxD9nL1VhQggg== X-Received: by 2002:aca:5bd7:: with SMTP id p206mr12465oib.2.1549873734545; Mon, 11 Feb 2019 00:28:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3d54:: with SMTP id k81ls1027991oia.1.gmail; Mon, 11 Feb 2019 00:28:54 -0800 (PST) X-Received: by 2002:aca:5884:: with SMTP id m126mr19847oib.4.1549873733923; Mon, 11 Feb 2019 00:28:53 -0800 (PST) Date: Mon, 11 Feb 2019 00:28:53 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <419b250c-491b-43de-96f8-d5dc34a5ff16@googlegroups.com> In-Reply-To: References: <730FBE36-8E4F-45F5-9DB9-3B3A04E708FA@nottingham.ac.uk> Subject: Re: [HoTT] Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_94_1724108199.1549873733395" X-Original-Sender: atmacen@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: , ------=_Part_94_1724108199.1549873733395 Content-Type: multipart/alternative; boundary="----=_Part_95_1822300861.1549873733395" ------=_Part_95_1822300861.1549873733395 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable OK, thanks. I stand corrected. But in that case, I'm with Thorsten: 2-level= =20 seems easier. On Monday, February 11, 2019 at 3:04:58 AM UTC-5, =D0=92=D0=B0=D0=BB=D0=B5= =D1=80=D0=B8=D0=B9 =D0=98=D1=81=D0=B0=D0=B5=D0=B2 wrote: > > Hi Matt, > > I should point out that when I say "a type theory" I mean an ordinary=20 > dependently typed language, without any strict equalities or 2-levelness.= =20 > Any such theory has only (dependent) types and terms and usual structural= =20 > rules. > Any "coherence problem" is solved by simply adding an infinite tower of= =20 > terms. For example, in MLTT, if f : A -> B -> C, you can define function= =20 > swap(f) =3D \x y -> f y x : B -> A -> C. Then swap \circ swap =3D id=20 > definitionally. Of course, you cannot have such a definitional equality i= n=20 > Q(MLTT), but instead you have a propositional equality p : Id(swap \circ= =20 > swap, id) and also an infinite tower of terms, which assure that p is=20 > coherent. Any rule that holds definitionally in MLTT will be true in=20 > 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, Mat= t Oliveri > >: > >> I think you're right. From discussions about autophagy, it seems like no= =20 >> one knows how to match judgmental equality using equality types, unless= =20 >> that equality type family is propositionally truncated in some way. >> >> Consequently, my guess is that Valery's Q transformation actually yields= =20 >> something rather like a 2-level system. >> >> On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch= =20 >> wrote: >>> >>> Hi, >>> >>> =20 >>> >>> what we need is a strict equality on all types. If we would state the= =20 >>> laws of type theory just using the equality type we would also need to = add=20 >>> coherence laws. Since I would include the laws for substitution (never= =20 >>> understood why substitution is different from application) this would= =20 >>> include the laws for infinity categories and this would make even basic= =20 >>> type theory certainly much more complicated if not unusable. Instead on= e=20 >>> introduces a 2-level system with strict equality on one level and weak= =20 >>> equality on another. For historic and pragmatic reasons this is combine= d=20 >>> with the computational aspects of type theory which is expressed as=20 >>> judgemental equality. However, there are reasons to separate these=20 >>> concerns, e.g. to work with higher dimensional constructions in type th= eory=20 >>> such as semi-simplicial types it is helpful to work with hypothetical= =20 >>> strict equalities (see our paper ( >>> http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf).=20 >>> >>> =20 >>> >>> I do think that the computational behaviour of type theory is important= =20 >>> too. However, this can be expressed by demandic a form of computational= =20 >>> adequacy, that is for every term there is a strictly equal normal form.= It=20 >>> is not necessary that strict equality in general is decidable (indeed= =20 >>> different applications of type theory may demand different decision=20 >>> procedures). >>> >>> =20 >>> >>> Thorsten >>> >> --=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. ------=_Part_95_1822300861.1549873733395 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
OK, thanks. I stand corrected. But in that case, I'm w= ith Thorsten: 2-level seems easier.

On Monday, February 11, 2019 at = 3:04:58 AM UTC-5, =D0=92=D0=B0=D0=BB=D0=B5=D1=80=D0=B8=D0=B9 =D0=98=D1=81= =D0=B0=D0=B5=D0=B2 wrote:
Hi Matt,

I should point out that = when I say "a type theory" I mean an ordinary dependently typed l= anguage, 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 fu= nction swap(f) =3D \x y -> f y x : B -> A -> C. Then swap \circ sw= ap =3D id definitionally. Of course, you cannot have such a definitional eq= uality in Q(MLTT), but instead you have a propositional equality p : Id(swa= p \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(M= LTT) propositionally.

Regards,
Valery Isaev


=D0=BF=D0=BD, 11 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 10:01, M= att Oliveri <atm...@gmail.com>:
I think you're right. From discus= sions about autophagy, it seems like no one knows how to match judgmental e= quality using equality types, unless that equality type family is propositi= onally truncated in some way.

Consequently, my guess is that Valery&= #39;s Q transformation actually yields something rather like a 2-level syst= em.

On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Alte= nkirch 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

--
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.
------=_Part_95_1822300861.1549873733395-- ------=_Part_94_1724108199.1549873733395--