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-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d17201f2 for ; Mon, 11 Feb 2019 08:37:37 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id g4sf10422235otl.14 for ; Mon, 11 Feb 2019 00:37:37 -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=1x6E08qECgDUWpLDBpvTs9FCXkOKfh4O9Te8UdG97Ug=; b=soFT80kW5fT9BZVaYcJUffFv4v9zMlVqa3aOeXOCrLq5Q74bLV0g+SMnMUr0aMA4VG NhmhXvdLFWHRD2IurmyIzMYkN6HAnogIqb6EG3LtNMWWZSDEsUHs0FnnNFmi55ebcx8m cmsi3nvDjseRvAxhzhEBKza7r31QswxutGi48lMxlub/ayYYuWCa45Nw395GiV6ljhuH iMQEobfuNyz5DjaS+bmO+vVJpC+cJmgMXI/iVqCZLV3Qgf1pR6X9/ksMplZs56eXEFVL Vorp4JoJm9LwipJb848VFRjwlMWuWYdyHBpO9TVUlpMUuWe3WpoXcH6Bug+UyCFAlb1W UGdw== 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=1x6E08qECgDUWpLDBpvTs9FCXkOKfh4O9Te8UdG97Ug=; b=WJa8goT9/4tk8iOgUKWujss2HljVQuxRIALHjh/LLbRdZxTRupbk9Rfp24GFJPzm45 Dpm13o5lqMZvOrztnUhfVH5w7dhrTGkSEGkoAf5CONVLyzEqDjr351B8rGVxMT9RGiIR OZ4/AFDzQzmhvhz3nTiJq5Eao0h5dCevr/ILlYwSOoSop5L/wQPohrQl1C3ykR/iAt/U DqNKDrO+X4v8GyjJbGlVEkHjknllriTQBegU2sd3LNFwdFldCqxNUlBj9AKDON/AawTM hNvjawfHtAQSyieRsPk7LkNPef34JeN/d4tnv/xbM9SqsFGNxwfwOZ8HI0969gdQUWk4 YZLg== 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=1x6E08qECgDUWpLDBpvTs9FCXkOKfh4O9Te8UdG97Ug=; b=IqHf2qBecTPk2mB2cT2qu1qYkGdzFRCFNrK3OHo/dViRjJsrI/txdsHdJaTx0iZ+DC A8zhZbgHI5oz7wFTjVtBp9UUhXLxpP6e0IAMC+zEOWterW8bXtvUjxTh/dyLHil+ZvLo YC9UQdTSD85++qxbXkd6ZJ9T5JAlxmnXgerIgbAC7uiNirVyjzgPdM65XufgAl95qEC2 91tRWR+IjnUqgFiKV+bfpa9Y8egW98izYZ/0ulWbyGT2AFAjbHHPPnCy2wSL0P0eOaok paoby9Ql8NyjEq+xG+VWPn3GzL1TL9hzDrReQCNFvy+SwfcT3Ua+8o3a+ke6smmAovkA sp6g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubH2w2Pu6oykkUrsXESnFrW7JRTy4ewDkszRjZmrbXzJZvl9oEg skFeUq7zc+AzeceoZJwlz84= X-Google-Smtp-Source: AHgI3Ia7M9bF58yk76XRKvLRkcFeGnbgp2DSCDChx/4wzbAQL4if40bKD85h9PZFrJu3pZWQ8KtFTA== X-Received: by 2002:a05:6830:130d:: with SMTP id p13mr205873otq.2.1549874256553; Mon, 11 Feb 2019 00:37:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:ecc:: with SMTP id 70ls6779628otj.1.gmail; Mon, 11 Feb 2019 00:37:36 -0800 (PST) X-Received: by 2002:a05:6830:130d:: with SMTP id p13mr205872otq.2.1549874256269; Mon, 11 Feb 2019 00:37:36 -0800 (PST) Date: Mon, 11 Feb 2019 00:37:35 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: <419b250c-491b-43de-96f8-d5dc34a5ff16@googlegroups.com> References: <730FBE36-8E4F-45F5-9DB9-3B3A04E708FA@nottingham.ac.uk> <419b250c-491b-43de-96f8-d5dc34a5ff16@googlegroups.com> Subject: Re: [HoTT] Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_884_1395301239.1549874255625" 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_884_1395301239.1549874255625 Content-Type: multipart/alternative; boundary="----=_Part_885_498859502.1549874255625" ------=_Part_885_498859502.1549874255625 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Come to think of it, that's pretty cool though, that you can systematically= =20 produce all the higher coherences for a system of judgmental equations! On Monday, February 11, 2019 at 3:28:53 AM UTC-5, Matt Oliveri wrote: > > OK, thanks. I stand corrected. But in that case, I'm with Thorsten:=20 > 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=20 >> dependently typed language, without any strict equalities or 2-levelness= .=20 >> Any such theory has only (dependent) types and terms and usual structura= l=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 = in=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 >> > --=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_885_498859502.1549874255625 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Come to think of it, that's pretty cool though, that y= ou can systematically produce all the higher coherences for a system of jud= gmental equations!

On Monday, February 11, 2019 at 3:28:53 AM UTC-5,= Matt Oliveri wrote:
OK, thanks. I stand corrected. But in that case, I'm with Thor= sten: 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 &qu= ot;a type theory" I mean an ordinary dependently typed language, witho= ut any strict equalities or 2-levelness. Any such theory has only (dependen= t) types and terms and usual structural rules.
Any "coherenc= e 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 defi= nitionally. Of course, you cannot have such a definitional equality in Q(ML= TT), 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. A= ny rule that holds definitionally in MLTT will be true in Q(MLTT) propositi= onally.

=
Regards,
Valery Isaev

--
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_885_498859502.1549874255625-- ------=_Part_884_1395301239.1549874255625--