From 0cd65c6cd9dd2cbbd5d01c3604142c026b7b3a8c Mon Sep 17 00:00:00 2001 From: kl-i Date: Wed, 21 Jul 2021 17:28:13 +0100 Subject: [PATCH] Cleaned up Trinitarianism.Quest0.agda --- Trinitarianism/Quest0.agda | 307 +----------------- Trinitarianism/Quest0.md | 2 +- Trinitarianism/Quest0Preamble.agda | 1 - .../agda/Trinitarianism/Quest0Preamble.agdai | Bin 0 -> 11330 bytes 4 files changed, 4 insertions(+), 306 deletions(-) create mode 100644 _build/2.6.3/agda/Trinitarianism/Quest0Preamble.agdai diff --git a/Trinitarianism/Quest0.agda b/Trinitarianism/Quest0.agda index 39c894e..dcb28cd 100644 --- a/Trinitarianism/Quest0.agda +++ b/Trinitarianism/Quest0.agda @@ -1,324 +1,23 @@ module Trinitarianism.Quest0 where open import Trinitarianism.Quest0Preamble -private - postulate - u : Level +postulate + u : Level - -{- -There are three ways of looking at `A : Type u`. - - proof theoretically, '`A` is a proposition' - - type theoretically, '`A` is a construction' - - categorically, '`A` is an object in category `Type u`' - -We will explain what u : Level and Type u is at the end. - -A first example of a type construction is the function type. -Given types `A` and `B`, we have another type `A → B` which can be seen as - - the proposition '`A` implies `B`' - - the construction 'ways to convert `A` recipes to `B` recipes' - - internal hom of the category `Type u` - -To give examples of this, let's make some types first! --} - --- Here is how we define 'true' data ⊤ : Type u where trivial : ⊤ -{- - -It reads '`⊤` is an inductive type with a constructor `trivial`', -with three interpretations - - `⊤` is a proposition and there is a proof of it, called `trivial`. - - `⊤` is a construction with a recipe called `trivial` - - `⊤` is a terminal object: every object has a morphism into `⊤` given by `· ↦ trivial` - -The above tells you how we _make_ a term of type `⊤`, -let's see an example of _using_ a term of type `⊤`: --} - TrueToTrue : ⊤ → ⊤ TrueToTrue = {!!} -{- - - press `C-c C-l` (this means `Ctrl-c Ctrl-l`) to load the document, - and now you can fill the holes - - navigate to the hole `{ }` using `C-c C-f` (forward) or `C-c C-b` (backward) - - press `C-c C-r` and agda will try to help you (r for refine) - - you should see `λ x → { }` - - navigate to the new hole - - `C-c C-,` to check the goal (`C-c C-comma`) - - the Goal area should look like - - ``` - Goal: ⊤ - ————————————————————————— - x : ⊤ - ``` - - - you have a proof/recipe/generalized element `x : ⊤` - and you need to give a p/r/g.e. of `⊤` - - you can give it a p/r/g.e. of `⊤` and press `C-c C-SPC` to fill the hole - -There is more than one proof (see solutions) - are they the same? -Here is an important one: --} TrueToTrue' : ⊤ → ⊤ TrueToTrue' x = {!!} -{- - - - Naviagate to the hole and check the goal. - - Note `x` is already taken out for you. - - You can try type `x` in the hole and `C-c C-c` - - `c` stands for 'cases on `x`' and the only case is `trivial`. - -Built into the definition of `⊤` is agda's way of making a map out of ⊤ -into another type A, which we have just used. -It says to map out of ⊤ it suffices to do the case when `x` is `trivial`, or - - the only proof of `⊤` is `trivial` - - the only recipe for `⊤` is `trivial` - - the only one generalized element `trivial` in `⊤` --} - - - --- Here is how we define 'false' data ⊥ : Type u where -{- - -It reads '`⊥` is an inductive type with no constructors', -with three interepretations - - `⊥` is a proposition with no proofs - - `⊥` is a construction with no recipes - - There are no generalized elements of `⊥` (it is a strict initial object) - -Let's try mapping out of `⊥`. --} - explosion : ⊥ → ⊤ explosion x = {!!} -{- - - - Navigate to the hole and do cases on `x`. - -Agda knows that there are no cases so there is nothing to do! -This has three interpretations: - - false implies anything (principle of explosion) - - ? - - ⊥ is initial in the category `Type u` - --} - -{- -We can also encode "natural numbers" as a type. --} -data ℕ : Type where +data ℕ : Type u where zero : ℕ suc : ℕ → ℕ -{- -As a construction, this reads ' - - ℕ is a type of construction - - `zero` is a recipe for ℕ - - `suc` takes an existing recipe for ℕ and gives - another recipe for ℕ. - ' - -We can see `ℕ` as a categorical notion: -ℕ is a natural numbers object in the category `Type u`, -with `zero : ⊤ → ℕ` and `suc : ℕ → ℕ` such that -given any `⊤ → A → A` there exist a unique morphism `ℕ → A` -such that the diagram commutes: - - -This has no interpretation as a proposition since -there are too many terms, -since mathematicians classically didn't distinguish -between proofs of the same thing. -(ZFC doesn't even mention logic internally, -unlike Type Theory!) - - - - --} - -postulate - A : Type u - -NNO : A → (A → A) → (ℕ → A) -NNO a s zero = a -NNO a s (suc n) = s (NNO a s n) - - - - - - - - - - - - - - - -{- -Let's assume we have the following the naturals ℕ -and try to define the 'predicate on ℕ' given by 'x is 0' --} -isZero : ℕ → Type u -isZero zero = {!!} -isZero (suc n) = {!!} - -{- -Here's how: - * when x is zero, we give the proposition ⊤ - (try typing it in by writing \top then pressing C-c C-SPC) - * when x is suc n (i.e. 'n + 1', suc for successor) we give ⊥ (\bot) -This is technically using induction - see AsTypes. - -In general a 'predicate on ℕ' is just a 'function' P : ℕ → Type u --} - -{- -You can check if zero is indeed zero by clicking C-c C-n, -which brings up a thing on the bottom saying 'Expression', -and you can type the following -isZero zero -isZero (suc zero) -isZero (suc (suc zero)) -... --} - -{- -We can prove that 'there exists a natural number that isZero' -in set theory we might write - ∃ x ∈ ℕ, x = 0 -which in agda noation is - Σ ℕ isZero - -In general if we have predicate P : ℕ → Type u we would write - Σ ℕ P -for - ∃ x ∈ ℕ, P x - -To formulate the result Σ ℕ isZero we need to define -a proof of it --} -ExistsZero : Σ ℕ isZero -ExistsZero = {!!} - -{- -To fill the hole, we need to give a natural and a proof that it is zero. -Agda will give the syntax you need: - * navigate to the correct hole then refine using C-c C-r - * there are now two holes - but which is which? - * navigate to the first holes and type C-c C-, - - for the first hole it will ask you to give it a natural 'Goal: ℕ' - - for the second hole it will ask you for a proof that - whatever you put in the first hole is zero 'Goal: isZero ?0' for example - * try to fill both holes, using C-c C-SPC as before - * for the second hole you can try also C-c C-r, - Agda knows there is an obvious proof! --} - -{- -Let's show 'if all natural numbers are zero then we have a contradiction', -where 'a contradiction' is a proof of ⊥. -In maths we would write - (∀ x ∈ ℕ, x = 0) → ⊥ -and the agda notation for this is - ((x : ℕ) → isZero x) → ⊥ - -In general if we have a predicate P : ℕ → Prop then we write - (x : ℕ) → P x -to mean - ∀ x ∈ ℕ, P x --} - -AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥ -AllZero→⊥ = {!!} - -{- -Here is how we prove it in maths - * assume hypothesis h, a proof of (x : ℕ) → isZero x - * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1 - * notice isZero 1 IS ⊥ - -Here is how you can prove it here - * navigate to the hole and check the goal - * to assume the hypothesis (x : ℕ) → isZero x, - type an h in front like so - AllZero→⊥ h = { } - * now do - * C-c C-l to load the file - * navigate to the new hole and check the new goal - * type h in the hole, type C-c C-r - * this should give h { } - * navigate to the new hole and check the Goal - * Explanation - * (h x) is a proof of isZero x for each x - * it's now asking for a natural x such that isZero x is ⊥ - * Try filling the hole with 0 and 1 and see what Agda says --} - -{- -Let's try to show the mathematical statement -'any natural n is 0 or not' -but we need a definition of 'or' --} -data OR (P Q : Type u) : Type u where - left : P → OR P Q - right : Q → OR P Q -{- -This reads - * Given propositions P and Q we have another proposition P or Q - * There are two ways of proving P or Q - * given a proof of P, left sends this to a proof of P or Q - * given a proof of Q, right sends this to a proof of P or Q - -Agda supports nice notation using underscores. --} - -data _∨_ (P Q : Type u) : Type u where - left : P → P ∨ Q - right : Q → P ∨ Q - -{- -[Important note] -Agda is sensitive to spaces so these are bad - -data _ ∨ _ (P Q : Prop) : Prop where - left : P → P ∨ Q - right : Q → P ∨ Q - -data _∨_ (P Q : Prop) : Prop where - left : P → P∨Q - right : Q → P∨Q - -it is also sensitive to indentation so these are also bad - -data _∨_ (P Q : Prop) : Prop where -left : P → P ∨ Q -right : Q → P ∨ Q - --} - -{- -Now we can prove it! -This technically uses induction - see AsTypes. -Fill the missing part of the theorem statement. -You need to first uncomment this by getting rid of the -- in front (C-x C-;) --} --- DecidableIsZero : (n : ℕ) → {!!} --- DecidableIsZero zero = {!!} --- DecidableIsZero (suc n) = {!!} - --- TODO terms and types --- TODO universe levels diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md index 74cdba6..7765f32 100644 --- a/Trinitarianism/Quest0.md +++ b/Trinitarianism/Quest0.md @@ -3,7 +3,7 @@ There are three ways of looking at `A : Type u`. - type theoretically, '`A` is a construction' - categorically, '`A` is an object in category `Type u`' -We will explain what u : Level and Type u is at the end. +We will explain what u : Level and Type u is at the end of Quest1. A first example of a type construction is the function type. Given types `A` and `B`, we have another type `A → B` which can be seen as diff --git a/Trinitarianism/Quest0Preamble.agda b/Trinitarianism/Quest0Preamble.agda index d5564dd..95c03ec 100644 --- a/Trinitarianism/Quest0Preamble.agda +++ b/Trinitarianism/Quest0Preamble.agda @@ -1,4 +1,3 @@ - module Trinitarianism.Quest0Preamble where open import Cubical.Core.Everything hiding (_∨_) public diff --git a/_build/2.6.3/agda/Trinitarianism/Quest0Preamble.agdai b/_build/2.6.3/agda/Trinitarianism/Quest0Preamble.agdai new file mode 100644 index 0000000000000000000000000000000000000000..6a29d8d860171c21039abaed61d1c1d220863168 GIT binary patch literal 11330 zcmYj%2{=_-*#Fx5jHctLlbLfuIo%Q^^Rx@mRfgP3WhzlA!bL)Cr4p4R-BQ9yZYibH z&2%LlO1LF5L}WfUnaY?U@n2i_`@a9)k7w__to5$<{k^|;SROrFj{m0T?OM2nIx-iK z_MQabB`MLZ$4;OVuYkOiTqcIE4EkX)(%kpshk5PWw?i%YEltJmAHTYBD7|vOwe$H* z-oq=wnOc56A&=@GelA`5XK<(7pZ$)-S>LCxF>KCX^0*RwEq7tCqHCG3>koi4xMV3N zh8Xji!5EOLL(X^tx+nOIZ_*)?1!Uq|jD!D)Q@L9Knu3yb#17$q(mD7rDATwDkOzRA z>_Vk`uHY|Ec@>I-Q1S+H!yz2(L=;aQmITO<t z1{RSrjx9(Xa_-hX#X3YYa~~TM$VQ;z5y&YsfdL2LCH*qePX`Y#80{l-ha~9l_fZ|` ze1U466KG-AAyZZ_>~T-6FOpnkK>sF;!KwHp?#TcYeEGK*YkUIbF6dCnOiY02;^iCo z0d)Rt5WwY=zFa)3hj+a-lyodw&1oT>Bb_yrS9&aC;~Be-gEQ!#){(eJY21$_xJ!{H z$50X~G=-8Qy0}8-@yaB_B{p8M>-gQAk5W@q(NM-v=%?#LEjw#4;Zt0ErYp9x=oUR42P%DRK_uE38y7qlXNx=l@;K330zumExi05ehC#eASwZr zt6ox^FtxW-Rysm2=(&zBPe1F|a`tzfa(U((F9|-W^whsC63m+y`+#^Yg}isvRLHD- zwZ>;OlJE#*Ro{LIejPX?hZu{4KE$}|h|8suNZIcr`?2m7xaVqjarvGzhU~sxZvqZa zZEQsRD8kx_ia$bwS-@TDGZrDa(+jPO`9^;5DhM0dQ^IfzGvl}<8bD}PxSwwBLg7Y| zBfptSXbWGDZpJE|N7s}9Z5mk);R|R4tUee}0%dyz6ewidgE9ag>JQ4qu>i3SDz`+1 z`JmDSSe7i4>)l_nRQ&={b|y^D6E`YRLIA6SL|^+V0y#5pyL zP<(WtRSSAPf+fsI@eC@ij?bOqLh3DRA!{&E>zqDkQ1iW zJmYG;lnT1-2%tU%8u4`yt}Ep;7ep?riXn|C zd4->??S4Hi%fa*UE)ysjdH!Pi8d|WBEnuxi%BDt6V%-bKspL@-HWCOVN8Mb{z8Xo``%y$O|tQfHf51NRjV(UW6DpmeIYi z7oDT*`v_{dgz1a7Au1`Q^gcd-4{{$&gpEslQOCyZn80=$da4cRWSyNhi*nfJ^je1+ zJJ7g+kNA@@lB=B-O)@|!UuEUJWq|7&fsI7?uHXxFJ?TZ1Y!zfLqC&xj$@DvcP>~mG zPgTli;mF;T$|YEK+C38_eh+m1JvU(KtCt_Y$9niztrzml`_4}hYSG13mE=Zoz{;m_ z8h`QC;svfP{X6)CG zp;2b}7X0kp(1Laaovd#!P}yt}5xGbCKH$usc;+VnwYvyZvajtk3Z=xhW*E~Q8>w)* zilqGZm5!DBCFyz&?Q)JOlvqXQO5_w}APgf7kiiDw#l|0qRDf29nkV+~_LpiA65|Ig1K0ozx2*$F{ZNCfR!{s?H4ra##3n3DrSPH1#SECym2?qnATnSSdP>9q49TMZ6?QDv%QuidGDZ??32dvbEW6LKj}#xi4g&6u%5U%6-sjZkq+J2&e>dIUEFm13T#pGzA+pd< zn~o+@KVxZ$!|R~BD<*%zoE}lhyPO^&lJ|BwN;IOAdwdmM;f~sO-D%tbQ%uM18Nxhz zdo3VKG%6ud*%C+{FxW1KD0b}`*oGtix7`!B4AcPbz2+MDeFq4iFwSd$+I<$01qR`E&xugLGgrjw^;CHdL4D4eqz^0J{N?qXx# zVy$z&h8lMnqzJ#@jv2Q~p-BmNm+XKYzC2{b+sc{7YY_jsYzL=|yQL^Sl)sh|>^bfD z<`z(qH%EV$2bfwGy#DdbE$V*P_CERE7g+24(leA3&OAP1-jaAYTG(~p!{F@AOidTKEH z2;`JaqaM6Nh}5U&;3h5ad8rs#x)>_DSoV?Z43hXUDgnO)bT|>yTKkvnM2sDGc`ge@ zVrN%OuEw06Q_0Ov&!NLp@13U+viIs(`=OXqA-bvE>IcKoMS?q^ z4|^TQXh44IsEacip9`o`bup~>o~t;G8QB)3_*n@~(WTkdp0+=diqneIW|d%l+f?Hm zO@oI1AUQ9p=743l-7^7a%%Gu4grU)(?0B{UMhoJEZX^YBlmrr2(M>#*B?e_}5b|c( zlO6-lvtVz=X*5*;)D(5gtxl=H@c>NO(bZ(WzyOy0Dh-a@+}F$yj}!04Eg0OtB$*G? z8*s*i+hbYcVfI*dHM0D5wK$eEjFhSE7L&g`EWjy$krwOk0mZtQQj7Qd<*+L8zr-C6 z=y6;$Oh{)BX!>rwSe-`j;V<>wB>L547~4ThcHTyedCmgGr8uv>>I<$G0Zv&~?Gf^Z ze!Wx0`atv)%b)U|0qcuM8Tx@%hd&^}I%)fj0&C;}s*X_kgOc+B3&7efO~0=8ofN+n zH5SJ|Dlkh<-9Uo*wcX$W8q8Do)Q;y9>^W%0wDLOHRlWjCpp`R2d?5f_x|2fW)s- zN0w_Q*&yO}z}lVy`D`S`^SZmTbM};-d!#A9$_us-e<{?(+$d+=K~%DrrIi1QRrOXW z;A)99a>4-#Pg~Ul${L>LV!Mm!lZ+iryu^=yzG3h_aKA^L3H#XsQVamp)uoF`FjjjJ6)$>(?mq_ZL^ z(M5RgC-xlL)PWKrm%Xlv0^A@mj%ZTkhnGj;YF~*KhiI8IKx47Nr|2cAEbe`xj6lV+>AWG zDuSrrYf0n)WsYbm%yHSh#DKZjXG~V0{vI{vY3{Ru6rN$tY~WWN1Z8S7Ydme&Y9<^= zawVD%$8pi`Fh5oGJzk{iE_9Q*JJY^)hrOQTyh2)?ijBgc#;cR>S-IbIajkeIh82ou2xZmOXtLs8x^2Sk6=}kA_KhK z4OmA>5CSDQI1I|Db6Pk<(mZ}Qi%&Z3;3eyf^V+J|z}lZi9;{{~mSYh?tN;FEPK@Z` ztVOj1L>@X@(hyuNniBi**Lf=U4H7>`9DhX_I7nyEXXN~8!Jd<)(`w>%F-_ll6JY6@ zx15*Yju8<~lD{0CY*M9?S5DLfdkJ_<+Vesq9|hKfIM3t|34>?%)+MkY)U5<%LGZwH zQw-|b3YF_PEw&XHcRfoHZpRKa08D`UM_Ct`^XshOKMqep(>DK$DaAXWlb#<}|Qwqd|-FLU3SCru$Lh30Vryd`N?| z_KU`7E7N1tbwIFZ55*8|LpD9t9R}Dt2AMo~_&6eY`1?Db!%y;zAT!8v?>0j~4|%P* z{g#-4#ujM%k@x{R{6pse%y6Mx4ql0FGP!UAVKIm#H5`D^#uSHQ^Kpg<9f}RX>%MGG zrLl&;;GRjL(n4P7u2z{m^+QuH7YlA{5+Qu5d@-YkvN(Ac^KK*7Cd!27-vMe!VYWUl zQmKnknLj@T+l-d(=V9!#P^66s!!fTHmb76q6zS2rF3;=GROO<-Ok`jR^;^1lP-!KB zTPl_j9KJxtF)x`2wg?><(nNc)R=5OK9N`(4Q)$R8vn!$E{6o?ta`QV?hJ3yK9kbYP z%vSZEMdzC>g*{j28lHsOmIMzM89(nR&m#}VuU9E=&#YWN}z=GW{sA1=mAm`2mJ7Z!J9M7$UsEwRGCt zk4x9Qo@{HKxYD})?RFhQ1!N;jvTfULPW1*F5>uf4MEl93>nC(ij{7uNlSOOJan1$N zcYLuVJIPqTBuSfcxxd8s$XK%|P8+9liWa_F7L%BPMvqZ)y$XH-U;{v5#GvIg%0uJ? zw5K2`Z;P=sJ<9}Zqe%h zfX5khh2W@J{qK)c1u^DuT%I}lOZ_-NIwj~?a$r3Q`p@9>=@3lgnS3Eht;-9y4HxsL zX@Gh=M4{zJf=k6(j2ap(pVJ~0mvt>Uip;cq1gt({;VV38{cG!A+iI)-;4(6$xpm#U z!&Kev!JQ0kPU?sytm$vcG9aP--Z(icgN&h@tY=qYXt_fDULZDNRKFLYgl9c{ zY!$8q1q?%lW%^Zcyb^x65uk+|aL`>7{4hpcP- zN!)f8^dCfGCN^R(o$70mP+ruHiKzPTTPza)!_xymJk4XhdsZV%+voJStSO$kB;Al) zMF&|PR4d^ik~FcpNQD=Z)+xO02-XXJS4u3mhH`h*SAv*{BZOto87&)Ux&7){iM%Kh z?H$dkBxWL&@JHq2tt|lK{E+2bHs3Vs2jA8&YAMHro{7uqRCkrG!kl{F+2WEcT~kFn zD3(;uM$!IcJnp$hJ1Gu-4Rt?^p%XHIg7zmObu=p>2_#J@)MtPtC~uy{+>%k2iijb$ z84!zuBRbe7Q11cM`gOx3ImMfE>ZD-Z`R~yEeb9$t* zqDc_y(s=K3Ds*Be#MQb!8le7Uf;!F6DECM@FGe8onhO-@5rPYD5DjX7Dvr%Y<8gO+ z^Gbr#6CPQQl1uGp*~(UI=9X)h=jEWLv$AUa#(-SEfT;BkW&Q*~5E1q&fkF zHVPG<+J8Mj7oaEDoXhGn`!V4@jPsQSRUZ2jr-yMkm$fw`nUEb*mFi5O&@$s`ikcuv zkt=3?!8p-MoXq8&5`xo_l$rHo-lCj9=1ELrPJgBia$9snU^UGG=*%8W!((%)0SEpa zOQVwp6c9Yp14BRJNB>ws~uKa zT$~G@K$61rW)$#KkvAhHuAY}hF;1s=oCulG$As$$W@jK)uJ$E#ChYT|3tW-)ysLpK zOE{$d{jTTIa9h`xyRv$0jAzZWn zn(cGTS+w7xy6PJ5k$SY;%+qR{sud?T&+o%t4vHz^SQL!k9U?iHSGLcob9f%)xGe9n z1SDy0)0i8sI_h8EcmB9cr$g}{0a}MQMN+%ZzxvU#^ zP3f7DZS_rA(n+OfYL^`6rQ1asj&2^)d+E@vk|hzlS1jT@TRkeK2S<)Uiu{qS|6p)C!>HufD+L z3u}9y;MxFcDit?vGrAQtn8nOm`B9~=5<61OcnHAlrZ zhJo($E-NJ=&=yEs?DynO$T)^AR;ol$Vh$$dld*#cqKOb+J27hcwE(eP(g9AS!nLj_ z+&0Q&Mg?M}$?16^Iu1)s=cXv789&kSrSD}1wAfSY^D!T!egiQN$&$VHc!DcO3utJ$6{2w zlU>w4lHiaIr>8>X0f{1Gp6C{fKvC+r?X>gQBOpFO_b69g+%N}PiOtLNvBZ&WL(2&x zpEKfOA67WO#P}D38KnI)kfcm9EeGk0;?7pREot};%+s+0Zy8h99mu?18uIvZB4D`C5d%% z-}7XcC+iB_2U1bm&CXMhmOtAXZ^Cwb5E=-~xyXTRI~FOL32!z)BwB@L+|1`CM&b zDWR3#8kx;-KW(_oqiO+#l2)vd`9@5VjC;ATGMWOnD^^SjJ_cp)LXz@Q=e|No+u5%d zon-+F7&g`ncgtF~W+@d4T0pJp)vG&+hQj~VPi7G{X;id8C59-AUU-h%8gHAIh5K(n zh=CH=amAzXb7IZV@=_GUsG(~2{z)8jxJD>t%?u&M@rckS(tRh8-Mk&=UHUciog=xr} z)r^Xd{irtkIjI>@n~7pgAy5)gQ_xu)3$%bW#rY%Kk@x)E9C;C1M^jjT5;Kcb9eIh# z$I8}^hC^$VK$0mxOb04z`rpV`U^T|;0dQpQ=$fUEXc&Lm9@D5@6^@@4HDC6yiBg}b z5oIi2SToaC{oHomd(5W#`R4g;W5<#$HqMjA%tRJy3t}@*M72p44)c4*I+GWY=4wUJ zD;AVyEUG*-qm$<>L<_g+tn2$VE0$DPv*esze+{Hm6gowkR6JYt#cmYD)0|9Wdv394 zh|D9+3m~TFDUf-T879xUytYCPe#+psd+tp8V_9K_73v7>{PCsc4kZcGQS}dFk8D}m zqf2+t=t!K?8H=c{U8$-*MSrv+^8Cn_`X^OO%fD9@GE27<-#{{h2r#q} z@yp_0;I>c)EiAK0jH@aghdrj+%5OJCmhm}mzmEQ3Igl?PNx`csk^x131R2ZWs@esT zVV;e@4M1Fx)Jcpl50+Ha031!llW}tnL{bdn8;ZrzS$6?K;W*x;YOq)i8zFzw#jA=~ z$VpQQe5G=^Q6S)QPd|)IP@xNvl*L}Ijo*vNNZ&F<=&Ti-o*33aAVXVa5A`?Z^Z;v0 zT$lzSTOLuHWhvnoUdz-~PLa@xVf<7N4QQ@!{>-F;0&YON!I8fta0wsQKS1 zf~if~Pz;_m(tlk?BgZqCqpWxe=N2cO(CaN}eeTLgv6DB+MnuE+#NZ9@x#_}GReY*07Zu~=TTCaV)~_nU9unJ+Z=l&&$`&0c_P1$ zq~~90bYb1b)2n=nNLrsh3xq4*_SzrqzCOLtRKg(j7vrO72~)c~AyCf! z)U_V(Frz5)BjM`N+hNPxFE)4OPp_LZbU)YJD;1_5g&r$U4K#>aVsWOh>tUEu$ED+4 zX<>357pJ0iwm3c2OPbydo55A?@#bAm-`TLa?x)OWKi^I???S+5(k$`w`L;A} z4)}@d7RS4f{2XFwTe9nH*x)3XfXf0Daw)>40ZNX_w+$Hpu(UIaB)IMjfM<|ImbWLD z2*v{w!ap`idG`I&v(;=(B_7!j=7fZrMtK`wPeWhkhhVB#+Nqp0mzxMnbKqSTc}O*H zGV9AgjksXyz+QupT?HW@8pp*vD{B&bJ0?NIG56oba}5sV1O@rHB4hvLJp^_+sXLxF z`8C$i1se_xZfS2yZBiEWjRe1YaLvuk?-QPOx5I*p2Si*I5;ZL98~4Jry=+J?ZNhTNhIP`h;!P_+>XcD21taDcVS>q z@ggvy{!A0Z1sX1T+4JVHHLXSO$YAxhUTaE=5q#-#k!aC{Ppt$WVy6wq-XkW(1xG*W z3hN&{)YNSI>v}CPk*y*0>HhH3B$bDoakr_GVPRxW|3402V z9b%y6WS1}?@Q&(LFX0LrV?zUJ@_@eIQ_}e1wi;xYO520hK%>;An$MyM*QPfP*ZiCf z)P>%6Z_Mo1Pc3lEkIEiwoqdy;1HLD&dF5uNwCh}P?!($O#lDP|sjS&I_ddDmnsqAY z=8PJ5WfDFx4)*ED|5reAEit|xvUha@{7Tqo;D^}dB=0T^Daw5{h@V`1b#D62&nP!z zH?nq5+MD8s`92+g)CkZu5AA*0-zNpN*dq};HJ|toR%PzJ;w9`LL@RFXYv1o0y3F(I zz=8LEQmx_Jk5BqgT-=G}8}}Z&>PBgKPHbA4Gw#>E<8*=YwqJ$y#MHEo>{juBnLST- zUmBeJ<1Z!uE4`z9Et}*eg6M}I)>KZ;{*!n8`0)OgZF_}(9I5d!%5C0tr>5kH+zbC! zbAMBnbkfHo|IG`2;``bu|1T%0TB+8c4XcpmT)otPi`*@YRkrqp>^ki>?(2P9F9E@gJ2w zJ9J%cDm1^aJow3NFT+H*;(teeqEj^GX}q?rxJ{AJ;VrxH^CkPIWx*XC;_yP7$n+YP*TIi&t^(Kn0{(Da|XwKSU|9~!xK?moWPVCRc< zT{oO-{`LtkHQHl;e`b$v%B9x@UkVl_{4OkY9`|*v={xuK&C>$qQ2gZGPfbNPYMXDI z*rophrmV&i#a-hw{D%gwbJ353b=PMy-Pl*$cIDTM4qUQs-#LD}p*PV239Gs_!yhWX z?`MDX%3#Cz_#cOLzqVEgQVS|uH+~4&(RQ=N_fE}wa=^d8eh4<$v90N9@9g!a$2IrO z*7-d(@?7|*=;pEC#xo6)`0cS-%T`(2T>Pw)BOFHluY(?9n* zSNT!Fa2{po+2T<8ja|LI=CuF$THAKVe=~0P{#EajhS2Q~**6|tcwJF~LPA|X?ydWP zk$<}(r0{Wg-%(fT!7q*`sO#VF-#q9vR$c&;i2>Qg|o+r&sS}rPe^;E(6@| z|06|?pV6cDFkd`+TNtuSWmVzZ-)!#I{F7&7;{Mwfi4+5-$7SVL$tw!&(0SH)<(HcwS*P_8$kIpkxt0B4ByuK%KldlzH0iX$n{N*QCGclO{8(hgZGOG z=XG)aCp^bqZ@fS3$sUg*#rL(&!HRt8H#Z}iYt;Sg4wb1*vq|??XSf!GobYk2LFCdF z$rc^?%pK-z>;DO@!1mwp?>~9?GnOtk1-KRvQT(FeTbSO>f+^ zL0@Bu?|+G3k04(0=kzdW7Znx|zt<=7VX;$gZkO%4-!Pn~@KA3&_vqQC{}HJqT(P<# z|I<;up@AA-zxAmFDxRHteqT&z`TEzlwJ`!JE+#-4Uv*o|{o@VZZLskO_)y(HVf*2z z3alHmbHN|wOJBUGR%0#5SbQ;C{iLJvZLo|5O|fb!rb;ouE4@ zP__v6Zrv&E24nxB|84)x&3=u8A-ct1HWs=U4Yn6{1hgLw^l_EG2LGkknvSOlE82cu zQ?Z~$%(dXz;`O7S2~1*+6#l#{R8UXNfYEP1FHK7@M9yvPSiDO67D&PJX}a+I2mT*q CdnOkE literal 0 HcmV?d00001