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-wr1-x438.google.com (mail-wr1-x438.google.com [IPv6:2a00:1450:4864:20::438]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 20b104f9 for ; Sat, 25 May 2019 15:36:45 +0000 (UTC) Received: by mail-wr1-x438.google.com with SMTP id r7sf6109430wrn.8 for ; Sat, 25 May 2019 08:36:45 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558798605; cv=pass; d=google.com; s=arc-20160816; b=kULY2TIKGVMTqhpXUwrkid6vuUgJihcn3btjL9WPNGGv9CBBEeVjIGZUl66irk5S/D D5AJD1TcUywXcwPHlUh6L2Y+YB++w+4kSfgzSEwMQ8xye7TFBuGUnwOhXDVBC+70wg8a t4+4rn7JqaKqpB6Or0gfh1mW9Giqn98bu50LlrCvLZn+wkaOueMQm72+PWhrvi509YRQ MACJAxjQzP8H/laFDvn+fgr8zhUIYgTQMuNaRPq9/1CAO6iJg8aUqg3p4FsQI3sDiGed 9kw9NtjcW5NSxEtpv8KQ1sGj9BUNC4SVZS7vj9ZN13dVQ1MjUPj/XXW/4/9jIBVEZKTK e48A== 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=+FaEcNsDSZkNdGtEQ+pPObJaHAR40v4KhgHadGJjcqE=; b=vnoI5ta0uTDSlfS+HLbZeW2r/hdWDE6BR6jx2qtUV1K7PR3ey1xjVAEdw7clGGY3Vw FvIme22wa6MvAcyZ92LwNZa6OVhfeBt/TYrOpITZDrteEZZ1zdIpsVTbJ8JQH4y7qxg6 /axvan1QqwPKMCiMtesjVsE54V6QUrulF4u6ecZbwG/U/Mmc7dlve8ySFhysg9MVoaSY pwEI7vu6c8WcnsmhWF2Mv84l9sLHMIo61ls0UuQvXIm6wbSGu30okG6C8w7D38Zs05uT RFSf/R9/M2Kt0NTOwfd6FSogdNjZNWHMijE2a6B7JvwW7cQ8StQrlhhhhkF8a970mFzw GuEA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=D6V8WLpf; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) smtp.mailfrom=kevin.m.buzzard@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=+FaEcNsDSZkNdGtEQ+pPObJaHAR40v4KhgHadGJjcqE=; b=NtRXjNzo3TMramwz5ZTfTBGg7U5plf5zZGhN5wWvVKZP33ATaUixyEPdJtzVPXQ6P7 oxkQ/gAhEwAdpjtgUQTMS/NdryxaFLiaydKNOr3Ij1FCcBieEVNaEQkoo+sZTZhEPlRj zqjQyTQUwXZUHlb49Q74NY/W+N9HUhysfNC9ZgSmVihZSYiVNsYxf/YYB66mVa06Odbp myk6mJeI3qHv+VLIgmSdiMFgwNpw548CUUoNoQeGqvUwwIPnXcvxpht4V5zU5DEmN5nH ZUnriFIMQkhd4GfqEsu0jOBsSiIOst+O1zzx6GA6jSVTt8K/ceJlMHEkMQ4WPJklZBUB RJRg== 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=+FaEcNsDSZkNdGtEQ+pPObJaHAR40v4KhgHadGJjcqE=; b=dGIZBKahyr1oOErYgDMHMfIYGNFG8JVL0HNzWaK/74OSOEq1NlTCmbbCPSQc71tmWb BXLhhgRgcXK4m92hOcL1MjzRMMDhiaee6AZdDutVZsI7uNt3ktfsdDjkLjARoYqHkIea XXULPV393fjzasjMlXOnjypnt0A1kRC4pBru5hh62e6RM1uW5kUJiEP984Ic+i4QA43g 5cgohk93cxazSrsT6AG1J7gX9LA4Z73IBbNmeJePAKrPTrW/mGmlqoa2J7OZ1LarN+7g X0kJkWP/fc96PApoEu3msXt7xtKmnfMUBbueyT/MveRQHm9RedShiScLgzcBFzhMw6m4 w1qg== 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=+FaEcNsDSZkNdGtEQ+pPObJaHAR40v4KhgHadGJjcqE=; b=heZQhf6Pgvdl+ExzPq53wTGu3mYbA5WrKRWcB5qtyHKA/gxEd8FDNTMiZT8N1yFUMq pAVV71nU5HmHycXlQtNElo0hdpU5eY52o///QIJQ+9XC/KGXI8OcYQ5uO9fawp791olJ UtCFp3EHfTY2ZQff0AkhNEXTvcvZSsnaqx/WPkftKLRsVQlNziNeZGgYB8x0B1YVazFw ei94454x6dvL9jii/5syD8BZVGoPjqLJRqhJ/Uy1SW0Rx7m9BrvOKx4dEPD8OCUSEqIT tCv8qOGcrU6EZjvT7IjYBN4h+shTPBtxsIPhjWgXQrPRqv+fPpRvUtf3EnyaLjD40x5n rXOg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV4zOvcXMSapSLqvnS2u8kW2VweCC4y2VaA/Ti4grPvV/k4nyoY kbTuPYS3GCJ4vfV+h176J3Q= X-Google-Smtp-Source: APXvYqyxPkjPx2yy53up6+TykHZnOs0AVRzmnIsNfqXgwnXov/SlitIu4DISHy1tS7Ro+RLiViEQGA== X-Received: by 2002:a7b:c301:: with SMTP id k1mr4524733wmj.43.1558798605058; Sat, 25 May 2019 08:36:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:5301:: with SMTP id e1ls2990578wrv.13.gmail; Sat, 25 May 2019 08:36:44 -0700 (PDT) X-Received: by 2002:adf:edce:: with SMTP id v14mr3185040wro.94.1558798604221; Sat, 25 May 2019 08:36:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558798604; cv=none; d=google.com; s=arc-20160816; b=Sk4ViKgmlS/ZADj48T9x1ScZjwQJlQ16MZJJUWuewqYdLI35ocQQPHKJaKK0j2QzdV 7Z+qGA2iLPt5UsWKyrmkEnSKHQ257X/1dK2Y6bZfpKzTIGKAQeTQ4svqDqA2lPrUIlRW tPQs4h6dl8O6sF5DtF7NKLMFA/SBzWUu3vBRlDE8hXrFT0PTGA/tmOJH1B089oVealCw faej8IrnzVr0Y2FxM818PAcECCB0ykWYpTCDLqXRvNhqcfsse7pQZULLS8hHYEDXN6tN KJ37x1e1A88ZttdOAA5CbGwjjrCbGr9Ni9X0ntN2muf4Ob8BZwRNajRCNj0nbbmtvdDO ex5A== 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=ivBNvuWkKbmzm25fKPmS0+fwWDirBscU0qumu1kRKCA=; b=qtZJ0PDTDNZvONJJN/eKOWxjV+svU7MzNBwDIVguEadhNffmTuhk6aIHc3WCApz61P tXtFN0ZXfszu5BgP3Kypt6A38BfAdJvPoKubN4XKiU5f4xhl9nZnshC1UUCVbTXR8aEl BFfRBPeQTakEHR0QD0pEp5qc1DLbqtYXwac8sNyA8hX8l4/XbWk5so6i6jxuULMXWCT1 /ZWrlioZ6U9E7lnycMOtsVrxjbRHsitOVvg0xdjFLkEwIOr/0VHMHbsdED5WESwouunF GXoxtx64iwQiLELWbmhu1yJJgOhS+pVrHQqrJv4yGsK08MolOmGBX+5gZefybCOLiNQD rT+A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=D6V8WLpf; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) smtp.mailfrom=kevin.m.buzzard@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x134.google.com (mail-lf1-x134.google.com. [2a00:1450:4864:20::134]) by gmr-mx.google.com with ESMTPS id y70si838683wmd.0.2019.05.25.08.36.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 25 May 2019 08:36:44 -0700 (PDT) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) client-ip=2a00:1450:4864:20::134; Received: by mail-lf1-x134.google.com with SMTP id y17so1320101lfe.0 for ; Sat, 25 May 2019 08:36:44 -0700 (PDT) X-Received: by 2002:a19:48c3:: with SMTP id v186mr3029304lfa.42.1558798603793; Sat, 25 May 2019 08:36:43 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Kevin Buzzard Date: Sat, 25 May 2019 16:36:26 +0100 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Noah Snyder Cc: Juan Ospina , Homotopy Type Theory Content-Type: multipart/related; boundary="0000000000000f079a0589b815bc" X-Original-Sender: kevin.m.buzzard@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=D6V8WLpf; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::134 as permitted sender) smtp.mailfrom=kevin.m.buzzard@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: , --0000000000000f079a0589b815bc Content-Type: multipart/alternative; boundary="0000000000000f07980589b815bb" --0000000000000f07980589b815bb Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Noah. Thank you for pointing out the category error. It seems to me that sometimes when I say "HoTT" I should be saying, for example, "UniMath". Tactics in Lean are absolutely crucial for library development. Coq has some really powerful tactics, right? UniMath can use those tactics, presumably? I understand that UniMath, as implemented in Coq, takes Coq and adds some "rules" of the form "you can't use this functionality" and also adds at least one new axiom (univalence). On Sat, 25 May 2019 at 15:50, Noah Snyder wrote: > I=E2=80=99d also imagine that a =E2=80=9Cpractical=E2=80=9D implementatio= n would likely have some > kind of =E2=80=9Ctwo-level=E2=80=9D type theory where you can use types t= hat behave > classically when that=E2=80=99s better and HoTT types when that=E2=80=99s= better. > But plain Coq has such types, right? OK so this has all been extremely informative. There are other provers being developed which will implement some flavour of HoTT more "faithfully", and it might be easier to develop maths libraries in such provers. For example, if G and H are isomorphic groups and you want to translate a > theorem or construction across the isomorphism. In ordinary type theory > this is going to involve annoying book-keeping which it seems like you=E2= =80=99d > have to do separately for each kind of mathematical object. > Yes. This is a pain point in Lean. It's a particularly nasty one too, as far as mathematicians are concerned, because when you tell a mathematician "well this ring R is Cohen-Macauley, and here's a ring S which is isomorphic to R, but we cannot immediately deduce in Lean that S is Cohen-Macauley" then they begin to question what kind of crazy system you are using which cannot deduce this immediately. As an interesting experiment, find your favourite mathematician, preferably one who does not know what a Cohen-Macauley ring is, and ask them whether they think it will be true that if R and S are isomorphic rings and R is Cohen-Macauley then S is too. They will be very confident that this is true, even if they do not know the definition; standard mathematical definitions are isomorphism-invariant. This is part of our code of conduct, in fact. However in Lean I believe that the current plan is to try and make a tactic which will resolve this issue. This has not yet been done, and as far as I can see this is a place where UniMath is a more natural fit for "the way mathematicians think". However now I've looked over what has currently been formalised in UniMath I am wondering whether there are pain points for it, which Lean manages to get over more easily. That is somehow where I'm coming from. > For example, say you have a theorem about bimodules over semisimple ring= s > whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we can assume both= algebras > are multimatrix algebras over division rings.=E2=80=9D Is that step some= thing > you=E2=80=99d be able to deal with easily in Lean? If not, that=E2=80=99= s somewhere that > down the line HoTT might make things more practical. > This is a great example! To be honest I am slightly confused about why we are not running into this sort of thing already. As far as I can see this would be a great test case for the (still very much under development) transport tactic. Maybe we don't have enough classification theorems. I think that our hope in general is that this sort of issue can be solved with automation. Kevin > But mostly I just want to say you=E2=80=99re making a category error in y= our > question. HoTT is an abstract type theory, not a proof assistant. > > Best, > > Noah > > On Sat, May 25, 2019 at 9:34 AM Juan Ospina wrote: > >> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the >> "additivity axiom". Please let me know if the following formulation of = the >> such axiom is correct: >> >> [image: additivity.jpg] >> >> >> >> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>> >>> A useful example for you might be Floris van Doorn=E2=80=99s formalizat= ion of >>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>> in HoTT using Lean: >>> >>> https://arxiv.org/abs/1808.10690 >>> >>> Regards, >>> >>> Steve >>> >>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard >>> wrote: >>> > >>> > Hi from a Lean user. >>> > >>> > As many people here will know, Tom Hales' formal abstracts project >>> https://formalabstracts.github.io/ wants to formalise many of the >>> statements of modern pure mathematics in Lean. One could ask more gener= ally >>> about a project of formalising many of the statements of modern pure >>> mathematics in an arbitrary system, such as HoTT. I know enough about t= he >>> formalisation process to know that whatever system one chooses, there w= ill >>> be pain points, because some mathematical ideas fit more readily into s= ome >>> foundational systems than others. >>> > >>> > I have seen enough of Lean to become convinced that the pain points >>> would be surmountable in Lean. I have seen enough of Isabelle/HOL to be= come >>> skeptical about the idea that it would be suitable for all of modern pu= re >>> mathematics, although it is clearly suitable for some of it; however it >>> seems that simple type theory struggles to handle things like tensor >>> products of sheaves of modules on a scheme, because sheaves are depende= nt >>> types and it seems that one cannot use Isabelle's typeclass system to >>> handle the rings showing up in a sheaf of rings. >>> > >>> > I have very little experience with HoTT. I have heard that the fact >>> that "all constructions must be isomorphism-invariant" is both a blessi= ng >>> and a curse. However I would like to know more details. I am speaking a= t >>> the Big Proof conference in Edinburgh this coming Wednesday on the pain >>> points involved with formalising mathematical objects in dependent type >>> theory and during the preparation of my talk I began to wonder what the >>> analogous picture was with HoTT. >>> > >>> > Everyone will have a different interpretation of "modern pure >>> mathematics" so to fix our ideas, let me say that for the purposes of t= his >>> discussion, "modern pure mathematics" means the statements of the theor= ems >>> publishsed by the Annals of Mathematics over the last few years, so for >>> example I am talking about formalising statements of theorems involving >>> L-functions of abelian varieties over number fields, Hodge theory, >>> cohomology of algebraic varieties, Hecke algebras of symmetric groups, >>> Ricci flow and the like; one can see titles and more at >>> http://annals.math.princeton.edu/2019/189-3 . Classical logic and the >>> axiom of choice are absolutely essential -- I am only interested in the >>> hard-core "classical mathematician" stance of the way mathematics works= , >>> and what it is. >>> > >>> > If this is not the right forum for this question, I would be happily >>> directed to somewhere more suitable. After spending 10 minutes failing = to >>> get onto ##hott on freenode ("you need to be identified with services")= I >>> decided it was easier just to ask here. If people want to chat directly= I >>> am usually around at https://leanprover.zulipchat.com/ (registration >>> required, full names are usually used, I'll start a HoTT thread in >>> #mathematics). >>> > >>> > Kevin Buzzard >>> > >>> > -- >>> > 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, sen= d >>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>> > To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5= -a3b7-b585e33375d4%40googlegroups.com. >>> >>> > For more options, visit https://groups.google.com/d/optout. >>> >>> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-= b42b-b9a9f639d89e%40googlegroups.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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEY= KQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.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/CAH52Xb3k4fmuPfpDSO%3DJmb3k19v3m6MjOLweQb_u8n0icdt0rQ%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --0000000000000f07980589b815bb Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Noah. Thank you for pointing out the category erro= r. It seems to me that sometimes when I say "HoTT" I should be sa= ying, for example, "UniMath".

Tactics in= Lean are absolutely crucial for library development. Coq has some really p= owerful tactics, right? UniMath can use those tactics, presumably?

I understand that UniMath, as implemented in Coq, takes Co= q and adds some "rules" of the form "you can't use this = functionality" and also adds at least one new axiom (univalence).

On Sat, 25 May 2019 at 15:50, Noah Snyder <nsnyder@gmail.com> wrote:
I=E2=80=99d also im= agine that a =E2=80=9Cpractical=E2=80=9D implementation would likely have s= ome kind of =E2=80=9Ctwo-level=E2=80=9D type theory where you can use types= that behave classically when that=E2=80=99s better and HoTT types when tha= t=E2=80=99s better.

But plain C= oq has such types, right?

OK so this has all been = extremely informative. There are other provers being developed which will i= mplement some flavour of HoTT more "faithfully", and it might be = easier to develop maths libraries in such provers.

For e= xample, if G and H are isomorphic groups and you want to translate a theore= m or construction across the isomorphism.=C2=A0 In ordinary type theory thi= s is going to involve annoying book-keeping which it seems like you=E2=80= =99d have to do separately for each kind of mathematical object.

Yes. This is a pain point in Lean. It's a p= articularly nasty one too, as far as mathematicians are concerned, because = when you tell a mathematician "well this ring R is Cohen-Macauley, and= here's a ring S which is isomorphic to R, but we cannot immediately de= duce in Lean that S is Cohen-Macauley" then they begin to question wha= t kind of crazy system you are using which cannot deduce this immediately. = As an interesting experiment, find your favourite mathematician, preferably= one who does not know what a Cohen-Macauley ring is, and ask them whether = they think it will be true that if R and S are isomorphic rings and R is Co= hen-Macauley then S is too. They will be very confident that this is true, = even if they do not know the definition; standard mathematical definitions = are isomorphism-invariant. This is part of our code of conduct, in fact.

However in Lean I believe that the current plan = is to try and make a tactic which will resolve this issue. This has not yet= been done, and as far as I can see this is a place where UniMath is a more= natural fit for "the way mathematicians think". However now I= 9;ve looked over what has currently been formalised in UniMath I am wonderi= ng whether there are pain points for it, which Lean manages to get over mor= e easily. That is somehow where I'm coming from.
=C2=A0
=C2= =A0For example, say you have a theorem about bimodules over semisimple ring= s whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we can assume both= algebras are multimatrix algebras over division rings.=E2=80=9D =C2=A0Is t= hat step something you=E2=80=99d be able to deal with easily in Lean?=C2=A0= If not, that=E2=80=99s somewhere that down the line HoTT might make things= more practical.

This is a great = example! To be honest I am slightly confused about why we are not running i= nto this sort of thing already. As far as I can see this would be a great t= est case for the (still very much under development) transport tactic. Mayb= e we don't have enough classification theorems. I think that our hope i= n general is that this sort of issue can be solved with automation.

Kevin



But mostly I just want to say you=E2=80=99= re making a category error in your question.=C2=A0 HoTT is an abstract type= theory, not a proof assistant.

Best,

Noah=C2= =A0

On Sat, May 25, 2019 at 9:34 AM Juan Ospina <jospina65@gmail.com> wrote:
<= div>On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "addi= tivity axiom".=C2=A0 Please let me know if the following formulation o= f the such axiom is correct:

3D"add=




On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, = awodey wrote:
A useful exa= mple for you might be Floris van Doorn=E2=80=99s formalization of=20
the Atiyah-Hirzebruch and Serre spectral sequences for cohomology=20
in HoTT using Lean:

=C2=A0https://arxiv.org/abs/1808.10690

Regards,

Steve

> On May 25, 2019, at 12:12 PM, Kevin Buzzard <kevin....@gmail.com> wrote:
>=20
> Hi from a Lean user.=20
>=20
> As many people here will know, Tom Hales' formal abstracts pro= ject https://formalabstracts.github.io/ wants to formalise many = of the statements of modern pure mathematics in Lean. One could ask more ge= nerally about a project of formalising many of the statements of modern pur= e mathematics in an arbitrary system, such as HoTT. I know enough about the= formalisation process to know that whatever system one chooses, there will= be pain points, because some mathematical ideas fit more readily into some= foundational systems than others.
>=20
> I have seen enough of Lean to become convinced that the pain point= s would be surmountable in Lean. I have seen enough of Isabelle/HOL to beco= me skeptical about the idea that it would be suitable for all of modern pur= e mathematics, although it is clearly suitable for some of it; however it s= eems that simple type theory struggles to handle things like tensor product= s of sheaves of modules on a scheme, because sheaves are dependent types an= d it seems that one cannot use Isabelle's typeclass system to handle th= e rings showing up in a sheaf of rings.
>=20
> I have very little experience with HoTT. I have heard that the fac= t that "all constructions must be isomorphism-invariant" is both = a blessing and a curse. However I would like to know more details. I am spe= aking at the Big Proof conference in Edinburgh this coming Wednesday on the= pain points involved with formalising mathematical objects in dependent ty= pe theory and during the preparation of my talk I began to wonder what the = analogous picture was with HoTT.
>=20
> Everyone will have a different interpretation of "modern pure= mathematics" so to fix our ideas, let me say that for the purposes of= this discussion, "modern pure mathematics" means the statements = of the theorems publishsed by the Annals of Mathematics over the last few y= ears, so for example I am talking about formalising statements of theorems = involving L-functions of abelian varieties over number fields, Hodge theory= , cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ri= cci flow and the like; one can see titles and more at http:= //annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom = of choice are absolutely essential -- I am only interested in the hard-core= "classical mathematician" stance of the way mathematics works, a= nd what it is.
>=20
> If this is not the right forum for this question, I would be happi= ly directed to somewhere more suitable. After spending 10 minutes failing t= o get onto ##hott on freenode ("you need to be identified with service= s") I decided it was easier just to ask here. If people want to chat d= irectly I am usually around at https://leanprover.zulipchat.com/ = (registration required, full names are usually used, I'll start a HoTT = thread in #mathematics).
>=20
> Kevin Buzzard
>=20
> --=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 email to HomotopyTypeTheory+unsubscribe@googleg= roups.com.
> To view this discussion on the web visit https://groups.goog= le.com/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40go= oglegroups.com.
> For more options, visit https://groups.google.com/d/optout<= /a>.

--
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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-= b9a9f639d89e%40googlegroups.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/CAO0tDg4dy= jZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40mail.gmail.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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3k4fmuPfpDSO%3DJmb3k19v3= m6MjOLweQb_u8n0icdt0rQ%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000000f07980589b815bb-- --0000000000000f079a0589b815bc Content-Type: image/jpeg; name="additivity.jpg" Content-Disposition: inline; filename="additivity.jpg" Content-Transfer-Encoding: base64 Content-ID: <4dd9a01b-962b-4d4e-85eb-85540c4734a3> X-Attachment-Id: 4dd9a01b-962b-4d4e-85eb-85540c4734a3 /9j/4AAQSkZJRgABAgAAAQABAAD/2wBDAAgGBgcGBQgHBwcJCQgKDBQNDAsLDBkSEw8UHRofHh0a HBwgJC4nICIsIxwcKDcpLDAxNDQ0Hyc5PTgyPC4zNDL/2wBDAQkJCQwLDBgNDRgyIRwhMjIyMjIy MjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjL/wAARCAGAAsMDASIA AhEBAxEB/8QAHwAAAQUBAQEBAQEAAAAAAAAAAAECAwQFBgcICQoL/8QAtRAAAgEDAwIEAwUFBAQA AAF9AQIDAAQRBRIhMUEGE1FhByJxFDKBkaEII0KxwRVS0fAkM2JyggkKFhcYGRolJicoKSo0NTY3 ODk6Q0RFRkdISUpTVFVWV1hZWmNkZWZnaGlqc3R1dnd4eXqDhIWGh4iJipKTlJWWl5iZmqKjpKWm p6ipqrKztLW2t7i5usLDxMXGx8jJytLT1NXW19jZ2uHi4+Tl5ufo6erx8vP09fb3+Pn6/8QAHwEA AwEBAQEBAQEBAQAAAAAAAAECAwQFBgcICQoL/8QAtREAAgECBAQDBAcFBAQAAQJ3AAECAxEEBSEx BhJBUQdhcRMiMoEIFEKRobHBCSMzUvAVYnLRChYkNOEl8RcYGRomJygpKjU2Nzg5OkNERUZHSElK U1RVVldYWVpjZGVmZ2hpanN0dXZ3eHl6goOEhYaHiImKkpOUlZaXmJmaoqOkpaanqKmqsrO0tba3 uLm6wsPExcbHyMnK0tPU1dbX2Nna4uPk5ebn6Onq8vP09fb3+Pn6/9oADAMBAAIRAxEAPwD3+iii gAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKA CiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAK KKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAoo ooAKKKKACiq95eW+n2ct3dzJDbxLueRzgKKyZfFul21qLu7NzaWrLuWe4t3jQj3JHy/8CxmgDeoq vZ3cV/ZQXdu26GeNZEYjGVIyP51YoAKKKKACiiigAooooAKKKKACiiigAooqteX1pp8ImvbqC2iL BA80gQFj0GT3oAs0UgIIyOlLQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAJS0VQ1XV7LRbQ 3V+8scC/edIXk2j1O0HA9zSAv0VlaN4i0zxBB5+mTSzQEblla3kjVh/sllAP4Vq0wCiiigAooooA KKrPf2cd4lm93At1IpZIGkAdgOpC5yRVmgAoqrf39rpllLeXsyw28Q3PI3QCqOk+JtL1q7ns7OZj cwKryROhVlVuhwf5daANiiiq0t/ZwXUNrNdwR3E2fKieQB3/AN0Hk/hQBZooooAKKKKACiis+fW9 LtppIpr+3R4iBJlx+7z03H+HPvQBoUU0MGUMCCDyCKdQAUUlY9h4o0nUtauNItp5Tf2yeZLDJbyR lVzjPzKMjPcZoA2aKKKACiori4gtLeS4uZo4YYwWeSRwqqPUk9KIZ4rmBJ4JUlikG5JI2DKw9QR1 FAEtFFFABRRRQAUUUUAFFFFABRWLB4o0m48QvoKTyjUkjaUwyW8iZQHBYMygMM9wTWzQAtFRXE6W 0DzSByiDJCIznHsqgk/hWLo/jLQtfvprLTLuSe4gJEyfZpV8s+jFlAB9jQBv0Vg3XjDRbPWTo81x P/aAUP5EdpM5KnuNqEEe/St0HIoAWiiigAoqOaVYIXlcMVQZO1Sx/AAZP4Vh6b400LVr+Sxsbmea 5ifZKgs5h5bejEoAv44oA6CiiigAooooAKKKytb8SaP4dgE+r6hDaIeRvOWI9lHJ/KkBq0VV0/UL XVbCC+sphNbToHjkXOGU9+aik1jT4tWi0p7pPt0qGRIBksVHU8dB9afkBfoqtHfW0t9LZJKDcQqG kjwcqD0qzQAUUUUAcZ8TLDUr3wlv0uA3M9pcxXTWo/5bqjBiuO/TOPasiL4neC/FlhPoeo3D6dcX UZgktb+IoVJGME9PzIrqPFfiEeG7fTrqTiCa9jgmIXcQrZGfzxVLxtY+HtX8FX1zqKWs1r9nZorg YYhsfKUb1zjGKno+w+qDUtdi8BeG9LiuLS5vLeNIbU3EAQKG4QEgtkAn0zVzxH4ti8NXWmw3Nhcy x39ylrHPGU2LI54DZOexPSuI8U22oQfBHSV1FZDdQCza43AkoBImd30HWrvxYv7ZB4TjaZM/23bT E54CDOWJ7Dkc1fX5/wCRK2+R02v+MovD2tadptxpl7KdQcxwSwhCrOBnbjdnPTqAPerE3imCx1iy 07U7Waye+O21lcho5H/55kg8P7Hg9ia5X4iXdvB4t8CXMsyLANQcmQn5QCmM5/rR8U0Osf8ACP6D p/73U5tSiuVCcmGJM7pT6AZAz3zUr9Rv9DfuPGsdt4vTw02k37XkkJniZdhSRAcZzu4HXrjp9M3b bxNbSeIW0G7hktNRMfnRJJgrOncow647g4PtXJ6lcw23x70nz5Vj8zRpI0LHGWMnApfE6NrXxa8K 2+nDfJpPnXN9KnSFGUBVY9i2Dx+NNdAfU61vEMc+s3Ok6bAbu7tVVrlt+yKEtyFZsH5iOcAH3xUH /CZaZHY6pcXXm20ulf8AH3byKN6Z+6Rg4IbIwf5c1z3gGOTSPFXi7S9RbZeXOotfQF+POhccFfUD GDjpWBq8tpJ4s8Y+ILq3+1eHY7CDT7khsLM5dQ20jqUBPToeKXYD0O78QXNgbJrrS5BFeXEcCNHK GMZfoZBxj043Uv8AwkqXWs3elaXateT2QU3T7wkcbHkJu5y+OcYx6kVxU2j33hL+x77Q/Et9qenX F5DCNPvpFnV43OMxNjI2j5u/AqXwJp507xN4r0rUZ54L2bUnvYcSlPPhcDDL/exjB9OlNa/16Adz oOvWniGye4tRIjRStBNDKMPFIpwysAetX7i4htLaW5nkEcMSF5HboqgZJNYnhmx0i0m1V9JSYia7 L3E7yF1llwNxUknIHQ47g+laGvW6XXh/UbeWJpkltpEaNergqRge9KWiuC3MGXx/aRaNZ6w2n3Y0 69lWK3mO0ZLHCswz8qn1/SqnirWrMaFBL4m8LTTW32xUCFo5EV921H6g4OfSuUsbnQNX8IaL4d1D xhpKWdo0TyAsIpZFTBWMhm+Ug4ye+O1dF8WLq1HgqAi4i2veWzIfMHzL5g5HqMU3o/mK7t8jd8Re MIPC72S3OmX0sN3KkEMsAj2eY3RTucY+tWtW8QnSrqwt/wCyb66kvSVQW/lnaQMnducY4781V8Xa GninwVd2MTBpXiEltIp+7IvKkH6j9ayvAOqz+K7eHWrqJo2tYBaBWGP3vHmsPxAH/AaO4zai8Trf X97aaVZSXjWJ2XL7wiK+MmNTzucenA96o3vxAsbbwk3iOCxvLm0iLLOiBFeBgdpDBmHfjjNYHw40 86dNr2j6hcTwahHfyT7RKU82NuRIPUds1F4tg0TTvhZ4nGl70huJGcySylhPIWXcyEnkZ9KT2uNK 8reZ1Nx43tbTSLTWJ7G6TTbmREWc7crv+6xXOdv6+1dQrBlDDoeRXl3xFu7T/hU1qI7iEgtbbdrj nBXpXpdjIk1lC8bq6lBhlOQePWq7kJ7FTXNcsvD9gLy+k2o0ixJyBuZjgDJ4FU08TRQ67baPqFu1 tc3aF7Zw++OUDqA3GGA5xj8ayviLqrafp2nWy21s5vr2ODz7qMPHbnrvIPGfTPeuc8WNHpvjzwZ5 +oTXTwSTNPNKwAAMfGQAFXODUrcpnq1cF8UtcvdJ0O1itbKSRLm8gieYOoCguDgDOSTj6V2tjdC+ sYbpUZBKgcK3UZriPi4jN4XsJADsi1S2eRuyqG5J9uab3XqCZ0N94il0vRJdSudFvzHAu6SOMxM4 UDJbG/n86iTxdBJ4RTxHFp169s6h1hXyzKVJ4ON+PwzmtC2vI9QuLyxMavDFGqswOQ25ckfka8/8 J293baxd+CJ45Daadd/aklI4aA/Mi/mf/HaN20Lpc6bWvHKaDp9je32i6lHFdyLEB+7LIzHgMA5O fpmrl74rh0k2j6pZXNnbXTiNLh9rKjHoHwflz+IrnPjBKkPh/SpZGComrW7Mx7DdUnxTuIr/AMDn TLQrcXupukdpHH8xY5B3DHYDvR0v5j6/I6fVfEdrpt9Z6eiPc395kw28WMlR1dieij1/nRYeIYbn Wp9GuIHttRhjEpjY7ldD/Ejdx+ANcLc6ZNpHxL0O81OaRLSXTRZrcK5VUmGPlLds12Eem6OnjCG6 X7TPqsduyeYZmdYoz2YZxz24pr/MR0lcJ8XNRax8A3VvE2J750tI8dcucV3deV+O7211n4heFdBF zCYoZmvLgbxgbegP41NrtIpO12eg+HtOTSPD2n2CLtEECpj3xz+tXLu6hsbOa6uG2xRIXdvQAc1K OQMdKzvEFzDaeH7+4uYBPBHAxkiJxuXHIok92KK2Rm3HiqS30ePVzpcr2Mu0oUkBkAY4DMvQDnPB J9qtXHiKFdZOj2qJPqCw+e0TShML+pJ/D8a89fRn0LwzB4g8K+JL5rFtjppd1KJ7dgxH7tQRkHn9 K27fUJ9Z+Id5ZnytL+xWqNJIsaefcBuSN7AkIPan5C6XOn0fxJba3Z3ctrDN9otJDFPauAHRx264 +hzXK+BfEWpaprHiF7jSpwRfCL5ZEIiCjgElsn14FZ/gDU7e18V+KIVLyfa9TRYstliuz73PJHvU 3g2+Ojz+MWdAbhdU+WFjgtuxjFC3+X+QPt5/5nQXV/pH/CxrGyutEf8AtV4JGtr91QjYPvAEHI/E CtKLxAb1rxtOs2uYbORopXMgQswGSEGDk/XFcvrd3bL8ZvDitcRBlsrhWBccE4wDVK30Ow8QXer6 toGvahoV/FcOl1Db3AMLOv8AG8ZHQ0ui+f5lPcPiPrj6r8OrW7hsLlIri6hJ3FfkxLja3PXj6V0u seLovDOnpqN/oGoJE7LG7xCFiCeF3fP05ri/FWrT3nwisZtUeBLtryEErhBIFlxvA9DjNek6xp1r 4l8M3VgXSWG5hKBkYEZxwQab0Tt3/wAhb2uRar4k/sq0sZ20q+uTdusaxW/lsyMemcuB+IJrK1LU tKPjXRLfUdAl/tGVWNpdyCMiPjLDIYkH8KzPh7dXutQW8epROsuhb7Ryw4klHy7h/wAB/nS+Lbu2 j+JvhFXuIlZWm3AuAR8vFD3QujNnUPHEOmeKbfQJ9LvjcXSM1u6hCsuPT5uPxxV+y8SwXPiK40Ga 3lt7+KEThWIZXQnGVI9+3FcrrV1aD4z+Hd9xDlLK4By4+UkDFM+123/C98faIv8AkE7fvjrv6fWh dPn+o31+R0zeLreS71OCxs7i8GmD/Snj2gA4ztXJ+Zsfh71J4f8AEZ8RRx3VtYSJp00Xmw3RkU7u cbSo5VvzrhoNQ0/Qde8U2R13T9Ma+uM+TfAhkJQfvFOQGByePbrXb+C7PSdN8LWen6NfxX1pbrs8 +KVXDNnJyVPqelC2uDNTVro2OkXl0oyYYWcfgM1yHw3t1vfhlbT3QEsuoLLPcMwzvZmbJP4YH4V2 Gq2pvtJu7UdZoWQfiMVxfw5u49O+GUdveusMulrLBdK5x5ZViefwINLo7j7E3wn1Ca98FiGZ2c2V 1LaKzdSqNx+hx+FdfqOo2uk6fPf3syw20CF5HbsBXnPgLw1rbeCrea31q60hru4muzHHBGxZXb5c 71OOBn8an8f+HNbm+G1/anUrjV7lZo5zviRGKKwJUBAM8A03fqKO50UnjKG10611TULOSy0+7dEi kmkUSfMflLJ2B68En2rnjfC0+OV2iwyTTTaPGqJGB/z0JJJPAAH+TXUjWNGvfDVrqJEV1auEaGMK rsz9lUH+LPGK5mzu7Rvjnfnz4d39jRoPnGd3m9PrRtL7/wAhfZ+78zq9H8S22ralqWmmGW3vtOZR PFJgjDDKspHUEVFa+Jf7UW5m0iykvLW3kaNpt4QSMv3hHn72Dxk4Hoa47RpY7v4oeOLe3uohLNaw JEQ4+9sI4/OtP4WTxad4Ah029ZLe80tpIryOQ7TGd7Hcc9iCDnvSWquN6M0dX8SaRqPge81NrCXU 9NCOt3bBVDIFzvDqxHIxyOtWI/EWjaJ4JsNVERtdPeCL7NbRplzvA2Rqo6tyBiuB02KS3+HXj7U7 giCz1Sa8nshIdu9CpAYA/wB7qPWl1qN5PAXgDWIv39jpU1pPeiP5tiBACxx/d701/l+IP/P8D0Jv E6Wl/p1nqlt9il1JilqpmV2LAZ2sB0P0yPeki8ULf3l/BpFlJfLYP5dxKHCJ5gGTGhP3mHGeg561 bu7zTJGsJisV1LM4Fo0YV256up9AOSR2rh/hjp/9n2esaLqFxPBqVtqE0siecUMkbEFZQM8g+vtR 1Dpc7zQtbsvEOkw6lYMxhkyCrjDIwJDKw7EEEVJq+q2miaVc6lfPstrdN7t7VneFLLSbLTrldGjm W1ku5JS8jlhK5PzOpJOVJz+X4ml8R9ZOh+CL67FjDe7tsRjuF3RDcwXc47qM5pPyBFiTxbBZ3Olp f27QW+qOI7S5SQSIzsMqrEdCecYyOOtM8VeM7fwk9ib6wu3trudIBcxBSqO2cAjO49D0BrivH8As dM8IRz6o97OutWkzSYVI1jBI3BUAVUywAPuOTVz4h6vZ6hp/hScukaHxHB8sjjlEd13/AO6cZz70 +3rb8g/yOvl8VRWesaZp+oWVxatqe4WzsVYblGSrYPynH1HvVi+8RW1rrMOjwRSXepSp5vkxY/dx 5xvck4Azx3PoK4/4g3lsPF/gQm5hwNRdj844Gzr+oqTSY30z4za5LekCPV7SB7CUn5XEYw6A+vIO PTmhasHt/XcYLtrn462iSW8kEsWiSBlfBBBlGCpHUV6RXmU+oWbftAWyi5i3JojRN8w4fzc7frjt XptC+FfP82D3YleQ6xcTeAvi6t1ZwrJa+JovL8kuFUXKnAJPYcjP+8a9C1/xVpfh+NUuLqA3kziO 3tfNCvI54A56Dnk9q47x/wCEGvvA99qd3cx/27BtvI7nOFiaPkRoT0XGQPUnJ5pXs+boO19DudI0 gaeJLm4cXGo3BDXFwVwWPYAdlHQCtWua8DeKIPFnhSw1JJIzO8QE8atyjjhhj6iukqmrOxK1Rkap qeo2eqabbWmjyXlvcuVuLlZVUWwA4JB+9n2rYrH1TxBFpWqabYPY307X7lFlt4d8cWB1c5+UVr0u g+pDeXMdnZz3UpxHDG0jH2Aya8/+Dls8nhq91ucfv9WvZblie4zgfyzV34s65HpHw/1NEnRbq5QW 8aFwGJc4PH0zW/4SsIdL8J6ZYwOjpBbom5DkEgc0R6sH0Rt0UVh3Hhe2uLiSZtQ1hC7FisepTKo+ gDYFAG5WBDrksXi640a+EcaSRrLYuBjzVx869eWB/Qik/wCEStP+gnrf/g1uP/i65DV/CcHiHxPF o9tqGqrDpxS4ubl9QlkZHP3UTcxAOOSaFuHQ9OrhPijdbfDyaVbIp1HWJVsoTj5gpOWP0Art4IRb 28cId3CKF3SMWY+5J5Jry7U9XtG+O9rb6tcR29tYaeXtjO4VDI2CSCeM44/Clu0g1SbPQtPtbTw3 4cgttyxWtjbhSxPAVRya8++HU58YeIfEni1kUxTN9isxIMgRqP696m8dajN4k8Pai1q7R+HrSBpJ 7kcfa3H3UT1TOMt37ZrV+EVtbWnw40uO3kiZmTzJRGwO1mOSDTWrbf8AVxPRJIzNK+H+o2fi6S9l lge1TYyxMhNv34jTflSvYnPtXplLWVd+ItKstbtNGuLoJf3aloIdjHeB15xijyH5mrRRRQBDNbw3 Bj86JJPLbem5c7W9R6Hk1RTw5okd99tTSbJbrdu84QLvz65xWpRQA10WRCjqGVhgqRkGqB0LSWgM B0y0MRYOU8lcZHQ49a0aKAOB8ZaPqeoeJvDM+n6S01npVy0spDooZSuMKCe3viuzs7C0tFLW1nFb M+CwRApz74q33ooWgbnn+oaPqd18VLbWX0dptLj097Jy0kZ3Fnzu2k/dx+PtXcWtnbWUfl2tvFCm c7Y1CjP4VYooWisHW5WurC0vkC3dtDOo5AkQNj86cbS3NuLfyI/JGMR7Rt45HH4VPRQBVh02xt7h p4bSCOVurrGAT+NLd2FnfqFu7WGcKcgSIGx+dWaKAGIixoERQqgYAAwBWT4p0u61rw1fafZXP2e4 mTCyZIHUEqccgEZBx2NbNFALQ5YR/wDEsWxk8IbiEEZjBhMHT1Jzt/4Dn2p3hXwsmj+GbTTtRS3u ZYix+7uWMMxYIpPOFzgfSumpaAGRxpFGEjUKijAVRgCmwwxW6bIY1jXJO1VwMnk1LRQBWutPsr7b 9rtYZ9v3fMQNj86WaytbiNY5reKRF+6rICBViigCo2l2DRrG1lblF+6pjGBViKKOGMRxIqIOiqMA U+igCOaCK5iaKeJJI26q65BquulaekAgWytxCG3BBGMZ9cVcooAQAAYFNlijniaOVFdGGGVhkEU+ igDC1VNS0q1tR4e061eMTj7RCFCny+5QZUZ+pqxpNnMs11qF3GI7m6YHZnPloBhVz+p961aKAOG+ I+k6prljp1ppuntcGG9iuXYyKo2qeRyetdVYWNpGBcpp8VrcSDLjYu4exIq9S0LRWB6kc0EVxEYp o0kjbqrrkH8KZbWdtZReXa28UKZ+7GoUfpU9FABVM6Vp5k3mxt9/Xd5YzVyigBAMDjpTXRJY2SRQ yMMFWGQafRQBUTS7CO4+0JZW6zDjeIwD+dLc6dZXrq91aQTMn3TJGGI/OrVFAEC2lsk/nrBGJtu3 zAgzj0zTW0+ze7W7a1hNwowJSg3D8as0UAVW06yebzmtIGlzneYxn86ZJpOnSsGksbdiCWBMQOCe 9XaKAK09haXIXz7WGTaMDegOKyL+XWdO1O0j0vTIJ9LaN/OWPCyLJ/DjLAbfXqa6CigDO0ewbT7H ZKVa4lcyzMvdz1/oPwqeXTrKabzZbSB5Ou9kBP51aooAqPpti83mvZwNJ13mMZ/OkbTLIyGUWkAm PPmCMbgfXNXKKAOM0TTLvQLe4tb3R31KR55JftkBjZpQSSN+9lIIGB3HHap/DXh+aw8Q6pq/2aLT 7e9VFSyjI6rnLvjjcc44z9TXWUlCAWs+50TSru4+0XOnWs03H7x4VLcdOSK0KKAEAAGO1LRRQBUj 0yxhuWuYrOBJ2+9IsYDH8aBplis3nCzgEuc7xGM5+tW6KAKsWm2UM3mxWkCSf31jAP50lxpljdTL NcWcEsq/dd4wSPxNW6KAIZrW3uYxHPBHIg6K6ggUQ20EEPlQwpHH/cVcD8qmooAq22m2Vk7va2kE LP8AeMaBSfrii606yvmRrq0hnKfdMkYbH51aooARVCqAAAB2FI6LIhR1DKwwQRkGnUUAUk0jTYre S3Swtlhk+/GIhhvqO9Pl06ynKmW0gfaAF3Rg4Aq1RQBUfS7CUqZLOByowpaMHAqSeztrqEQz28Us YxhHUED8KnooAo/2Ppgmhm/s+282EBY38oZQDsD2q9RRQBUl02xnl82WzgeTruaME/nU00EVxEY5 okkjPVWXIqWigCvb2NpaEm3tooieuxAufyqxRRQAUUUUAVp9Ps7p99xawyt6ugJ/WpYoY4IxHFGs aDoqjAqSigAooooAKiSCGKWSSOJFeQ5dgACxHHJqWigArNv9A0fVLmK51DS7O6nh/wBXJNCrsn0J HFaVFAFe5sbW8s3s7m3iltpF2vE6gqw9CKSx0+z0y0S1sLWG2t0+7FCgVR9AKs0UAFRtDE0qytGp kUYViORUlFABRRRQAlFch8S9b1Dw/wCCrnUNLuPs90kkarJsVsAuAeGBHQ1Q+IHjGbRrfTtP03Vr Gz1G8uY4pZZmRjbRtnMhQnge54oA7+isjw2LkaJC11rcWtO5LC9iiSNZFzxgISOOma16AQUUUUAF FFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUU UUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRR QAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAef/GX /knN5/11h/8ARgql8RtL0+fUfCU0thaySz6rDDM7wqWkjwfkY45X2PFdL4/8OXfirwncaVYyQRzy PGwadiFwrAnJAJ7elN8U+HLzW5vD720kCjTtQjupvNYjcq5yFwDk/XFJbfP/ACB/ozo7W1t7K2jt 7WCKCCMYSKJAqqPYDgVPRRTAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKK ACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooA KKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAo oooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACii igAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKK ACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooA KKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAo oooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACii igAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKK ACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooA KKKKACiiigAooooAKKKKACiiigAooooAKrt94/WrFV2+8frQBYooooAKKKKACiiigAooooAKKK8m +JI+IfhrS9Q8Q6R4wR7GKTebJtPhDQxlsAK5U78ZHXFAHrNFfPnw31/4nfEOa8ZPGEdjaWm0SStp 8EjFmzgKuweh5z+de33Vjqkvh0WVvrBg1PyUT+0fsyMd4xufyz8vODx0GaANSivm/wCIXi74nfD/ AFuKxuPFcd3DPH5sM6WECbhnBBXYcHPua9J+Hlp49v7TTNd8ReK45rS4iE39nR2MI3o6ZTdIoBB5 DYHpjNAHo9FFFABRRRQAUUU1WDDIz1I6UAOooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKK ACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooA KKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKrt94/WrFV2+ 8frQBYrxz4l+KPHXgOWzu01awuNMvLho9/8AZ+02/cA/Od3y59M7TXsdcR8WbGy1L4c6na3j7ZXC /YwFLO9wD+7RAOSWPy8diaAG+K9X1zR/BVkdO1W1ufEFxIiW+20yL1j/AAom75Rg7t2SAFOetafh mz8YRkT+JtW0+bdFg2tnaldj8c+YW5xyMbe9cN8C5odc0I6nfXEl1q2ngaeizf8ALrCANoQdt3c9 Ttx0Fev0AFFIeB0rmP7f8TZ/5Euf/wAGMH+NAHUUVy/9v+Jv+hLn/wDBjB/jWhpGpatfTSLqOgya cirlXa6jl3H0wpyKANiuK+Ln/JKtf/64L/6GtdrXFfFz/klWv/8AXBf/AENaAPPv2af+QV4h/wCu 8P8A6C1e7V4T+zT/AMgrxD/13h/9BavdqAPnD9pT/kYdD/69JP8A0OvcvBf/ACInh7/sGW3/AKKW vDf2lP8AkYdD/wCvST/0OvcvBf8AyInh7/sGW3/opaAN2q15ewWFs1xcsyxL95lRmx+ABNWaayhl IIyDwRSYGXo/iPSfECu+lXi3SIcM6K20H0yRjNMg8U6Lc6pJpsN55l7GdrwrE5KH344rzXQJ73wZ 4+1nwfZRBo9Rb7XYM5G2IN94nPUD07mvUdJ0i30m3ZYxvnkbfNOw+aVz1JNPdJi62LVzeWtlGJLu 5igRmCBpXCgk9Bk96nGDXK6trmgXepWOmalYm5WW7MVvJJErR+cgzxk549cV1QGBxR0uMWiiigAo oooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACii igAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKK ACiiigAooooAKKKKACiiigAqu33j9asVXb7x+tAGL4l8ceHPCKga1qcdvK0ZkSAAtI456KPcEelc 94Gvrfx9ct4wuJ0lEEjw2FiORYjoWf1lYYOewIA6mvQSiswJUEjoSOlIkaRghFVQTk4GOaAPnvQf FOheCPjhrMdvqdudA1XJklRv3cEvLc/Rt68dmr3+yvbbUbOG8s50ntplDxyxnKsPUGpHhilULJGj qDkBlBApyqFUKoAA4AHagBeccVzH9keMf+hssf8AwT//AG6uoooA5f8Asjxj/wBDZY/+Cf8A+21o aRZa5azyNqus21/GVwiRWPkFT653tn6VsUUAFcV8XP8AklWv/wDXBf8A0Na7WuK+Ln/JKtf/AOuC /wDoa0Aef/s0/wDIK8Qf9d4f/QWr3WvCf2af+QV4h/67w/8AoLV7tQB84ftKf8jDof8A16Sf+h17 l4L/AORE8Pf9gy2/9FLXhv7Sn/Iw6H/16Sf+h17l4L/5ETw9/wBgy2/9FLQBr3FzBaxiSeVIkZ0j DOcAszBVH1LEAfWsjWfEdvYTw6bazQS6vcnbBbGQAj1ZvQD9a3CAetZw0HSFuxdjTbUXAO4S+UNw PrnFIDzT4j6A3h7TtP8AGFvN5uq6bciW5nc4MyNww+g6AV6hpWpW+r6XbX9tIrxTxh1KnPUU6902 y1GMR3trDcIDkLKgYA/jRZadZadGY7K1ht0PJWJAoP5U1tYHvc88uZbeX4mvIYCtjoMKrFCi48y4 mPUDuQK9MVsjoQaqnS7Br8X7WcBuwMCcoN+PrVyhbWB73CiiigAooooAKKKKACiiigAooooAKKKK ACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooA KKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAq u33j9asVXb7x+tAFiiiigAooooAKKKKACiiigAryP4nar4v13R9S8N6P4Mvnhlk8p713Xa6KwOUX 3wOTXrlFAHgPwpg8U/D+y1KC98F6tdNdyI6mExjaFBHOW969D/4TzXf+ie6//wB9Rf8AxVd3RQB8 5fFXSfFvxA1PT7qy8HaparawtGyzbCSS2eMGvRPhzrviqOx0rw/rvhG8s1t4RB9vDr5YVE+XcvUE 4A4zzXpNFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABR RRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFF FABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAVXb7x+tWKrt94/WgCxRU HmN60eY3rQBPRUHmN60eY3rQBPRUHmN60eY3rQBPTHdY42djhVGST2pqOxYAmsjxjcPbeDtXmjOH W1fB/Ck3ZXGld2Kvhm6n12WfXJXcW0jNFZwgkKIwcbyO5JH5VqXb6wNXs0tIrM6aQ32p5WbzQe2w Dj86o+GIng8DabHahfMFkmzceNxXPP41z3hq61G4+IOoWovZ5rOxtES73yFka4bk4B6YHpTa96xN 9LnoNFJisfSfD0Gk6nqV9FdXcr38gkdJpNyoR2UdqBmzXC/EnxBqnh3TrKbSbvZeXVyltHC8asrE nk8jOce9dzXmfij/AInnxf8ADWkD5otPje+mHo3RaXVINk2djd6bqEmhlf7RlfUIx5kc2AvzjthQ AV7YNTeHNZXXdEgvgoSRspLH/ckU4YfmK1e1cl4DjEK+IoVPyR6zMFHoCkbfzJovrYLaXOuoqORi uMUzzG9aYE9FQeY3rTkdiwBNAEtFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFF FFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUVi +KPEMPhXw/c6vcQyTJDtHlxkAsSQByenJrN8XeJrzQZPD4tIoHGo6jFaS+apO1G6lcEc/XNAHWUU UUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFV2+8frVim7FJzigCCip/LX0o 8tfSgCCip/LX0o8tfSgCCip/LX0o8tfSgCJPvioNYsRqWjXlkf8AlvC0f5jFXAig5Ap1J6qwLRnN eBblp/CNnBLxc2im2mU9VdOP5YNZ/hjwnqOj3Vx9puI2jkvZLtpY3O+cn7oYY4A9Mmukg0qK21Wa +t3aP7Qo86IY2uw6N7GtCnfW4ulgrG0nSdQsNU1K6u9XmvILqQPBBIoAtxjoP8itqkoGMmMgiYxI rSAfKrNgE/XBxXEaJ4Y1y08faj4jvxZSC8jWFVSVswoOcDK8/pXdUtC3uHSxHPKkEEksjBURSzE9 gK5f4fwy/wBiXd/MCP7SvpbtAf7hwq/mFB/Gt3VNNXVbX7LLK6QMw81U/wCWi/3T7GrkcaRRrHGo VFGFUDAA9KXmHkJL2qKrBUN1FJ5a+lMCCnR/6wVL5a+lARQcgUAOooooAKKKKACiiigAooooAKKK KACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAoooo AKKKKACiiigAooooAKKKKAPOPjRplnd+BZb2eHfc2bp5D7iNm91DcA4OR65rI8feHbTSdD8KaTog awR9Yj8tldmMbtn5gWJPXmu2+IOhXniPwVf6bYBWupAjRq52hirBsZ7dKwNa03xL4ksfDE1zoX2O 6sdXimuYRdxybYl6uGBGfoMmku3mge3yZj+NPCeneB7PT/EGhPdwalHexJLM1w7m4Vjzvye/t70/ 4ja/YyeNrHw/rmqT6foKW32i68kPm4YkhUOwE44/n7V1XxJ0PUdf8NQ2mmW3nzreRSlN6r8qk5OW IFReJ/D+sxeJrTxV4cSCe+hgNtcWcz7BcRZzgN2YH19vTBPXv+gL9DhNP8QeFNB8ZaKvgjU5ms72 4Fte6ewm8v5sBZB5g6gn1/rWra+HLfxL8V/FlrqEs505BbvLaxymMTtswu4ryQPm4yOTXT2Nx471 jW7WS7sLfw/pcB3TxefHdS3H+yCBhR+Rp/h/Q9RsviH4n1W4ttllerALeTep37VweAcjn1FNb6+Y ns/kY3hGyXwx8TtX8N6dLMNJayS7jt5JC4ifIB2k9uT+npXpdcbbaHqMfxYvdbe3xp0umrAk29eX DA425z0HXFdlR0QdWLRRRQMKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKA CiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAK KKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAoo ooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiii gAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKA CiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAK KKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAoo ooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiii gAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKA CiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAy9X1200ZU89LmV3yR HbQNK2B1bCjpSaT4g07XNx02Zp41ALSBCqgn+HkDn1Haual8U60/xEbwvaw6e+21+0vcMj/u1zgK Ru5PT0q5rupeJNBsEvIodLuY/PjjkRUeMgO4XI+Y5OWHFC/MH2OupK4uHxJrc/i660lorKC2trYX M8rBmaIFm2jg4JKgH2rX8Ia1ceIPDNpqd1CkUswJwgIBXJwRk8ZHNAGrPe29vc21vLIqy3LlIV7s QpY4/BTViuH0+U678UdQuSc22iQi2hHbzZBlz9cYFdxSXcGLXJ+LfHUHg9wbrQtcvbfyvNe5sLQS RRjJGGYsMHjP0IrrKayhlKsAQeCD3pgeSRftE+FJpUii0rXpJHO1UW3iJY9gB5lejeHdd/4SHTDe /wBlanpoEhQQ6lB5Mh4B3Bcn5eevsa+afg5DF/wumFfLTbGbnYNv3cK3T0r6toA8x1j426PoE4i1 Xw34nsyxIQz2SIHx1KkyDNM0z456Jrc7Q6V4c8T3sqjLLbWUchUepxJxSfH+NH+GUjsilku4ipI5 U8jj04NUv2dI0Hw+vZAih21KQMwHJAjjxz+JoA9fooooAKKKKACiim4+bdzzxQA6qVvqdrc6jeWE b/6TaFRIh64ZQwI9ufzBq5XEeMXOgeING8RxZVGmFleAfxRv90n6H+dHUDuKKQHIzS0AFFcbqPj8 W+oXNtpnh7WNZis5DHdXFjCrJG46ouSN7DjIHSt7QvEGm+JNOF9plwJYtxR1I2vE46o6nlWHoaAN SiqUupRRaxbaZhjNPBJOMYwqoUBz+Mgq7QAhIUEk4A6mvJvE/wAXrmXWW8P+A9MOtampKyT7S0MZ 74wRnHqSB9af8Y/EuoD+zvBOgsf7U1o7ZSnVIScfhu559Fauy8EeC9N8D6BHp1igaVsNc3BHzTP6 n29B2FAHkPi3S/ixpvhe/wDEet+LhbLbKrC0sZCh+Z1XGUCgY3ep6Vb8O6Z8Wl8K2Ov6P4oi1NLq AT/Yr753IIztDOD/AOhLXefGb/kkmvf7kX/o5K0fhn/yTPw7/wBeMf8AKgDmPB/xdGoav/wj/i3T jomtDhd+VilOegzyp/Eg4616lXGfET4f2HjvRGikVYtTgUtZ3QHKN/dPqp7j8ayfg94tvtd0K60f Wd39s6LL9muPMPzsMkAt6kbSCfagD0miiigAorF1aHxDNMG0m7sbdI1BCzwmTzW9CQRtH0yefzta UNUNuz6sbZZ2PEVvkog+p5P6UAaFFN3qASWHHHWnUAFFQ/aYDdG1EqGcJvMYPIXOM49KmoAKKKKA Ciiobe5huoy8EqyKGKEqc4IOCD70ATUVD9ph+1G281fPCb/LzztzjOPTNTUAFFFFABRRRQAUUUUA FFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAU UUUAFFFFABRRRQAUUUUAHek7UtZeu3F9Bpk39nWcl1dPGwjCsqhWxwSSemfrSb0BHm3gybU9S8X+ MfE1jbW06vc/ZIXnmKDbEO2FPHSu18NGS78LWUmvGM3V9J55ic8By3mKqg/3cDA9qxvh/p+p+EvC Nvpl1ol293ueSd43jIZmYnglq1tMi1rVfEzahq2nrY2VnGUsofNDs7N952xwDgAAe5qttBeZfPhi wa41mdzKz6ugjuCWxhQmwBcdOM/nU2haFbaBY/Zrd5JOAC8hGSAAAOABgAAVrUlIZwXwxPnHxNdn 70+sznPsMAfyrupJooSgkkRN7bE3MBub0HqeK4T4bj7LqHizT24aHV5HVf8AZYBga7HUHtlez+02 b3JNyoiKwGXynwcOeDsA5G7tn3o6L0X5C6v1ZeooooGfKnwb/wCS1r/29f8AoLV9V18q/Bv/AJLW v/b1/wCgtX1VQB5f8fv+SXz/APX3D/M1T/Z0/wCSdXf/AGE5f/RcVXPj9/yS+f8A6+4f5mqf7On/ ACTq7/7Ccv8A6LioA9cprruQqcgEYyDg06koA8ve+v8Aw98XLfTtS1a9fRr+AvZLJOdqyDqrHv36 10RtLzxNrYv7bVL+z0iEbAsEpUXTf3h6L7jrXK/FGzuPFmhSX+lQRyQ6NJ56zMM+eR95U/2cdT3r v/CmsW2veGNP1G02iKaFTtUY2nHI/OiO3oEt/U0LiKUWEkNrOIpthWOWQb9rY4JyeaZpcF7b6bBD qN4t3dquJZ1jEYc+u0dK4f4nxuNO2B/MutQeOysYgP8AVMTlpPrgV3lhEYLCCEyeY0caoXJzkgYz QtmwfRFmuM+KkYb4darL/FAiyqfQhga7OuN+Kbhfhxq8f8U0axKPcsBUscd9TpNIm+0aNZTE5LwI x/FRV6qOjQ/Z9FsYSMFIEXH0UVeq5bkR2OQ0fxF4N0DSbfS08VaITbrtdmvoVZ3zl2I3dSxJPuax Nam8GX2qNrGj+PtM0TWHULLc2t/AyzqOgljZtr49evvW5L4gCyup8Ea25DEbxbW5De/+spv/AAkK /wDQia5/4C2//wAdpFEfgwaJ9vupo/F9t4j1y4jXzp1uImZYlPCpHGcImWzx1J57V2lYGi6qL68e MeGtS0zCFvOuoYkU8j5QVcnPOenat+gD57vPF+j6H+0RrOreIZ3S3srcW9r5cRch9iDoPYyH8a7j /hfXgP8A5/rv/wABX/wrnLizsNK/aRni1eytriz120XyBcQh1WTao4yDzujYf8Cr1f8A4RPw5/0L +lf+Acf/AMTQB5D8SPi74S8SeANV0jTbq4e7uFjEavbsoOJFY8n2Bq54K+Mng3RPBWj6Ze3dwt1a 2qRSqtszAMBzg962/i54d0Sy+Fut3Fpo+n286LFtlitkRlzKg4IGR1rQ+HfhvQrr4daBPcaJps00 llGzySWqMzHHUkjk0AUv+F9eA/8An+u//AV/8K4/wT4l0rVP2gr680GaRrDVbNi6shT94qqTwfdS fxNeyf8ACJ+HP+hf0r/wDj/+JryjwXa22rftA6/f6ba29vp2kQG2VbeMKu/hP4RjJIkP4UAe30hw QQelFUdav00rRb2/kOEt4XkJ+gzSbsrgtXY818HadZ654+8WXkkSvpdnItrBCSTGGA+dgOmcj9a6 G+8N6fqTaLqeiQtCI7xHZ4GKBowTnI7jiue8AeDl1P4ZPPcPOl7q5luWK3Dou5ycEgH2BrvdNni0 65svDlsm/wCy2amVw3+rUYVcj1bn8jTtay7W/wCCK97vozz1LSKysfG2tC1knS2zZ2iOC2WVPncj uSznJ+tdv4fvotL8BwTTSSPFp9qFeZ/+WmxBuZT3XIOD7V0u1cEbRg9RjrXMfEUEfDrXRGMf6HJ0 9MVLdkykrtEngmCV9Cj1e8Gb7VMXUxP8IblEHsq4H5+tO8aeHF8R+HLy2iPlX3lN9mnU4ZH6jkds gZrT0TaNB0/Z937NHjHptFQ6vqxsfLtbWMT6jc5EEGeOOrMeyjufwHJpyV9ETB9TgfAfiNNV8BW2 j2lsja389rdwyZIjZflaWT2xj6nge3beHPCun+GrNIrbzJpwuHuZ3Lu/ryeg46DivP8ARYJvAPxd ksbubzbPxLF5qzbQo+1KcsAOw5OP94V6reW5urKe3ErwmWMp5kf3kyMZHvTb05gtrymWEtdS8Rw3 lrrsjGzjZZLC3nUxvu43Oo5JBBx7is29mOgePrBlO2y1xXhlTsLhF3I/1ZQyn/dX0rF8Em2vfGmt 6zGyRWcRXRdOQHAcRAs+PXnP5GtH4h4+0+EtufM/t6324642vn9M0u39bj7/ANbF/wAdJLaaE2u2 YP23ST9qTb/HGP8AWIfZkz+OD2rorS6ivbOC6gbdFNGsiH1UjIqj4l2f8Itqvmf6v7HLu+mw5qj4 A3/8K+8Pb87v7Pgzn/cFNdRPodHRRVHS7u6vLeZ7uza1dLmaJFY53osjKr+24AH8aBl6iiigAooo oAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiig AooooAKKKKACiiigAooooAKKKKACiiigAooooA4w2cujfE5buOMmz1yDypCBws8SlgT9UB/KuypC oLAkAkHI9qdS8gYUUVnarrmlaHbST6nqFtaIiFz5soUkD0B6/hTA+Zfg3/yWtf8At6/9Bavquvk/ 4N3cA+MEd00qpCy3DB3IUYKnHX619Sf2tpv/AEELT/v8v+NAHnfx+/5JfP8A9fcP8zVP9nT/AJJ1 d/8AYTl/9FxVJ8d7+zuPhnNHBdwSv9qhO1JAx6nsKx/2fPEWkWvhK80m51C3gvRetMIppAhZGRAC MnnlT09qAPcK5nW9A1nUtMj0+18QPbRCNUlmaBWlmwMHc3AG7vgDrXTUUAUPsDJov2GIxKwi8sHy /k6Y+7np7ZrnvBHg688GWstkNVF3ZPI0ojaHaULckA56fhXYUUdbh0sc54h8MPrOq6XqUN2sFxp7 OUEke9fmGM4yOR2NbGn2MenWUVtEWKxrjLHlj3Jq3RQAlcR40U67rejeGofmDTi8u8fwRJyM/U/y rtm3bTtIBxwSKydH0T+z7i6vrqcXWo3bAzT7NowBhVUdgB/iaFuHQ1wMDA6ClxRRQAUUUUAFFFFA Hn3xW8ET+LNDhvNKPl63pjme0deGfHJTPYkgEe496j+G/wAT7TxbbjTNUK2PiK3/AHc9tL8hlI6s gPfg5XqPpXotcL40+FXh/wAZzG9kEljqoxtvrbhiR03Do314PvQA34zf8kk17/ci/wDRyVo/DP8A 5Jn4d/68Y/5V5trPwz+KNxo1zoaeL7TU9JmCqyXhYSMFYMOSjEcgfx0/T/hl8TLjSbXRdR8ZW+n6 RBGIkisdxcKB0OFTP4saAOh+JXxNXRwfDnhv/TvEl3mFEg+c25PGTj+Prgdup99z4ZeCT4J8Kra3 DCTUrpzPeSg5y5/hz3AHH1ye9O8FfDPw94HXzbGFp9QZdsl7cHdIQeoHZR9PxJrsqACsXxH4dj8S 6bJp9ze3UNpMhSWOAgbwfUkZraopWC5z9n4alsNOhsbbW7+O3hjEUaqsfyqBgc7PSpfD/hq18Pi7 eKe5uZ7uXzJp7mTe7EDAGfQelbVLTuIKqalYx6npl1YzDMVxE0bD2Iwat0Umrqw9jl/B0k7eGl0i 5kaLUNOX7HKwHI2jCOM9QVwfz9KsaP4Wi0nWbvVP7Rvru4ukCSfaZAwAByNoxwOTwK2fskAuzdCJ ROU2GTHJXOcZqan5i6WOY8T+CbLxVeWNze3l5E1jIJbcQOF2OP4s4znpXQ28LQ26xSTPMwGDI4GW +uABU9FHSwzntC8IWHh9lFtLM8UTyPBFIQVhMjFmxgc9cZOSBxVG/gOvePdOjQbrPRA9xM/Y3Drt RPqFLMfqtddUNtaQWcbJbxLGrOzsFHVickn3zQBzvjp5rnQX0Ozyb3V/9EjA/gRv9Y59lTJ+uB3r orO1isbKC0gGIoI1jQegAwKPssH2z7X5S+fs8vzMc7c5xn61NQgFooooAKKKKACiiigAooooAKKK KACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAoooo AKKKKACiiigAooooAKKKKACiiigAooooAKwta8HeHfEd1Hc6xpFtezRp5avKuSFyTj8yanvtY8jV bXTLaITXcw3sM4EUY6sT+gHep9W1iw0Owa91K5W3tlYKXYE8k4AwBmkBgf8ACrfA/wD0LNh/3x/9 ej/hVvgf/oWbD/vj/wCvXVxuskaupyrAEH1FPpgch/wq3wP/ANCzYf8AfH/16P8AhVvgf/oWbD/v j/69dfVPUb8abZSXTwTSpGCzCLGQB1PJFK4Fyiuf0LxRB4n0w3+k2tyYGUmKWdQiuRxjrn9KvaPq 8Wr2jSopjmicxTwseYnHUH/PSmBpUUUUAFFFFABRRRQAUUUUAFFFFACUUtc94y1eXR/D8j23/H3O 628Hs7nAP9aQG3FcQzlxDNHIY22vsYHa3ocdDU1ZumWVtoWjRQF1SOFMySucZPdifc81BpEEL399 qVvrU9/DcMAIfOV4oMdQgHSn1sLpc2aKinnitoJJ5nWOKNSzs3QAd6g03U7LWLCO+0+5S4tZRlJE 6GgZbooryy9s7fWvjbDYRxgWljZGe7jThZXY4XcO/ahb2Dpc9PNxD9o8jzU87bu8vcN2PXHpUlcv 4yt2stCXVbBRHc6XiaMKMZQfeT6EZrobK6jvrG3u4v8AVzxrKn0YZH86ALFFFFABRRRQAUUUUAFF FFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUU UAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFABRRRQAUUUUAFFFFAHF+DJ P7T1vxHq0nzMbz7LGT/CkY6fmam1fxjFY31vbtYC4tpr1bMPv+YyHk7VxyBx3qv8Pl+zS+IrFv8A WQ6nIxHswBFZWvXBl+KFt9ohJh0y0M1rD/z8TucDb64pLogfU9KrHurzWo/Elna2+nRSaS8bGe6M mGjbsAvetWMu0SGRQrkDcBzg1k3et3Ft4ls9KTSbqWC4jZ2vVx5cRHY/Wn1DobVcZ8UtUbSvh9qb xnE06C3j/wB5zgfzrsq8q+JWo2mr+IfDWhrcRtbfbhNeODlUVezHoDmk1eyGnbU7rwjpY0Xwjpen qu3ybdAw/wBojJ/Umsuy3WPxSv7aM4gvtOW6Zf8AbRwhP5OK62NleNWQgqRkEdxXJxyed8WXVeVt 9HZXPoXlQj/0E0Sb5kxRXunXMdoyab5o9DSyfcNQUwJvNHoaVXDHAzUFPi+/+FAE1FFFABRRRQAU UUUAFcR8QQTdeGc/6v8AtWPd+uK7eud8aaRLq/h51thm7t5EuYB6uhyB+PSl2Ydy14jFsmjyXV7I VtrT/SHXjD7ecH2rnvhjC0fh97u5cC91OV754ieURj8vH0xW88Vl4v8ACzQzhjbXkOyRQcMp7j2I NT6PosOjxbUlknkKqhllxu2qMAcAAAfSmtGxbpGhMsTQuswUxFTvD9Md81X0yPT4tPiTS1t1swP3 Yt8eXj2xxU1zbxXdtJbzoHilUo6nuDVbR9HsdC0yLTtOhENrECEQEnH4mgZdZgiljwAMmvNfhgp1 XXvFXiV+RdXpt4Sf7kfHH6V3+pWT6haNbrdz2wbIZoduSPTJBrN8LeFbbwnYGxsbq5kttxYJMVOG J5OcZoW9we1i34i2Hw3qXmfc+zPn/vk1D4P/AORK0HPX+zrf/wBFrVLxtLLNojaRaAteakfs8YH8 Kn7zH2AzW/Y2sdjYW9nF/q4IliX6KMD+VSlq2NvRIsUUUVQgooooAKKKKACiiigAooooAKKKKACi iigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKK KACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigDnZ9Nn0/xP/a9nEZIrtVh vIl68fdkH06GugKKWDFRuHQ4paKAFooooAKYYoycmNPyp9FAEU0hhgd1jZyq5CL1PsKxvDukTWkl 5qV9j7ffuHkHXy0HCp+Az+JNb1JQAjDcpFR+U3tU1FAEPlN7U5EKnnFSUUAFFFFABRRRQAUUUUAF FFFAEEFpBbNK0ESxmVt77Rjc3rU9FFABRRRQAUUUUAQfZIPtf2vyl8/bs8zHIX0qeiigAooooAKK KKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooo oAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiig AooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKAC iiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKK KKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKAP/9k= --0000000000000f079a0589b815bc--