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=-0.7 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-ed1-x53f.google.com (mail-ed1-x53f.google.com [IPv6:2a00:1450:4864:20::53f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 378757be for ; Sat, 17 Aug 2019 00:14:48 +0000 (UTC) Received: by mail-ed1-x53f.google.com with SMTP id m30sf4345453eda.11 for ; Fri, 16 Aug 2019 17:14:48 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1566000887; cv=pass; d=google.com; s=arc-20160816; b=cJwTAMastb23FDXeWGiJz97wAncwNb09GbVrgA1g1i5p+tPxOIJsDSUvjnFyUZQffA uvV3dDPV6vwMAeE8LYkeGS7Q0ZTcL6MEKvmf6C/JNY7skP9GeeqFdVixNpEZsZvdDvN4 fMz4/waNnhbgIhDADolpz5XpIXxKYRhMX38qGHhHZxAFg86znUalIPKuv3Vj9bVIHlpa 3A8Ez8oSigzyZawxPxlOoXSaHBInfRkrWlQVj7v0mqe9sGa7BMKMv6WdUohDGdBu7swg aBGyYx9ebeuo9A+klahQyrarLFjviCOGsaX4va1vLo/LE8SBIC/PDVeqKdfT0az18O9n s8bA== 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=CltmhA1gHDnjtOG9JUv+eV8wNL+QMiM8IjG2FBYeSpE=; b=FVrvCrZ84OxNb3tQUsghC+1XeA9m1ywLjFtfFVtEzD3sKkOWDYa0qL3apwptyU0UY5 9R+5gIKorAuM0H5F8T+brIrMPruFd4Gnxr8TK0hxqNLoBHpiXLULjHd0Bq8ELi6I/cEg S+lRdJ13lG3OSum3gXqjPuyLDkteN8Qs+EURaDY6SNuzkBgv8eXUWZGJvh6ZVPqF/QfI eHyoQtTcVF4XDgpObbBkkEb1oh2NHHH6zGaoDG46gGPkZqO8qs3Kvi2Ry3qseR5jeCYm iHcp0eNEznqopRqhALLPlukFnqShPE+ErWFbJkUu3n/uJri8ZWHHanp16lh0xFSVBqEw wUsw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=HpdIjReF; spf=pass (google.com: domain of jasongross9@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=jasongross9@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=CltmhA1gHDnjtOG9JUv+eV8wNL+QMiM8IjG2FBYeSpE=; b=Kt1NFZzWNTeQMkgp9PgWbKfd7AwH5IfaN/lM4luJq+FATZ0dx71qQYvvndQHAyPQyZ kOTen2e2RKyanIFhdyjtIQfHaj35TU9IgZo3G2BV9QfXCnH4cIkwUDshWuevc/w88lz6 lbeZQ0Q2FMg+/SJAC3UcbMo2r3JAPaGA92yxLK820ir95HRa+RVYV9VQ8Q9WTW+iznTJ I82pggF5oGuZR2CIipZ2saOpiI7xWORV9/NnT8pbU7nJEirlOOjHoFzHcWPzsSP1i1oU AN6NCzehQo4M64qL4RqRGoYrcQZDziDJ4BL2mt0xjCgJZmk6esA6bWyo4hnOojfaZyIm MzAA== 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=CltmhA1gHDnjtOG9JUv+eV8wNL+QMiM8IjG2FBYeSpE=; b=e/zouHvDdR7AqwyNWx04/f0PdtyhSaI33mVmj6RxG/NQmdWfQ7EeLTxJ8rNUQ/1jc6 17pg21NpZpkjUXzuVztrEAamPRVXcdr874alpmVVzzN/d8jjfb3FWKfrl/gpYYshH93g nlbvLY01s1FKeaSG73R7fFTsq50t58xABqAXIvM+V3d2WA5uT/a3dKBeORq97JLTVe27 EQ00SBSc02gSwkdfuxG+EEuppE49fh1raPn1jstPo5P0vLwVJJA1cpQJgLY+WSlRBZfd /9y0BoHr4EqXEdQ5cyPXxm9NbEZVrSQdn95/9VSDjuMJeuuV0oHcjeyMmlG/39n3fu0k sDeg== 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=CltmhA1gHDnjtOG9JUv+eV8wNL+QMiM8IjG2FBYeSpE=; b=Bjhm5qqzI+lNeoRRksLv210iuWfks2iZTmh2GrtnpbAueNsQ/alaeXW8/k5rkW0CHw PZZW3dFdQ6Py5/UdvykkhSYW6Zi8G0RrXjfhAdI5hRSwrrZYhmNmdulh4xKXlUkqOqHE dzsMYvW5ZF9aNU9t0nontcODRJaxlAyDEMteOODwS++BR/i05KInoSNdTfiX2fNNPy/I e5XEI66K9x0HLkYR4TedmqlvEP6aa64TL/a5Ss8YZ1fwnC4Q+6GbA0SuqgsZltbieJwy ocmGejghlF1DkX+QSI3ufeaZnuA0O6/rlUoj0Pe9vIUuppmOFxz1fdM0G0xk3aBMLZ75 7ptg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXyY3l/Sut64An6Mlk/UfeBWFOGiUXOq4BYIqdJVl0iC0SvebG4 hFQeLj/akTAEFwqi1SAuNV8= X-Google-Smtp-Source: APXvYqyF99IRaxgn+iRTTKXBa3ClA25+rmIxrbZQTMDNNab2cG2iIWME1n7J+ciLKraJEm6n2AzBpA== X-Received: by 2002:a17:906:4c81:: with SMTP id q1mr351557eju.185.1566000887695; Fri, 16 Aug 2019 17:14:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:4351:: with SMTP id z17ls421751ejm.6.gmail; Fri, 16 Aug 2019 17:14:47 -0700 (PDT) X-Received: by 2002:a17:906:a952:: with SMTP id hh18mr11441194ejb.289.1566000887298; Fri, 16 Aug 2019 17:14:47 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1566000887; cv=none; d=google.com; s=arc-20160816; b=v8OAGV7n2PtdIFiGkB9z56hifCPg6bB/nlpTBlDvlB6ACDeFaVnPWDRPCAMLBIxcdG vfYuSrtbMRmyaBglHtTgJU1yvrevUUZyLZOveEbqMJb6TrpNZAwdvimmilYGQs0513cC feQOYqO4UGgG2voc16QCoX8MFTCURm+UCRliirsJ7c3Egc8MXzz+LzeBo+tvX3tw7XfU ExzoPRfGYkV2qzHmU12DzM1bkWEZ/3gEOMhWZOo7acwr76Yo8H0FWHuPMNERIWbng8GV yk1B7q0LnLBtd8Nagsg+2mRRHCpmstKnY+zcFoSNouKx0gssraQ2tH/dCGHiTOpWscJg kJ9A== 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=BmF7g+lr6ZyZBPBl6aEqNFYcwKK7k+QJ2kcgoNFqOhc=; b=YE4Y6/5Dp62HD8GkTV2miLTXFpA0BfhmZZ+vScsnfHG1gLcqpc3cU6JcQWhaHp+9uu nmGpMCdGz4tsMQWauFyVZxUQfRRqCjmKcMw+J25x6kJBD92ICfCPgdxUY26uwhGT5Tyy rMMH1WZE91BBgObzr0gagsZ3HpTTTORfA2kGf6GR+JvD0diPXd1+nyuQ7O+tTeJ37XwJ gkzecabArnUxk1qE1hIpKIqu6NrBppcM/SqYtzottQmmFeqcVG2zLuu5ujAYoXKzmBHO 4VnPovwKjRl8g3kkTEADs/zmfuqARxcQ/nAlFYKGb+fl0awzr0nLpPBEroWviV0c8JEy sdyw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=HpdIjReF; spf=pass (google.com: domain of jasongross9@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x52f.google.com (mail-ed1-x52f.google.com. [2a00:1450:4864:20::52f]) by gmr-mx.google.com with ESMTPS id m16si453518edv.2.2019.08.16.17.14.47 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 16 Aug 2019 17:14:47 -0700 (PDT) Received-SPF: pass (google.com: domain of jasongross9@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) client-ip=2a00:1450:4864:20::52f; Received: by mail-ed1-x52f.google.com with SMTP id r12so6539226edo.5 for ; Fri, 16 Aug 2019 17:14:47 -0700 (PDT) X-Received: by 2002:a17:907:2101:: with SMTP id qn1mr11657571ejb.3.1566000886952; Fri, 16 Aug 2019 17:14:46 -0700 (PDT) MIME-Version: 1.0 References: <50f257f8-f6a0-410e-9f32-512ebcef1e05@googlegroups.com> <68F509C8-C1BC-40B9-BE23-B930C801AF1D@ias.edu> <4957EC32-97FE-4383-AA07-C1ADF4EAF243@ias.edu> <435F59BF-DD90-43E0-926A-D197D38B94B4@ias.edu> In-Reply-To: <435F59BF-DD90-43E0-926A-D197D38B94B4@ias.edu> From: Jason Gross Date: Fri, 16 Aug 2019 17:14:19 -0700 Message-ID: Subject: Re: [HoTT] Definitions of equivalence satisfying judgmental/strict groupoid laws? To: Vladimir Voevodsky Cc: Peter LeFanu Lumsdaine , Thierry Coquand , "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000095b98c059044fe60" X-Original-Sender: JasonGross9@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=HpdIjReF; spf=pass (google.com: domain of jasongross9@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=jasongross9@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: , --00000000000095b98c059044fe60 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Resurrecting this thread from many years ago, because I was thinking about it again recently, it seems to me that although { f & isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) =3D e judgmentally, it doesn't satisfy the rule that sym id =3D id judgmentally. (In particula= r, I am not sure what relational equivalence to use for the identity equivalence which does not change judgmentally when I flip the order of its arguments.) Is there a version of equivalence which simultaneously satisfies that the inverse of the identity is judgmentally the identity, and that inverting an equivalence twice judgmentally gives you what you started with? -Jason On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky wrote: > In general no. But their model is essentially syntactic and more or less > complete. Or, to be more precise, I would expect it to > be more or less complete. > > V. > > > On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine < > p.l.lumsdaine@gmail.com> wrote: > > On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky > wrote: > >> The question is about how you interpret this operation for the univalent >> universe. If there is an interpretation of such an operation then there = is >> a way to define equivalences between types in an involutionary way. >> > > I don=E2=80=99t follow why this should be the case. This shows that ther= e is some > notion of equivalence *in the model* (i.e. constructed in the meta-theory= ) > which is strictly involutive. But there is no reason that this notion ne= ed > be definable in the syntax of the object theory, is there? > > =E2=80=93p. > > -- > 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. > > > -- > 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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAKObCao60%3DRFWY%3DCn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg%= 40mail.gmail.com. --00000000000095b98c059044fe60 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Resurrecting this thread from many years ago, because I wa= s thinking about it again recently, it seems to me that although=C2=A0{ f &= amp; isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) =3D e judgment= ally, it doesn't satisfy the rule that sym id =3D id judgmentally.=C2= =A0 (In particular, I am not sure what relational equivalence to use for th= e identity equivalence which does not change judgmentally when I flip the o= rder of its arguments.)=C2=A0 Is there a version of equivalence which simul= taneously satisfies that the inverse of the identity is judgmentally the id= entity, and that inverting an equivalence twice judgmentally gives you what= you started with?

-Jason

On Thu, Nov 13, 2014 at 1= 2:59 PM Vladimir Voevodsky <vladimir= @ias.edu> wrote:
In general no. But their = model is essentially syntactic and more or less complete. Or, to be more pr= ecise, I would expect it to=C2=A0
be more or less complete.=C2=A0

V.


On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.c= om> wrote:

On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vlad= imir@ias.edu> wrote:
The question is about how you interpret this operation for the= univalent universe. If there is an interpretation=C2=A0of such an operatio= n then there is a way to define equivalences between types in an involution= ary way.

I don=E2=80=99t follow why this should be the case.=C2=A0 This shows tha= t there is some notion of equivalence *in the model* (i.e. constructed in t= he meta-theory) which is strictly involutive.=C2=A0 But there is no reason = that this notion need be definable in the syntax of the object theory, is t= here?

=E2=80=93p.=C2=A0

--
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 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.
To view this discussion on the web visit https:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCao60%3DRFWY%3DCn0BTV9bW= cRCQXRSqOjvCYbS37mHOeJ0Yqg%40mail.gmail.com.
--00000000000095b98c059044fe60--