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-io1-xd3c.google.com (mail-io1-xd3c.google.com [IPv6:2607:f8b0:4864:20::d3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 08f27010 for ; Sat, 25 May 2019 14:50:28 +0000 (UTC) Received: by mail-io1-xd3c.google.com with SMTP id e129sf9906826iof.16 for ; Sat, 25 May 2019 07:50:27 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558795827; cv=pass; d=google.com; s=arc-20160816; b=pfD5PC2cn9TWqdBhLADsJL/g6jFZ1nR+WeRwBrjShxe6IAZ+GXkYyojr3RmnOYlR4k 0/NcGo0kiXW8G44emtv41ZisUbHFOx3Gd2zsV8AWNp41EaaUeQ2AtffVFHofh9mXOVug UiAz1OyCSZFpLyW2OvtzsA0vV3nsYhn3Nb3QN23PwrhB7OTk+dLW63R50SQpyq24WCCN kvP8qADm0iM0GK2kqvpEHW+8fXbrtn2pi3YPeYWUntmSDxp3K+Elj24Lc9wHYlv2JAit ZS0NI/uwxRz0vB85zNC0UgBFmBZaah+kh6Wf9CiK6H6y251GLrVD2NBEgBAamyml6eKv MjoA== 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=xOAkvYLBvJU58jhJnK9v+TKeuouI+2CplCIACIFTXak=; b=GV9lhLr0lVbRvlyaXYffip3xHzBoqz0q/C3enFV+NKD6rdJeOywV9JTWPPLSqFtyAV tVmvrDJ0Z7A5i4cut6knw9e1fBXk8DCS67kQdMz5ObeMVswEOkwGIeNV2VsY+dmiQyO4 NvO75OkAW35ulcPWqli1TvD7htB/xgHnYxP/iMYhEVtOxRnyBwkXE9Rn+OqKwOqluFDz DInFOZ3OXa1GLFp4R89KmIC/39gfTYkhi1x7Kd3SqyETG+UQwHkh0IPSGwe2uptxBVK1 1X9pViokjytCYwCXoDx9cVTb1zP9DzGYx+Y/X3dhyfrJHsX/ZzmC+zoH4V+Vt+t1gikB 0MSA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=b64VdgmO; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::335 as permitted sender) smtp.mailfrom=nsnyder@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=xOAkvYLBvJU58jhJnK9v+TKeuouI+2CplCIACIFTXak=; b=NOZq2Tt9on9ri1ZCtxS4BmIFjdVyrKpivQRpnTzyKmt6FIY0PbtjabdxzC4THJ5Mvv aEqtMFTk7KZVF9Rwj9BWGeeS8qZoOvR7sVLukfR1m6vki3BExxg/Ojw0GaufsY87p8CP OlhgtkaXYlr8INIrcF69YwtT37EaA5RXcN+ULw/QcZCSYmVxdYSp99qzslvW/DQfQU9H IBmqSn1+ERrS+T2QspH1c+OsU3ogSPLPze3h09H/Y2Tj1aq2Yv7i2jHO135yKee2e8vA 09iBNN8rPN8cqYuNfkn6pZOi7GytFPJ4DEpXJNyKlzrgnVfpWiB0ulZ5R4UMF9wq+3ve UQhw== 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=xOAkvYLBvJU58jhJnK9v+TKeuouI+2CplCIACIFTXak=; b=sT3YoWXUr1slDrSfw6lY0mJ+pQXxj+hHfSJ1d/WNBHoO8MGchj/zgUR/o2z4+M4KML ApFiI0GvDAKrmPKC9C6XJ6jl+yiv1f7tMdX2zkrZZZYRAQdOB5Onh398MeWg5V2jVXww 2BbKfiaEJwV5oJ6YiqEogREVac4xaAW5Fmtw781I7T4VN+/nc2vTYv6oXWKTOCtGjJ0E JdRKAANHvIpXW0IkOEAS3YEt0ZBpMGSODLaokBamNcLvcT9XiHtmerk8be3znQWafZ46 MLzUdvIeDxw+Fi2pHE8wxaOBkGvPexj6Y8M+mpognW9+zl22gplFHNLWL01bYTFAo+Er uQaA== 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=xOAkvYLBvJU58jhJnK9v+TKeuouI+2CplCIACIFTXak=; b=jruurYC08k0bWD6DeS+nyQRHGO+frhFwwaLGGQgBgNr3zYbDl6gFCx49Fn0L9GIJQP yuUknzMZ7/wuWDhMkiiVM3Et4e6lYvUBgeV6D2KjC+NZUmQgsjkLfOpgh2tLl5c6eGcB 1Xe1sqkxu3uefIL41zjjcHLyreTBYMH4/RE3wxa4CMnNew3l10vn1YHJ/qvZ77DWIkih l+QfmhXLYv++8vd3BHMjJJDxiJBV0JiU8zzPIzS4l9/0Z1KieONt4sKIRVa8/F9VvUWK 32d1jy1JXOaqBUNNyVdsYo1tx8Lvesa58o1YYAEgQIw793i1odeaPY0xzawUqgTpp6mm CFKg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWu+QAx7lf5qjnndWz5UM0Gn2T+kJN7k4WNWnj7AkQlQE8ra/Vp SfGK56EhEkWS3KAoO8kvrZ0= X-Google-Smtp-Source: APXvYqzgKH+XdR9SvxsvL3XQX83VXmNnU5/8SfogvEv/xGabD3lJNrPXDlKJXj0UTsS4OyIDeG61Kw== X-Received: by 2002:a5d:8e0e:: with SMTP id e14mr2357323iod.118.1558795826849; Sat, 25 May 2019 07:50:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:fb10:: with SMTP id h16ls2090608iog.12.gmail; Sat, 25 May 2019 07:50:26 -0700 (PDT) X-Received: by 2002:a5e:8513:: with SMTP id i19mr2772186ioj.119.1558795826408; Sat, 25 May 2019 07:50:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558795826; cv=none; d=google.com; s=arc-20160816; b=KS66loSuVDadRqZUdckJ3URZyodI2v+BeGaf69G+IFoB7LS87+CTfb44iAwgsMgwQO 35AczV12/C+2Fr6OoHxOpVcEel5qWMg61yvCVXd/Zrp+XyXgpN9JHYJ4m2jHuvWB7EJQ ll4HrstWZWd5aV3sdAFxGSgMdn3kHPIGIsxjhxe1RNZomOYhvTbuTuqRJj+9frjB/Roo j6e7q7doqXJWfysLOv+hV3qeXqEvdaulu5PSqbyPz1DtUotWHPjM+D9l46l53MMP9Jup zyc8DoFTMU16nfFdF40u6yvDfwzkY+UXrv42V/F7lQDbeQZdrj2h4g88MBVicd0M1I4E GFIg== 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=FxAgfeCiwi+vK8MSQ4GGNPB+h+dyQuC0CdXwmOvWL2k=; b=corODk+DOiHWlmlQ0LARuiVUf06PmGfVK4rfuJpLWjkoljXYVcO+9mm+q7e+4fPv8c VM8lymSQniLQCe5UORNekA+DDqFHit6DfdrnwwwUKHlzD+YXb/+gySUMahcWd/ESazwT cq/qDuCVurfjsnrXjQeU57rO2P9l6pWGWClNPbhq+AVCKPXkJ4j/2nEJjrNCOZDZAiVd LXOj96NBK2YAEsv6204KYpMPEWaSubWq6gbC3mBzpZOcP6V3/VwWEljArW1/55FQA9z3 psleZv6XxK7qEbGmlibhwXGPdT4ZenFdyo4FBtUP6KwQh5CkAnOS3MtwkxDBTkBUYLbS mXrw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=b64VdgmO; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::335 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x335.google.com (mail-ot1-x335.google.com. [2607:f8b0:4864:20::335]) by gmr-mx.google.com with ESMTPS id y3si298788ioy.2.2019.05.25.07.50.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 25 May 2019 07:50:26 -0700 (PDT) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::335 as permitted sender) client-ip=2607:f8b0:4864:20::335; Received: by mail-ot1-x335.google.com with SMTP id l17so11295409otq.1 for ; Sat, 25 May 2019 07:50:26 -0700 (PDT) X-Received: by 2002:a9d:70d2:: with SMTP id w18mr1582196otj.289.1558795825815; Sat, 25 May 2019 07:50:25 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> From: Noah Snyder Date: Sat, 25 May 2019 10:50:14 -0400 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Juan Ospina Cc: Homotopy Type Theory Content-Type: multipart/related; boundary="0000000000007a08680589b76f5a" X-Original-Sender: nsnyder@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=b64VdgmO; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::335 as permitted sender) smtp.mailfrom=nsnyder@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: , --0000000000007a08680589b76f5a Content-Type: multipart/alternative; boundary="0000000000007a08670589b76f59" --0000000000007a08670589b76f59 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable HoTT is NOT a specific proof assistant the way that Lean is. Instead it=E2= =80=99s a different flavor of type theory which is well attuned to things that have a homotopical flavor. It can be implemented in various proof assistants (Coq, Agda, Lean 2) but none of them are really fully designed for HoTT. But the kind of practical question you=E2=80=99re asking depends on the implementation. I don=E2=80=99t think any of the implementations are pract= ical in the way that you want. For example, I=E2=80=99m not aware of any kind of = =E2=80=9Ctactics=E2=80=9D for HoTT. The bookkeeping involved in saying that the two proofs of Eckman-Hilton for 3-loops agree (which I could explain in one hand gesture in person and where I understand all the relevant issues in HoTT) is very very intimidating practically. I=E2=80=99d also imagine that a =E2=80=9Cpr= actical=E2=80=9D implementation would likely have some kind of =E2=80=9Ctwo-level=E2=80=9D t= ype theory where you can use types that behave classically when that=E2=80=99s better and Ho= TT types when that=E2=80=99s better. HoTT is mostly better for math that=E2=80=99s explicitly homotopical. But = there are situations in more ordinary math where you can see why it would be useful. 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 obje= ct. In HoTT that happens automatically. For example, say you have a theorem about bimodules over semisimple rings 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 something you=E2=80=99d be able to d= eal with easily in Lean? If not, that=E2=80=99s somewhere that down the line HoTT might ma= ke things more practical. But mostly I just want to say you=E2=80=99re making a category error in you= r 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 t= he > 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 formalizati= on 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 genera= lly >> about a project of formalising many of the statements of modern pure >> mathematics in an arbitrary system, such as HoTT. I know enough about th= e >> formalisation process to know that whatever system one chooses, there wi= ll >> be pain points, because some mathematical ideas fit more readily into so= me >> 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 bec= ome >> 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 >> seems that simple type theory struggles to handle things like tensor >> products of sheaves of modules on a scheme, because sheaves are dependen= t >> 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 blessin= g >> and a curse. However I would like to know more details. I am speaking at >> 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 th= is >> discussion, "modern pure mathematics" means the statements of the theore= ms >> 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 t= o >> 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, send >> 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 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/18681ec4-dc8d-42eb-b= 42b-b9a9f639d89e%40googlegroups.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/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmMw%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout. --0000000000007a08670589b76f59 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
HoTT is NOT a specific proof assistant the way that = Lean is.=C2=A0 Instead it=E2=80=99s a different flavor of type theory which= is well attuned to things that have a homotopical flavor.=C2=A0 It can be = implemented in various proof assistants (Coq, Agda, Lean 2) but none of the= m are really fully designed for HoTT.=C2=A0 But the kind of practical quest= ion you=E2=80=99re asking depends on the implementation.=C2=A0 I don=E2=80= =99t think any of the implementations are practical in the way that you wan= t.=C2=A0 For example, I=E2=80=99m not aware of any kind of =E2=80=9Ctactics= =E2=80=9D for HoTT.=C2=A0 The bookkeeping involved in saying that the two p= roofs of Eckman-Hilton for 3-loops agree (which I could explain in one hand= gesture in person and where I understand all the relevant issues in HoTT) = is very very intimidating practically.=C2=A0 I=E2=80=99d also imagine that = a =E2=80=9Cpractical=E2=80=9D implementation would likely have some kind of= =E2=80=9Ctwo-level=E2=80=9D type theory where you can use types that behav= e classically when that=E2=80=99s better and HoTT types when that=E2=80=99s= better.

HoTT is m= ostly better for math that=E2=80=99s explicitly homotopical.=C2=A0 But ther= e are situations in more ordinary math where you can see why it would be us= eful.=C2=A0 For example, if G and H are isomorphic groups and you want to t= ranslate a theorem or construction across the isomorphism.=C2=A0 In ordinar= y 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 obj= ect.=C2=A0 In HoTT that happens automatically.=C2=A0 For example, say you h= ave a theorem about bimodules over semisimple rings whose proof starts =E2= =80=9Cwlog, by Artin-Wedderburn, we can assume both algebras are multimatri= x algebras over division rings.=E2=80=9D =C2=A0Is that step something you= =E2=80=99d be able to deal with easily in Lean?=C2=A0 If not, that=E2=80=99= s somewhere that down the line HoTT might make things more practical. =C2= =A0

But mostly I just wa= nt to say you=E2=80=99re making a category error in your question.=C2=A0 Ho= TT 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:
On page 117 of= https:/= /arxiv.org/pdf/1808.10690.pdf appears the "additivity axiom".= =C2=A0 Please let me know if the following formulation of the such axiom is= correct:

3D"additivity.jpg"




On Saturday, May 25, 20= 19 at 5:22:41 AM UTC-5, awodey wrote:
https://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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNU= C8y49JHMoR9oTQOmMw%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000007a08670589b76f59-- --0000000000007a08680589b76f5a 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= --0000000000007a08680589b76f5a--