From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.81.8 with SMTP id f8mr2827185iob.41.1511990007785; Wed, 29 Nov 2017 13:13:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.39.203 with SMTP id g194ls2223009ita.1.canary-gmail; Wed, 29 Nov 2017 13:13:26 -0800 (PST) X-Received: by 10.36.0.21 with SMTP id 21mr124699ita.13.1511990006818; Wed, 29 Nov 2017 13:13:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1511990006; cv=none; d=google.com; s=arc-20160816; b=FIPb2kTxyiczxsyLvw+mc0emgHkmS0vtOhNPW6x+KbaMW39LjDGA6izeaMqqIt2DVH F43Szut4VTltaZx6jijPwoFhvocTQCFPPUFB3LZa1onCxIPtbEp30Fu81xN/Qy3PGElb owLRjTtUy6q+1lU1/T0xfgSRneU/70Bh6duBeCN4IY7kH4dDOzIu0KHirdg+7H+yg7BN P9uAUNA0+aGRXyuz8Upao74p6aD7RYxwFgPS+L5wRo+zdL+HFVeGnyFn/TQE2WoeGUpR LWIphwh89YjO3J+0lyU7gV3xFbuch6z5WsASv/bwz8dVOn827hSO7uMf4Q8XOTLfxEOd SyZQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=1ueR2tlIcN+obJ/kVvbtfN4F1J8vbl7cOGMcnrODMAk=; b=QqfkfDE3OTuYndiPLBz6KhA6DF1RQqrYoAGTNGdup5/txzvLIhJNEcxrE+xULpdzdH vm2j6OJTMNRFmjPiAJIkwg2a7yWuIxiAjBg1axp5xVG01+nqPw2ckuADUFJTjUTWjmrf rz9W4hkZU3rdWDFXoAEOzySrfgARe+lpn4q2XHiSVpi3v0HIa+v9aDy82k9sj0w5opMp avMWGZK4r6wIkckc0XmTp4hOBYELiHzA/+/siVEsOobycod11/IhM3BqH/1U6tOsdCEV ObVaxDojU+G5OgQkMbyyud9ds7oG2bhxUSvJ8L5ZgXK22173P7ZqQCg2q3RraxYQ/Cls +Slw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=GndHzIZW; spf=pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c09::233 as permitted sender) smtp.mailfrom=evanc...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yb0-x233.google.com (mail-yb0-x233.google.com. [2607:f8b0:4002:c09::233]) by gmr-mx.google.com with ESMTPS id d125si456109itg.0.2017.11.29.13.13.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 29 Nov 2017 13:13:26 -0800 (PST) Received-SPF: pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c09::233 as permitted sender) client-ip=2607:f8b0:4002:c09::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=GndHzIZW; spf=pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c09::233 as permitted sender) smtp.mailfrom=evanc...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-yb0-x233.google.com with SMTP id g187so1886211yba.13 for ; Wed, 29 Nov 2017 13:13:26 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=1ueR2tlIcN+obJ/kVvbtfN4F1J8vbl7cOGMcnrODMAk=; b=GndHzIZWYj5mplsiWSM9npqeq0eg2BhVJiPJBiPHOOBHbvIv5wu9mbOmRFNOUlraU5 DRIOQJGYa+/3sXNLx5HVVM+SJZt0HRA29Xa68IPkgVkHSr1LkLmRSQkspbHQlkPYwpAr pNrQg7SC5OeEQbLJCc3Mxpq9hrhz/nMw3X4a0dFKjiLwRQdjuwGytRud9QmvlsH9zfiv e8hqIRqsJ1V7cxfa+tj5ijNq0tOHqTGvWktiN67iTmr4SU42k1LrWPyEXoPGVJj4w2F1 BtpAhoG74TRCG6ozb6gsNPyzPK6entqF5nt83wz5Kl2Ou86gwmtEtwd2Y3iq2dZPc+3x STuQ== X-Gm-Message-State: AJaThX53NAeFpRXKLd67Gzq68A6B4BDOxCGWPWIAW4x/QC7izZBmZG0s SDuHYJJ0BLp7lFo+zCYF163RLVk3Ci5mzmYzpprmsw== X-Received: by 10.37.104.195 with SMTP id d186mr162267ybc.470.1511990005750; Wed, 29 Nov 2017 13:13:25 -0800 (PST) MIME-Version: 1.0 Received: by 10.37.139.140 with HTTP; Wed, 29 Nov 2017 13:12:59 -0800 (PST) In-Reply-To: References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> From: Evan Cavallo Date: Wed, 29 Nov 2017 16:12:59 -0500 Message-ID: Subject: Re: [HoTT] Yet another characterization of univalence To: Homotopy Type Theory Content-Type: multipart/mixed; boundary="f403045c03de327c6d055f259bf6" --f403045c03de327c6d055f259bf6 Content-Type: multipart/alternative; boundary="f403045c03de327c69055f259bf4" --f403045c03de327c69055f259bf4 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Maybe this is interesting: assuming funext, if the canonical map Id A B -> A =E2=89=83 B is an embedding for all A,B, then Martin's axiom holds. Since= Id x y is always equivalent to (=CE=A0(z:X), Id x z =E2=89=83 Id y z), showing tha= t it is equivalent to Id (Id x) (Id y) can be reduced to showing that the map Id (Id x) (Id y) -> (=CE=A0(z:X), Id x z =E2=89=83 Id y z) is an embedding. Id A B -> A =E2=89=83 B is an embedding both if univalence holds and if axi= om K holds. Evan 2017-11-28 4:40 GMT-05:00 Andrej Bauer : > > If univalence holds, then Id : X -> (X -> U) is an embedding. > > > > But If the K axiom holds, then again Id : X -> (X -> U) is an embedding= . > > > > And hence there is no hope to deduce univalence from the fact that Id_X > is > > an embedding for every X:U. > > > > (And, as a side remark, I can't see how to prove that Id_X is an > embedding > > without using K or univalence.) > > So you've invented a new axiom? > > Escardo's axiom: Id : X =E2=86=92 (X =E2=86=92 U) is an embedding. > > (We could call it Martin's axiom to create lots of confusion.) > > With kind regards, > > Andrej > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --f403045c03de327c69055f259bf4 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Maybe this is interesting: assuming funext, if the ca= nonical map Id A B -> A =E2=89=83 B is an embedding for all A,B, then Ma= rtin's axiom holds. Since Id x y is always equivalent to (=CE=A0(z:X), = Id x z =E2=89=83 Id y z), showing that it is equivalent to Id (Id x) (Id y)= can be reduced to showing that the map Id (Id x) (Id y) -> (=CE=A0(z:X)= , Id x z =E2=89=83 Id y z) is an embedding.

Id A B= -> A =E2=89=83 B is an embedding both if univalence holds and if axiom = K holds.

Evan

2017-11-28 4:40 GMT-05:00 Andrej Bauer= <andrej...@andrej.com>:
> If univalence holds, then Id : X -> (X -> U) = is an embedding.
>
> But If the K axiom holds, then again Id : X -> (X -> U) is an em= bedding.
>
> And hence there is no hope to deduce univalence from the fact that Id_= X is
> an embedding for every X:U.
>
> (And, as a side remark, I can't see how to prove that Id_X is an e= mbedding
> without using K or univalence.)

So you've invented a new axiom?

=C2=A0 Escardo's axiom: Id : X =E2=86=92 (X =E2=86=92 U) is an embeddin= g.

(We could call it Martin's axiom to create lots of confusion.)

With kind regards,

Andrej

--
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 HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--f403045c03de327c69055f259bf4-- --f403045c03de327c6d055f259bf6 Content-Type: application/octet-stream; name="IdEmbedding.agda" Content-Disposition: attachment; filename="IdEmbedding.agda" Content-Transfer-Encoding: base64 X-Attachment-Id: f_jaljivn20 ey0jIE9QVElPTlMgLS13aXRob3V0LUsgLS1yZXdyaXRpbmcgIy19CgpvcGVuIGltcG9ydCBIb1RU Cgptb2R1bGUgSWRFbWJlZGRpbmcgd2hlcmUKCmlzLWVtYmVkZGluZyA6IOKIgCB7aSBqfSB7QSA6 IFR5cGUgaX0ge0IgOiBUeXBlIGp9IChmIDogQSDihpIgQikg4oaSIFR5cGUgKGxtYXggaSBqKQpp cy1lbWJlZGRpbmcgZiA9IOKIgCBiIOKGkiBpcy1wcm9wIChoZmliZXIgZiBiKQoKZXF1aXYtaXMt ZW1iZWRkaW5nIDog4oiAIHtpIGp9IHtBIDogVHlwZSBpfSB7QiA6IFR5cGUgan0gKGYgOiBBIOKG kiBCKSDihpIgaXMtZXF1aXYgZiDihpIgaXMtZW1iZWRkaW5nIGYKZXF1aXYtaXMtZW1iZWRkaW5n IGYgZi1lcSBiID0gY29udHItaXMtcHJvcCAoZXF1aXYtaXMtY29udHItbWFwIGYtZXEgYikKCmVt YmVkZGluZy1hcC1pcy1lcXVpdiA6IOKIgCB7aSBqfSB7QSA6IFR5cGUgaX0ge0IgOiBUeXBlIGp9 IChmIDogQSDihpIgQikKICDihpIgaXMtZW1iZWRkaW5nIGYKICDihpIg4oiAIGHigoEgYeKCgiDi hpIgaXMtZXF1aXYgKGFwIGYgOj4gKGHigoEgPT0gYeKCgiDihpIgZiBh4oKBID09IGYgYeKCgikp CmVtYmVkZGluZy1hcC1pcy1lcXVpdiBmIGYtZW0gYeKCgSBh4oKCID0gaXMtZXEKICAoYXAgZikK ICAozrsgcSDihpIgZnN0PSAocHJvcC1oYXMtYWxsLXBhdGhzIHt7Zi1lbSAoZiBh4oKCKX19IChh 4oKBICwgcSkgKGHigoIgLCBpZHApKSkKICAozrsgcSDihpIg4oiYLWFwIGYgZnN0IF8g4oiZICEg KOKGky1hcHA9Y3N0LW91dCcgJCBhcGQgc25kIChwcm9wLWhhcy1hbGwtcGF0aHMge3tmLWVtIChm IGHigoIpfX0gKGHigoEgLCBxKSAoYeKCgiAsIGlkcCkpKSkKICAozrsgcCDihpIgIGFwIGZzdD0g KHByb3AtaGFzLWFsbC1wYXRocyB7ez0tcHJlc2VydmVzLWxldmVsIChmLWVtIChmIGHigoIpKX19 IF8gXykg4oiZIGZzdD0tzrIgcCAo4oaTLWFwcD1jc3QtaW4nIGlkcCkpCgphcC1lcXVpdi1pcy1l bWJlZGRpbmcgOiDiiIAge2kgan0ge0EgOiBUeXBlIGl9IHtCIDogVHlwZSBqfSAoZiA6IEEg4oaS IEIpCiAg4oaSICjiiIAgYeKCgSBh4oKCIOKGkiBpcy1lcXVpdiAoYXAgZiA6PiAoYeKCgSA9PSBh 4oKCIOKGkiBmIGHigoEgPT0gZiBh4oKCKSkpCiAg4oaSIGlzLWVtYmVkZGluZyBmCmFwLWVxdWl2 LWlzLWVtYmVkZGluZyBmIGVxLWFwIGIgPSBhbGwtcGF0aHMtaXMtcHJvcCAkICjOuyB7KGHigoEg LCBw4oKBKSAoYeKCgiAsIHDigoIpIOKGkgogIHBhaXI9IChpcy1lcXVpdi5nIChlcS1hcCBh4oKB IGHigoIpIChw4oKBIOKImSAhIHDigoIpKQogICAgICAgICjihpMtYXBwPWNzdC1pbiAkIGxlbW1h IHDigoEgcOKCgiDiiJkgISAoYXAgKM67IHIg4oaSIHIg4oiZIHDigoIpIChpcy1lcXVpdi5mLWcg KGVxLWFwIGHigoEgYeKCgikgKHDigoEg4oiZICEgcOKCgikpKSl9KQogIHdoZXJlCiAgbGVtbWEg OiDiiIAge2l9IHtBIDogVHlwZSBpfSB7YeKCgSBh4oKCIGHigoMgOiBBfSAocCA6IGHigoEgPT0g YeKCgikgKHEgOiBh4oKDID09IGHigoIpCiAgICDihpIgcCA9PSAocCDiiJkgISBxKSDiiJkgcQog IGxlbW1hIGlkcCBpZHAgPSBpZHAKCl/iiJhlbWJfIDog4oiAIHtpIGoga30ge0EgOiBUeXBlIGl9 IHtCIDogVHlwZSBqfSB7QyA6IFR5cGUga30ge2cgOiBCIOKGkiBDfSB7ZiA6IEEg4oaSIEJ9CiAg 4oaSIGlzLWVtYmVkZGluZyBnIOKGkiBpcy1lbWJlZGRpbmcgZiDihpIgaXMtZW1iZWRkaW5nIChn IOKImCBmKQpf4oiYZW1iXyB7ZyA9IGd9IHtmID0gZn0gZy1lbSBmLWVtID0gYXAtZXF1aXYtaXMt ZW1iZWRkaW5nIChnIOKImCBmKSAkIM67IGHigoEgYeKCgiDihpIKICB0cmFuc3BvcnQgaXMtZXF1 aXYKICAgICjOuz0gKOKImC1hcCBnIGYpKQogICAgKGVtYmVkZGluZy1hcC1pcy1lcXVpdiBnIGct ZW0gKGYgYeKCgSkgKGYgYeKCgikg4oiYaXNlIGVtYmVkZGluZy1hcC1pcy1lcXVpdiBmIGYtZW0g YeKCgSBh4oKCKQoKYXAtaGZpYmVyIDog4oiAIHtpIGoga30ge0EgOiBUeXBlIGl9IHtCIDogVHlw ZSBqfSB7QyA6IFR5cGUga30gKGYgOiBBIOKGkiBCKSAoZyA6IEIg4oaSIEMpCiAgKGIgOiBCKSDi hpIgaGZpYmVyIGYgYiDihpIgaGZpYmVyIChnIOKImCBmKSAoZyBiKQphcC1oZmliZXIgZiBnIGIg KGEgLCBwKSA9IChhICwgYXAgZyBwKQoKYXAtaGZpYmVyLWVtYmVkZGluZy1pcy1lcXVpdiA6IOKI gCB7aSBqIGt9IHtBIDogVHlwZSBpfSB7QiA6IFR5cGUgan0ge0MgOiBUeXBlIGt9IChmIDogQSDi hpIgQikgKGcgOiBCIOKGkiBDKQogIOKGkiBpcy1lbWJlZGRpbmcgZwogIOKGkiDiiIAgYiDihpIg aXMtZXF1aXYgKGFwLWhmaWJlciBmIGcgYikKYXAtaGZpYmVyLWVtYmVkZGluZy1pcy1lcXVpdiB7 QSA9IEF9IGYgZyBnLWVtIGIgPSBpcy1lcQogIChhcC1oZmliZXIgZiBnIGIpCiAgKM67IHsoYSAs IHEpIOKGkiBhICwgPOKAkyBlIHF9KQogICjOuyB7KGEgLCBxKSDihpIgcGFpcj0gaWRwICg84oCT LWludi1yIGUgcSl9KQogICjOuyB7KGEgLCBwKSDihpIgcGFpcj0gaWRwICg84oCTLWludi1sIGUg cCl9KQogIHdoZXJlCiAgZSA6IOKIgCB7YuKCgSBi4oKCfSDihpIgKGLigoEgPT0gYuKCgikg4omD IChnIGLigoEgPT0gZyBi4oKCKQogIGUge2LigoF9IHti4oKCfSA9IChhcCBnICwgZW1iZWRkaW5n LWFwLWlzLWVxdWl2IGcgZy1lbSBi4oKBIGLigoIpCgplcXVpdi1saWZ0IDog4oiAIHtpIGoga30g e0EgOiBUeXBlIGl9IHtCIDogVHlwZSBqfSB7QyA6IFR5cGUga30gKGYgOiBBIOKGkiBCKSAoZyA6 IEIg4oaSIEMpCiAg4oaSIGlzLWVxdWl2IChnIOKImCBmKSDihpIgaXMtZW1iZWRkaW5nIGcg4oaS IGlzLWVxdWl2IGYKZXF1aXYtbGlmdCBmIGcgZ2YtZXEgZy1lbSA9IGNvbnRyLW1hcC1pcy1lcXVp diAkIM67IGIg4oaSCiAgZXF1aXYtcHJlc2VydmVzLWxldmVsICgoXyAsIGFwLWhmaWJlci1lbWJl ZGRpbmctaXMtZXF1aXYgZiBnIGctZW0gYinigbvCuSkge3tlcXVpdi1pcy1jb250ci1tYXAgZ2Yt ZXEgKGcgYil9fQoK57Gz55SwIDog4oiAIHtpfSB7QSA6IFR5cGUgaX0ge2HigoEgYeKCgiA6IEF9 IOKGkiBh4oKBID09IGHigoIg4oaSICjiiIAgYSDihpIgUGF0aCBh4oKCIGEg4omDIFBhdGggYeKC gSBhKQrnsbPnlLAgcCBhID0gcHJl4oiZLWVxdWl2IHAKCuexs+eUsC1pcy1lcXVpdiA6IOKIgCB7 aX0ge0EgOiBUeXBlIGl9IHth4oKBIGHigoIgOiBBfSDihpIgaXMtZXF1aXYgKOexs+eUsCB7YeKC gSA9IGHigoF9IHth4oKCID0gYeKCgn0pCuexs+eUsC1pcy1lcXVpdiA9IGlzLWVxIOexs+eUsCBn IOexs+eUsC1nIGct57Gz55SwCiAgd2hlcmUKICBnIDog4oiAIHtpfSB7QSA6IFR5cGUgaX0ge2Hi goEgYeKCgiA6IEF9IOKGkiAo4oiAIGEg4oaSIFBhdGggYeKCgiBhIOKJgyBQYXRoIGHigoEgYSkg 4oaSIGHigoEgPT0gYeKCggogIGcge2HigoIgPSBh4oKCfSBlID0g4oCTPiAoZSBh4oKCKSBpZHAK CiAg57Gz55SwLWcgOiDiiIAge2l9IHtBIDogVHlwZSBpfSB7YeKCgSBh4oKCIDogQX0gKGUgOiDi iIAgYSDihpIgUGF0aCBh4oKCIGEg4omDIFBhdGggYeKCgSBhKSDihpIg57Gz55SwIChnIGUpID09 IGUKICDnsbPnlLAtZyBlID0gzrs9ICQgzrsgYSDihpIgcGFpcj0gKM67PSAkIG5hdHVyYWxpdHkg ZSkgcHJvcC1oYXMtYWxsLXBhdGhzLeKGkwogICAgd2hlcmUKICAgIG5hdHVyYWxpdHkgOiDiiIAg e2l9IHtBIDogVHlwZSBpfSB7YeKCgSBh4oKCIDogQX0gKGUgOiDiiIAgYSDihpIgUGF0aCBh4oKC IGEg4omDIFBhdGggYeKCgSBhKQogICAgICB7YSA6IEF9IChwIDogYeKCgiA9PSBhKSDihpIg4oCT PiAoZSBh4oKCKSBpZHAg4oiZIHAgPT0g4oCTPiAoZSBhKSBwCiAgICBuYXR1cmFsaXR5IGUgaWRw ID0g4oiZLXVuaXQtciBfCgogIGct57Gz55SwIDog4oiAIHtpfSB7QSA6IFR5cGUgaX0ge2HigoEg YeKCgiA6IEF9IChwIDogYeKCgSA9PSBh4oKCKSDihpIgZyAo57Gz55SwIHApID09IHAKICBnLeex s+eUsCBpZHAgPSBpZHAKCmFwcGx5IDog4oiAIHtpfSB7QSA6IFR5cGUgaX0ge2HigoEgYeKCgiA6 IEF9IOKGkiBQYXRoIGHigoEgPT0gUGF0aCBh4oKCIOKGkiAo4oiAIGEg4oaSIFBhdGggYeKCgSBh IOKJgyBQYXRoIGHigoIgYSkKYXBwbHkgzrEgYSA9IGNvZS1lcXVpdiAoYXBwPSDOsSBhKQoKVGht 4oKBIDog4oiAIHtpfSB7QSA6IFR5cGUgaX0KICDihpIgKChh4oKBIGHigoIgOiBBKSDihpIgaXMt ZW1iZWRkaW5nIChhcHBseSB7YeKCgSA9IGHigoF9IHth4oKCID0gYeKCgn0pKQogIOKGkiBpcy1l bWJlZGRpbmcgKFBhdGgge0EgPSBBfSkKVGht4oKBIGFwcGx5LWVtID0gYXAtZXF1aXYtaXMtZW1i ZWRkaW5nIF8gJCDOuyBh4oKBIGHigoIg4oaSCiAgZXF1aXYtbGlmdCAoYXAgUGF0aCkgIQogICAg KGVxdWl2LWxpZnQgKCEg4oiYIGFwIFBhdGgpIGFwcGx5ICh0cmFuc3BvcnQgaXMtZXF1aXYgKCEg JCDOuz0gdHJpYW5nbGUpIOexs+eUsC1pcy1lcXVpdikgKGFwcGx5LWVtIGHigoIgYeKCgSkpCiAg ICAoZXF1aXYtaXMtZW1iZWRkaW5nICEgKHNuZCAhLWVxdWl2KSkKICB3aGVyZQogIHRyaWFuZ2xl IDog4oiAIHtpfSB7QSA6IFR5cGUgaX0ge2HigoEgYeKCgiA6IEF9IChwIDogYeKCgSA9PSBh4oKC KSDihpIgYXBwbHkgKCEgKGFwIFBhdGggcCkpID09IOexs+eUsCBwCiAgdHJpYW5nbGUgaWRwID0g zrs9ICQgKM67IF8g4oaSIHBhaXI9IGlkcCAkIHByb3AtaGFzLWFsbC1wYXRocyBfIF8pCgpwb3N0 4oiYLWlzLWVxdWl2JyA6IOKIgCB7aSBqIGt9IHtBIDogVHlwZSBpfSB7QiA6IEEg4oaSIFR5cGUg an0ge0MgOiBBIOKGkiBUeXBlIGt9IChoIDog4oiAIGEg4oaSIEIgYSDihpIgQyBhKQogIOKGkiAo 4oiAIGEg4oaSIGlzLWVxdWl2IChoIGEpKQogIOKGkiBpcy1lcXVpdiAozrsgKGsgOiDOoCBBIEIp IGEg4oaSIGggYSAoayBhKSkKcG9zdOKImC1pcy1lcXVpdicgaCBlID0gaXMtZXEKICAozrsgayBh IOKGkiBoIGEgKGsgYSkpCiAgKM67IGsgYSDihpIgaXMtZXF1aXYuZyAoZSBhKSAoayBhKSkKICAo zrsgayDihpIgzrs9ICjOuyBhIOKGkiBpcy1lcXVpdi5mLWcgKGUgYSkgKGsgYSkpKQogICjOuyBr IOKGkiDOuz0gKM67IGEg4oaSIGlzLWVxdWl2LmctZiAoZSBhKSAoayBhKSkpCgpwb3N04oiYLWlz LWVtYmVkZGluZyA6IOKIgCB7aSBqIGt9IHtBIDogVHlwZSBpfSB7QiA6IEEg4oaSIFR5cGUgan0g e0MgOiBBIOKGkiBUeXBlIGt9IChnIDog4oiAIGEg4oaSIEIgYSDihpIgQyBhKQogIOKGkiAo4oiA IGEg4oaSIGlzLWVtYmVkZGluZyAoZyBhKSkKICDihpIgaXMtZW1iZWRkaW5nIHtBID0gzqAgQSBC fSAozrsgZiBhIOKGkiBnIGEgKGYgYSkpCnBvc3TiiJgtaXMtZW1iZWRkaW5nIHtBID0gQX0ge0Ig PSBCfSBnIGctZW0gPSBhcC1lcXVpdi1pcy1lbWJlZGRpbmcgXyAkIM67IGbigoEgZuKCgiDihpIK ICBsZXQKICAgIGxlbW1h4oKBIDogaXMtZXF1aXYgKM67IChwIDogKGEgOiBBKSDihpIgZuKCgSBh ID09IGbigoIgYSkgKGEgOiBBKSDihpIgYXAgKGcgYSkgKHAgYSkpCiAgICBsZW1tYeKCgSA9IChw b3N04oiYLWlzLWVxdWl2JyAozrsgYSDihpIgYXAgKGcgYSkpICjOuyBhIOKGkiBlbWJlZGRpbmct YXAtaXMtZXF1aXYgKGcgYSkgKGctZW0gYSkgKGbigoEgYSkgKGbigoIgYSkpKQogIGluCiAgICB0 cmFuc3BvcnQgaXMtZXF1aXYKICAgICAgKM67PSAkIGxlbW1h4oKCIGbigoEgZuKCgikKICAgICAg KHNuZCAoYXBwPS1lcXVpdiDigbvCuSkg4oiYaXNlIGxlbW1h4oKBIOKImGlzZSBzbmQgYXBwPS1l cXVpdikKICB3aGVyZQogIGxlbW1h4oKCIDogKGbigoEgZuKCgiA6IM6gIEEgQikgKHAgOiBm4oKB ID09IGbigoIpIOKGkiA84oCTIGFwcD0tZXF1aXYgKM67IGEg4oaSIGFwIChnIGEpIChhcHA9IHAg YSkpID09IGFwICjOuyBmIGEg4oaSIGcgYSAoZiBhKSkgcAogIGxlbW1h4oKCIGbigoEgLl8gaWRw ID0gPOKAky1pbnYtbCBhcHA9LWVxdWl2IGlkcAoKVGht4oKCIDog4oiAIHtpfQogIOKGkiAoKEEg QiA6IFR5cGUgaSkg4oaSIGlzLWVtYmVkZGluZyAoY29lLWVxdWl2IDo+IChBID09IEIg4oaSIEEg 4omDIEIpKSkKICDihpIgKChBIDogVHlwZSBpKSDihpIgaXMtZW1iZWRkaW5nIChQYXRoIHtBID0g QX0pKQpUaG3igoIgY29lLWVxdWl2LWVtIEEgPSBUaG3igoEgJCDOuyBh4oKBIGHigoIg4oaSIAog IHBvc3TiiJgtaXMtZW1iZWRkaW5nICjOuyBhIM6xYSDihpIgY29lLWVxdWl2IM6xYSkgKM67IGEg 4oaSIGNvZS1lcXVpdi1lbSAoUGF0aCBh4oKBIGEpIChQYXRoIGHigoIgYSkpCiAg4oiYZW1iCiAg KGVxdWl2LWlzLWVtYmVkZGluZyBhcHA9IChzbmQgKGFwcD0tZXF1aXYpKSkK --f403045c03de327c6d055f259bf6--