[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Altenkirch Thorsten]

UC5TLiBBbiBhdHRlbXB0IGF0IGEgc3VtbWFyeToNCg0KV2UgYWxyZWFkeSBrbmV3IHRoYXQgcGF0
dGVybiBtYXRjaGluZyBpcyBpbmNvbXBhdGlibGUgd2l0aCB1bml2YWxlbmNlDQpiZWNhdXNlIHdl
IGNhbiBwcm92ZSBLLg0KDQpOb3csIGR1ZSB0byB0aGUgZXhhbXBsZSBieSBNYXhpbWUgKGFuZCBD
b25vcikgdGhlcmUgaXMgYW5vdGhlcg0KaW5jb21wYXRpYmlsdHkgd2hpY2ggYXJpc2VzIGZyb20g
cGF0dGVybiBtYXRjaGluZyBtYWtpbmcgdGhpbmdzIGFwcGVhcg0Kc3RydWN0dXJhbGx5IHJlY3Vy
c2l2ZSB3aGljaCBzaG91bGRuJ3QgYmUuDQoNClRoaXMgb25lIGlzIG5vdCBjb3ZlcmVkIGJ5IEsg
YW5kIGl0IGlzIGFub3RoZXIgZXhhbXBsZSB3aGVyZSBwYXR0ZXJuDQptYXRjaGluZyBpcyBub24t
Y29uc2VydmF0aXZlIG92ZXIgdGhlIHN0YW5kYXJkIGVsaW1pbmF0b3JzIChJIGd1ZXNzIHdlDQpj
b3VsZCBpbnZlbnQgYSB2ZXJzaW9uIG9mIGNvbWJpbmF0b3JzIHdoaWNoIGFsbG93IHVzIHRvIHVz
ZSBwcm9wb3NpdGlvbmFsDQplcXVhbGl0eSBvZiB0eXBlcyBkdXJpbmcgcmVjdXJzaW9uKS4NCg0K
QXMgYSBjb25zZXF1ZW5jZSBpdCBhbHNvIGFmZmVjdHMgQ29xLCB3aGljaCBhbHdheXMgcnVsZWQg
b3V0IEsgYnV0IG5vdA0KdGhpcyBvbmUuDQoNClRoaXMgaXMgY2xlYXJseSBhIGJ1ZyAoaGFzIGFu
eWJvZHkgZmlsZWQgYSBidWcgcmVwb3J0KSB3aGljaCBzaG91bGQgYmUNCmZpeGVkIGFzIGEgbWF0
dGVyIG9mIHVyZ2VuY3kuIEFueSBwcm9wb3NhbHM/DQoNClRob3JzdGVuDQoNCg0KT24gMDgvMDEv
MjAxNCAwOTo1MiwgIkFsdGVua2lyY2ggVGhvcnN0ZW4iDQo8cHN6dHhhQGV4bWFpbC5ub3R0aW5n
aGFtLmFjLnVrPiB3cm90ZToNCg0KPk9uIDA3LzAxLzIwMTQgMjM6MDMsICJDb25vciBNY0JyaWRl
IiA8Y29ub3JAc3RyaWN0bHlwb3NpdGl2ZS5vcmc+IHdyb3RlOg0KPg0KPj4NCj4+T24gNyBKYW4g
MjAxNCwgYXQgMjI6NDcsIEFsdGVua2lyY2ggVGhvcnN0ZW4NCj4+PHBzenR4YUBleG1haWwubm90
dGluZ2hhbS5hYy51az4gd3JvdGU6DQo+Pg0KPj4+IEhpIENvbm9yLA0KPj4+IA0KPj4+IEkgYW0g
c3VyZSB0aGlzIG11c3QgYmUgYSBzdHVwaWQgcXVlc3Rpb24gYnV0IHdoeSBpcyB0aGlzIG5vdCBj
b3ZlcmVkDQo+Pj4gYnkgeW91ciByZXN1bHQgdGhhdCBwYXR0ZXJuIG1hdGNoaW5nIGNhbiBiZSBy
ZWR1Y2VkIHRvIGVsaW1pbmF0b3JzICsgSz8NCj4+DQo+PlRoZSByZWN1cnNpdmUgY2FsbCBpc24n
dCBjb3ZlcmVkIGJ5IHRoZSBpbmR1Y3RpdmUgaHlwb3RoZXNpcy4gVGhlIGRpcmVjdA0KPj52ZXJz
aW9uDQo+PmdpdmVzIG5vIGFjY291bnQgb2YgdGhlIGluZHVjdGl2ZSBoeXBvdGhlc2lzICphdCBh
bGwqLCBoZW5jZSB0aGUgd2hvbGUNCj4+bWVzcy4NCj4+DQo+Pj4+Pj4gbW9vICh3cmFwIGYpID0g
bm9vIChaZXJvIC0+IFdPbmUpIG15SXNvIGYNCj4+Pj4+PiBub28gLldPbmUgUmVmbCB4ID0gbW9v
IHgNCj4+DQo+PlRoZSByZWN1cnNpdmUgY2FsbA0KPj4NCj4+ICBtb28geA0KPj4NCj4+aXMgcmVh
bGx5IGEgcmVjdXJzaXZlIGNhbGwNCj4+DQo+PiAgbW9vIChzdWJzdCBteUlzbyAuLi4gZikNCj4+
DQo+PmJ1dCB0aGUgaW5kdWN0aXZlIGh5cG90aGVzaXMgdGVsbHMgdXMganVzdCB0aGF0IHdlIGNh
biBjYWxsIG1vbyBvbg0KPj5vdXRwdXRzIG9mIGYuDQo+Pg0KPj5Cb3R0b20gbGluZTogaXQncyBu
b3Qgc3RydWN0dXJhbGx5IHJlY3Vyc2l2ZS4NCj4NCj5JIGtub3cgdGhpcyAtIHRoaXMgd2FzIHBy
ZWNpc2VseSB0aGUgY29tbWVudCBJIG1hZGUgaW4gbXkgcmVwbHkgdG8gTWF4aW1lLg0KPg0KPkhv
d2V2ZXIsIGl0IHNlZW1zIEkgYW0gYSB2aWN0aW0gb2YgbXkgb3duIHByb3BhZ2FuZGE6IEkgd2Fz
IGFsd2F5cw0KPnRoaW5raW5nIHRoYXQgQ29ub3IncyByZXN1bHQgdGVsbHMgdXMgdGhhdCB3ZSBj
YW4gcmVwbGFjZSBwYXR0ZXJuIG1hdGNoaW5nDQo+KHdpdGggZ3VhcmRlZCByZWN1cnNpb24pIGJ5
IGVsaW1pbmF0aW9uIGNvbnN0YW50cy4NCj4NCj5Ib3dldmVyLCB0aGlzIGV4YW1wbGUgc2hvd3Mg
dGhhdCB0aGlzIGlzIG5vdCB0cnVlLiBPbmNlIHdlIHBlcmZvcm0gdGhlDQo+dW5pZmljYXRpb24g
cmVxdWlyZWQgYnkgcGF0dGVybiBtYXRjaGluZyB3ZSBvYnRhaW4gYSBhIHRlcm0gd2hpY2ggImxv
b2tzIg0KPmFzIGlmIGl0IGlzIHN0cnVjdHVyYWxseSBzbWFsbGVyIGV2ZW4gdGhvdWdoIGl0IGlz
bid0Lg0KPg0KPk9uZSBvYnZpb3VzIHF1ZXN0aW9uIGlzIGhvdyB3ZSBjYW4gcmVjb2duaXplIGdv
b2QgaW5zdGFuY2VzIG9mIHBhdHRlcm4NCj5tYXRjaGluZyBmcm9tIGJhZCBvbmVzLg0KPg0KPlRo
aXMgYWxzbyBpbmNyZWFzZXMgdGhlIGFyZ3VtZW50IGluIGZhdm91ciBvZiBhIHNhZmUgdmVyc2lv
biBvZiBwYXR0ZXJuDQo+bWF0Y2hpbmcgd2hpY2ggaXMgZXZpZGVuY2UgcHJvZHVjaW5nLiBPbmUg
b2YgbXkgbmV3IHN0dWRlbnRzLCBHYWJlDQo+RGlqa3N0cmEsIGlzIHdvcmtpbmcgb24gdGhpcyAt
IG1haW5seSB0cmlnZ2VyZWQgYnkgdGhlIHdpdGhvdXQtSyBpc3N1ZS4NCj5Ib3dldmVyLCBhcyB3
ZSBzZWUgbm93IHRoZXJlIGFyZSBvdGhlciBpc3N1ZXMgd2hpY2ggd2VudCB1bm5vdGljZWQuDQo+
DQo+Q2hlZXJzLA0KPlRob3JzdGVuDQo+DQo+Pg0KPj5DaGVlcnMNCj4+DQo+PkNvbm9yDQo+Pg0K
Pj4NCj4+Pj4gDQo+Pj4+IG1vbydzIGlucHV0IGlzIGJpZ2dlciB0aGFuIHRoZSB0aGlyZCBhcmd1
bWVudCBpbiBpdHMgbm9vIGNhbGwNCj4+Pj4gbm9vJ3MgdGhpcmQgaW5wdXQgaXMgdGhlIHNhbWUg
YXMgdGhlIGFyZ3VtZW50IGluIGl0cyBtb28gY2FsbA0KPj4+PiANCj4+Pj4gU2l6ZS1jaGFuZ2Ug
dGVybWluYXRpb24sIGhvdyBhcmUgeWU/DQo+Pj4+IA0KPj4+PiBXaGVuIHlvdSBkbyB0aGUgdHJh
bnNsYXRpb24gdG8gZWxpbWluYXRvcnMsIHlvdSdyZSBvYmxpZ2VkIHRvDQo+Pj4+IHNob3cgaG93
IHJlY3Vyc2l2ZSBjYWxscyBjb3JyZXNwb25kIHRvIGludm9jYXRpb25zIG9mIHRoZQ0KPj4+PiBp
bmR1Y3RpdmUgaHlwb3RoZXNpczogaGVyZSB0aGF0J3MganVzdCBub3QgZ29pbmcgdG8gaGFwcGVu
Lg0KPj4+PiBUcmFuc3BvcnRpbmcgZiBhY3Jvc3MgbXlJc28gZG9lcyBpbmRlZWQgZ2l2ZSBhbiBl
bGVtZW50IG9mDQo+Pj4+IFdPbmUgKHlvdXIgQm94KSwgYnV0IHRoYXQgZG9lcyBub3QgbWFrZSBh
IG51bGxhcnkgaW5kdWN0aXZlDQo+Pj4+IGh5cG90aGVzaXMgYW55IGVhc2llciB0byBpbnZva2Uu
DQo+Pj4+IA0KPj4+PiBJJ2QgcXVpdGUgbGlrZSB0byBzZWUgdXMgZGVmaW5pbmcgYSB0eXBlIHRo
ZW9yeSBpbiB3aGljaCB0aGUNCj4+Pj4gb25seSBjaGVja2luZyBpcyB0eXBlIGNoZWNraW5nLCB0
aGVuIHVzaW5nIGl0IGFzIGEgdGFyZ2V0IGZvcg0KPj4+PiBlbGFib3JhdGlvbi4gRWxpbWluYXRv
cnMgYXJlIG9uZSBjYW5kaWRhdGUsIGJ1dCB0aGVyZSBhcmUNCj4+Pj4gb3RoZXJzLiBTaXplZCB0
eXBlcyBhcmUgY2VydGFpbmx5IGFub3RoZXIgc3Ryb25nIGNhbmRpZGF0ZS4NCj4+Pj4gSSdtIGFs
c28gaW50ZXJlc3RlZCB0byBzZWUgd2hldGhlciB0aGVyZSBhcmUgImxvY2FsbHkgY2xvY2tlZCIN
Cj4+Pj4gZXhwbGFuYXRpb25zIGZvciB0ZXJtaW5hdGlvbiwgYXMgdGhlcmUgc2VlbSB0byBiZSBm
b3INCj4+Pj4gcHJvZHVjdGl2aXR5Lg0KPj4+PiANCj4+Pj4gSW50ZXJlc3RpbmcgdGltZXMNCj4+
Pj4gDQo+Pj4+IENvbm9yDQo+Pj4+IA0KPj4+PiANCj4+Pj4+PiANCj4+Pj4+PiBiYWQgOiBaZXJv
DQo+Pj4+Pj4gYmFkID0gbW9vICh3cmFwIFwgKCkpDQo+Pj4+Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4g
DQo+Pj4+Pj4+IFQuDQo+Pj4+Pj4+IA0KPj4+Pj4+Pj4gSSBhbSBhbHNvIG5vdCBzdXJlIGhvdyBz
cGVjaWZpYyB0aGUgcHJvYmxlbSBpcyB0byB1bml2YWxlbmNlLiBBcw0KPj4+Pj4+Pj5Db2R5DQo+
Pj4+Pj4+PiBzYWlkLCBJIHdvdWxkIGV4cGVjdCB0byBmaW5kIHNvbWUgc2V0LXRoZW9yZXRpY2Fs
IG1vZGVscyB3aGVyZSB0aGUNCj4+Pj4+Pj4+IGVxdWFsaXR5IGhvbGRzLiBTbyBiZWluZyBhYmxl
IHRvIHByb3ZlIHRoZSBuZWdhdGlvbiBpcyBkaXN0dXJiaW5nLg0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+
PiBNYXhpbWUuDQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+IE9uIDAxLzA2LzIwMTQgMDc6MjMgUE0sIEFi
aGlzaGVrIEFuYW5kIHdyb3RlOg0KPj4+Pj4+Pj4+IEl0IGlzIGtub3duIHRoYXQgVUlQIGlzIGlu
Y29uc2lzdGVudCB3aXRoIHVuaXZhbGVuY2UuDQo+Pj4+Pj4+Pj4gRG9lcyB0aGlzIHR5cGVjaGVj
ayBldmVuIGFmdGVyIGRpc2FibGluZyBVSVAoPT1LIGF4aW9tPykgPw0KPj4+Pj4+Pj4+IEkgbWln
aHQgYmUgd3JvbmcsIGJ1dCBJIHRoaW5rIHRoYXQgVUlQIGlzIGJha2VkIGludG8gdGhlDQo+Pj4+
Pj4+Pj50eXBlY2hlY2tlcg0KPj4+Pj4+Pj4+IG9mIEFnZGEuDQo+Pj4+Pj4+Pj4gQnV0LCBVSVAg
Y2FuIGJlIGRpc2FibGVkIHNvbWVob3c/DQo+Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gDQo+Pj4+Pj4+
Pj4gLS0gQWJoaXNoZWsNCj4+Pj4+Pj4+PiBodHRwOi8vd3d3LmNzLmNvcm5lbGwuZWR1L35hYTc1
NS8NCj4+Pj4+Pj4+PiA8aHR0cDovL3d3dy5jcy5jb3JuZWxsLmVkdS8lN0VhYTc1NS8+DQo+Pj4+
Pj4+Pj4gDQo+Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gT24gTW9uLCBKYW4gNiwgMjAxNCBhdCAzOjQy
IFBNLCBNYXhpbWUgRKimbqiocyA8bWFpbEBtYXhpbWVkZW5lcy5mcg0KPj4+Pj4+Pj4+IDxtYWls
dG86bWFpbEBtYXhpbWVkZW5lcy5mcj4+IHdyb3RlOg0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+ICBC
aW5nbywgQWdkYSBzZWVtcyB0byBoYXZlIHRoZSBzYW1lIHByb2JsZW06DQo+Pj4+Pj4+Pj4gDQo+
Pj4+Pj4+Pj4gIG1vZHVsZSBUZXJtaW5hdGlvbiB3aGVyZQ0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+
ICBvcGVuIGltcG9ydCBSZWxhdGlvbi5CaW5hcnkuQ29yZQ0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+
ICBkYXRhIEVtcHR5IDogU2V0IHdoZXJlDQo+Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gIGRhdGEgQm94
IDogU2V0IHdoZXJlDQo+Pj4+Pj4+Pj4gIHdyYXAgOiAoRW1wdHkgofogQm94KSCh+iBCb3gNCj4+
Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgcG9zdHVsYXRlDQo+Pj4+Pj4+Pj4gIGlzbyA6IChFbXB0eSCh
+iBCb3gpIKHUIEJveA0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+ICBsb29wIDogQm94IC0+IEVtcHR5
DQo+Pj4+Pj4+Pj4gIGxvb3AgKHdyYXAgeCkgcmV3cml0ZSBpc28gPSBsb29wIHgNCj4+Pj4+Pj4+
PiANCj4+Pj4+Pj4+PiAgZ2lmdCA6IEVtcHR5IKH6IEJveA0KPj4+Pj4+Pj4+ICBnaWZ0ICgpDQo+
Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gIGJ1ZyA6IEVtcHR5DQo+Pj4+Pj4+Pj4gIGJ1ZyA9IGxvb3Ag
KHdyYXAgZ2lmdCkNCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgSG93ZXZlciwgSSBtYXkgYmUgbWlz
c2luZyBzb21ldGhpbmcgZHVlIHRvIG15IGlnbm9yYW5jZSBvZiBBZ2RhLg0KPj4+Pj4+Pj4+ICBJ
dCBtYXkgYmUgd2VsbCBrbm93biB0aGF0IHRoZSBheGlvbSBJIGludHJvZHVjZWQgaXMNCj4+Pj4+
Pj4+PmluY29uc2lzdGVudC4NCj4+Pj4+Pj4+PiAgRm9yZ2l2ZSBtZSBpZiBpdCBpcyB0aGUgY2Fz
ZS4NCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgTWF4aW1lLg0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+
IA0KPj4+Pj4+Pj4+ICBPbiAwMS8wNi8yMDE0IDAxOjE1IFBNLCBNYXhpbWUgRKimbqiocyB3cm90
ZToNCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgICAgIFRoZSBhbnRpLWV4dGVuc2lvbmFsaXR5IGJ1
ZyBpcyBpbmRlZWQgcmVsYXRlZCB0bw0KPj4+Pj4+Pj4+dGVybWluYXRpb24uDQo+Pj4+Pj4+Pj4g
ICAgICBNb3JlIHByZWNpc2VseSwgaXQgaXMgdGhlIHN1YnRlcm0gcmVsYXRpb24gdXNlZCBieSB0
aGUgZ3VhcmQNCj4+Pj4+Pj4+PiAgICAgIGNoZWNrZXIgd2hpY2ggaXMgbm90IGRlZmluZWQgcXVp
dGUgdGhlIHJpZ2h0IHdheSBvbg0KPj4+Pj4+Pj4+ZGVwZW5kZW50DQo+Pj4+Pj4+Pj4gICAgICBw
YXR0ZXJuIG1hdGNoaW5nLg0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+ICAgICAgSXQgaXMgbm90IHRv
byBoYXJkIHRvIGZpeCAod2UgaGF2ZSBhIHBhdGNoKSwgYnV0IGRvaW5nIHNvDQo+Pj4+Pj4+Pj4g
ICAgICB3aXRob3V0IHJ1bGluZyBvdXQgYW55IGludGVyZXN0aW5nIGxlZ2l0aW1hdGUgZXhhbXBs
ZQ0KPj4+Pj4+Pj4+KGRlYWxpbmcNCj4+Pj4+Pj4+PiAgICAgIHdpdGggcmVjdXJzaW9uIG9uIGRl
cGVuZGVudGx5IHR5cGVkIGRhdGEgc3RydWN0dXJlcykgaXMgbW9yZQ0KPj4+Pj4+Pj4+ICAgICAg
Y2hhbGxlbmdpbmcuDQo+Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gICAgICBJIGFtIGFsc28gY3VyaW91
cyBhcyB0byB3aGV0aGVyIEFnZGEgaXMgaW1wYWN0ZWQuIExldCdzIHRyeQ0KPj4+Pj4+Pj4+aXQN
Cj4+Pj4+Pj4+PiA6KQ0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+ICAgICAgTWF4aW1lLg0KPj4+Pj4+
Pj4+IA0KPj4+Pj4+Pj4+ICAgICAgT24gMDEvMDYvMjAxNCAxMjo1OSBQTSwgQWx0ZW5raXJjaCBU
aG9yc3RlbiB3cm90ZToNCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgICAgICAgICBXaGljaCBidWcg
d2FzIHRoaXM/DQo+Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gICAgICAgICAgSSBvbmx5IHNhdyB0aGUg
b25lIHdoaWNoIGFsbG93ZWQgeW91IHRvIHByb3ZlDQo+Pj4+Pj4+Pj4gICAgICAgICAgYW50aS1l
eHRlbnNpb25hbGl0eT8gQnV0DQo+Pj4+Pj4+Pj4gICAgICAgICAgdGhpcyB3YXNuJ3QgcmVsYXRl
ZCB0byB0ZXJtaW5hdGlvbiwgb3I/DQo+Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gICAgICAgICAgVGhv
cnN0ZW4NCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgICAgICAgICBPbiAwNi8wMS8yMDE0IDE2OjU0
LCAiQ29keSBSb3V4Ig0KPj4+Pj4+Pj4+PGNvZHkucm91eEBhbmRyZXcuY211LmVkdQ0KPj4+Pj4+
Pj4+ICAgICAgICAgIDxtYWlsdG86Y29keS5yb3V4QGFuZHJldy5jbXUuZWR1Pj4gd3JvdGU6DQo+
Pj4+Pj4+Pj4gDQo+Pj4+Pj4+Pj4gICAgICAgICAgICAgIE5pY2Ugc3VtbWFyeSENCj4+Pj4+Pj4+
PiANCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgICAgICAgICAgICAgT24gMDEvMDYvMjAxNCAwODo0
OSBBTSwgQWx0ZW5raXJjaCBUaG9yc3RlbiB3cm90ZToNCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAg
ICAgICAgICAgICAgICAgIEFnZGEgZW5mb3JjZXMgdGVybWluYXRpb24gdmlhIGEgdGVybWluYXRp
b24NCj4+Pj4+Pj4+PiAgICAgICAgICAgICAgICAgIGNoZWNrZXIgd2hpY2ggaXMgbW9yZQ0KPj4+
Pj4+Pj4+ICAgICAgICAgICAgICAgICAgZmxleGlibGUgYnV0IEkgdGhpbmsgbGVzcyBwcmluY2lw
bGVkIHRoYW4gQ29xJ3MNCj4+Pj4+Pj4+PiAgICAgICAgICAgICAgICAgIGFwcHJvYWNoLg0KPj4+
Pj4+Pj4+IA0KPj4+Pj4+Pj4+ICAgICAgICAgICAgICBUaGF0J3MgYSBiaXQgc2NhcnkgZ2l2ZW4g
dGhhdCB0aGVyZSB3YXMgYW4NCj4+Pj4+Pj4+PiAgICAgICAgICAgICAgaW5jb25zaXN0ZW5jeSBm
b3VuZCBpbg0KPj4+Pj4+Pj4+ICAgICAgICAgICAgICB0aGUgQ29xIHRlcm1pbmF0aW9uIGNoZWNr
ZXIganVzdCBhIGNvdXBsZSBvZiB3ZWVrcw0KPj4+Pj4+Pj4+YWdvDQo+Pj4+Pj4+Pj4gOikNCj4+
Pj4+Pj4+PiANCj4+Pj4+Pj4+PiAgICAgICAgICAgICAgQlRXLCBoYXMgYW55b25lIHRyaWVkIHJl
cHJvZHVjaW5nIHRoZSBidWcgaW4gQWdkYT8NCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiANCj4+Pj4+
Pj4+PiAgICAgICAgICAgICAgQ29keQ0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+ICAgICAgICAgIFRo
aXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJlIGludGVuZGVkIHNvbGVseSBmb3INCj4+
Pj4+Pj4+PiAgICAgICAgICB0aGUgYWRkcmVzc2VlIGFuZCBtYXkgY29udGFpbiBjb25maWRlbnRp
YWwgaW5mb3JtYXRpb24uDQo+Pj4+Pj4+Pj5JZg0KPj4+Pj4+Pj4+ICAgICAgICAgIHlvdSBoYXZl
IHJlY2VpdmVkIHRoaXMgbWVzc2FnZSBpbiBlcnJvciwgcGxlYXNlIHNlbmQgaXQNCj4+Pj4+Pj4+
PiAgICAgICAgICBiYWNrIHRvIG1lLCBhbmQgaW1tZWRpYXRlbHkgZGVsZXRlIGl0LiBQbGVhc2Ug
ZG8gbm90DQo+Pj4+Pj4+Pj51c2UsDQo+Pj4+Pj4+Pj4gICAgICAgICAgY29weSBvciBkaXNjbG9z
ZSB0aGUgaW5mb3JtYXRpb24gY29udGFpbmVkIGluIHRoaXMNCj4+Pj4+Pj4+Pm1lc3NhZ2UNCj4+
Pj4+Pj4+PiAgICAgICAgICBvciBpbiBhbnkgYXR0YWNobWVudC4gQW55IHZpZXdzIG9yIG9waW5p
b25zIGV4cHJlc3NlZCBieQ0KPj4+Pj4+Pj4+ICAgICAgICAgIHRoZSBhdXRob3Igb2YgdGhpcyBl
bWFpbCBkbyBub3QgbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUNCj4+Pj4+Pj4+PiAgICAgICAgICB2
aWV3cyBvZiB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtLg0KPj4+Pj4+Pj4+IA0KPj4+Pj4+
Pj4+ICAgICAgICAgIFRoaXMgbWVzc2FnZSBoYXMgYmVlbiBjaGVja2VkIGZvciB2aXJ1c2VzIGJ1
dCB0aGUNCj4+Pj4+Pj4+PmNvbnRlbnRzDQo+Pj4+Pj4+Pj4gICAgICAgICAgb2YgYW4gYXR0YWNo
bWVudA0KPj4+Pj4+Pj4+ICAgICAgICAgIG1heSBzdGlsbCBjb250YWluIHNvZnR3YXJlIHZpcnVz
ZXMgd2hpY2ggY291bGQgZGFtYWdlDQo+Pj4+Pj4+Pj55b3VyDQo+Pj4+Pj4+Pj4gICAgICAgICAg
Y29tcHV0ZXIgc3lzdGVtLCB5b3UgYXJlIGFkdmlzZWQgdG8gcGVyZm9ybSB5b3VyIG93bg0KPj4+
Pj4+Pj4+ICAgICAgICAgIGNoZWNrcy4gRW1haWwgY29tbXVuaWNhdGlvbnMgd2l0aCB0aGUgVW5p
dmVyc2l0eSBvZg0KPj4+Pj4+Pj4+ICAgICAgICAgIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3Jl
ZCBhcyBwZXJtaXR0ZWQgYnkgVUsNCj4+Pj4+Pj4+PiBsZWdpc2xhdGlvbi4NCj4+Pj4+Pj4+PiAN
Cj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+
PiAgICAgIF9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fDQo+
Pj4+Pj4+Pj4gICAgICBBZ2RhIG1haWxpbmcgbGlzdA0KPj4+Pj4+Pj4+ICAgICAgQWdkYUBsaXN0
cy5jaGFsbWVycy5zZSA8bWFpbHRvOkFnZGFAbGlzdHMuY2hhbG1lcnMuc2U+DQo+Pj4+Pj4+Pj4g
ICAgICBodHRwczovL2xpc3RzLmNoYWxtZXJzLnNlL21haWxtYW4vbGlzdGluZm8vYWdkYQ0KPj4+
Pj4+Pj4+IA0KPj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4+ICBfX19fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fXw0KPj4+Pj4+Pj4+ICBBZ2RhIG1haWxpbmcgbGlzdA0KPj4+
Pj4+Pj4+ICBBZ2RhQGxpc3RzLmNoYWxtZXJzLnNlIDxtYWlsdG86QWdkYUBsaXN0cy5jaGFsbWVy
cy5zZT4NCj4+Pj4+Pj4+PiAgaHR0cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xpc3Rp
bmZvL2FnZGENCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+PiANCj4+Pj4+Pj4+IF9fX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fDQo+Pj4+Pj4+PiBBZ2RhIG1haWxpbmcg
bGlzdA0KPj4+Pj4+Pj4gQWdkYUBsaXN0cy5jaGFsbWVycy5zZQ0KPj4+Pj4+Pj4gaHR0cHM6Ly9s
aXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xpc3RpbmZvL2FnZGENCj4+Pj4+Pj4gX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18NCj4+Pj4+Pj4gQWdkYSBtYWls
aW5nIGxpc3QNCj4+Pj4+Pj4gQWdkYUBsaXN0cy5jaGFsbWVycy5zZQ0KPj4+Pj4+PiBodHRwczov
L2xpc3RzLmNoYWxtZXJzLnNlL21haWxtYW4vbGlzdGluZm8vYWdkYQ0KPj4+Pj4gDQo+Pj4+IA0K
Pj4+IA0KPj4NCj4NCj4NCg0K