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

[Altenkirch Thorsten]

T24gMDcvMDEvMjAxNCAyMzowMywgIkNvbm9yIE1jQnJpZGUiIDxjb25vckBzdHJpY3RseXBvc2l0
aXZlLm9yZz4gd3JvdGU6DQoNCj4NCj5PbiA3IEphbiAyMDE0LCBhdCAyMjo0NywgQWx0ZW5raXJj
aCBUaG9yc3Rlbg0KPjxwc3p0eGFAZXhtYWlsLm5vdHRpbmdoYW0uYWMudWs+IHdyb3RlOg0KPg0K
Pj4gSGkgQ29ub3IsDQo+PiANCj4+IEkgYW0gc3VyZSB0aGlzIG11c3QgYmUgYSBzdHVwaWQgcXVl
c3Rpb24gYnV0IHdoeSBpcyB0aGlzIG5vdCBjb3ZlcmVkDQo+PiBieSB5b3VyIHJlc3VsdCB0aGF0
IHBhdHRlcm4gbWF0Y2hpbmcgY2FuIGJlIHJlZHVjZWQgdG8gZWxpbWluYXRvcnMgKyBLPw0KPg0K
PlRoZSByZWN1cnNpdmUgY2FsbCBpc24ndCBjb3ZlcmVkIGJ5IHRoZSBpbmR1Y3RpdmUgaHlwb3Ro
ZXNpcy4gVGhlIGRpcmVjdA0KPnZlcnNpb24NCj5naXZlcyBubyBhY2NvdW50IG9mIHRoZSBpbmR1
Y3RpdmUgaHlwb3RoZXNpcyAqYXQgYWxsKiwgaGVuY2UgdGhlIHdob2xlDQo+bWVzcy4NCj4NCj4+
Pj4+IG1vbyAod3JhcCBmKSA9IG5vbyAoWmVybyAtPiBXT25lKSBteUlzbyBmDQo+Pj4+PiBub28g
LldPbmUgUmVmbCB4ID0gbW9vIHgNCj4NCj5UaGUgcmVjdXJzaXZlIGNhbGwNCj4NCj4gIG1vbyB4
DQo+DQo+aXMgcmVhbGx5IGEgcmVjdXJzaXZlIGNhbGwNCj4NCj4gIG1vbyAoc3Vic3QgbXlJc28g
Li4uIGYpDQo+DQo+YnV0IHRoZSBpbmR1Y3RpdmUgaHlwb3RoZXNpcyB0ZWxscyB1cyBqdXN0IHRo
YXQgd2UgY2FuIGNhbGwgbW9vIG9uDQo+b3V0cHV0cyBvZiBmLg0KPg0KPkJvdHRvbSBsaW5lOiBp
dCdzIG5vdCBzdHJ1Y3R1cmFsbHkgcmVjdXJzaXZlLg0KDQpJIGtub3cgdGhpcyAtIHRoaXMgd2Fz
IHByZWNpc2VseSB0aGUgY29tbWVudCBJIG1hZGUgaW4gbXkgcmVwbHkgdG8gTWF4aW1lLg0KDQpI
b3dldmVyLCBpdCBzZWVtcyBJIGFtIGEgdmljdGltIG9mIG15IG93biBwcm9wYWdhbmRhOiBJIHdh
cyBhbHdheXMNCnRoaW5raW5nIHRoYXQgQ29ub3IncyByZXN1bHQgdGVsbHMgdXMgdGhhdCB3ZSBj
YW4gcmVwbGFjZSBwYXR0ZXJuIG1hdGNoaW5nDQood2l0aCBndWFyZGVkIHJlY3Vyc2lvbikgYnkg
ZWxpbWluYXRpb24gY29uc3RhbnRzLg0KDQpIb3dldmVyLCB0aGlzIGV4YW1wbGUgc2hvd3MgdGhh
dCB0aGlzIGlzIG5vdCB0cnVlLiBPbmNlIHdlIHBlcmZvcm0gdGhlDQp1bmlmaWNhdGlvbiByZXF1
aXJlZCBieSBwYXR0ZXJuIG1hdGNoaW5nIHdlIG9idGFpbiBhIGEgdGVybSB3aGljaCAibG9va3Mi
DQphcyBpZiBpdCBpcyBzdHJ1Y3R1cmFsbHkgc21hbGxlciBldmVuIHRob3VnaCBpdCBpc24ndC4N
Cg0KT25lIG9idmlvdXMgcXVlc3Rpb24gaXMgaG93IHdlIGNhbiByZWNvZ25pemUgZ29vZCBpbnN0
YW5jZXMgb2YgcGF0dGVybg0KbWF0Y2hpbmcgZnJvbSBiYWQgb25lcy4NCg0KVGhpcyBhbHNvIGlu
Y3JlYXNlcyB0aGUgYXJndW1lbnQgaW4gZmF2b3VyIG9mIGEgc2FmZSB2ZXJzaW9uIG9mIHBhdHRl
cm4NCm1hdGNoaW5nIHdoaWNoIGlzIGV2aWRlbmNlIHByb2R1Y2luZy4gT25lIG9mIG15IG5ldyBz
dHVkZW50cywgR2FiZQ0KRGlqa3N0cmEsIGlzIHdvcmtpbmcgb24gdGhpcyAtIG1haW5seSB0cmln
Z2VyZWQgYnkgdGhlIHdpdGhvdXQtSyBpc3N1ZS4NCkhvd2V2ZXIsIGFzIHdlIHNlZSBub3cgdGhl
cmUgYXJlIG90aGVyIGlzc3VlcyB3aGljaCB3ZW50IHVubm90aWNlZC4NCg0KQ2hlZXJzLA0KVGhv
cnN0ZW4NCg0KPg0KPkNoZWVycw0KPg0KPkNvbm9yDQo+DQo+DQo+Pj4gDQo+Pj4gbW9vJ3MgaW5w
dXQgaXMgYmlnZ2VyIHRoYW4gdGhlIHRoaXJkIGFyZ3VtZW50IGluIGl0cyBub28gY2FsbA0KPj4+
IG5vbydzIHRoaXJkIGlucHV0IGlzIHRoZSBzYW1lIGFzIHRoZSBhcmd1bWVudCBpbiBpdHMgbW9v
IGNhbGwNCj4+PiANCj4+PiBTaXplLWNoYW5nZSB0ZXJtaW5hdGlvbiwgaG93IGFyZSB5ZT8NCj4+
PiANCj4+PiBXaGVuIHlvdSBkbyB0aGUgdHJhbnNsYXRpb24gdG8gZWxpbWluYXRvcnMsIHlvdSdy
ZSBvYmxpZ2VkIHRvDQo+Pj4gc2hvdyBob3cgcmVjdXJzaXZlIGNhbGxzIGNvcnJlc3BvbmQgdG8g
aW52b2NhdGlvbnMgb2YgdGhlDQo+Pj4gaW5kdWN0aXZlIGh5cG90aGVzaXM6IGhlcmUgdGhhdCdz
IGp1c3Qgbm90IGdvaW5nIHRvIGhhcHBlbi4NCj4+PiBUcmFuc3BvcnRpbmcgZiBhY3Jvc3MgbXlJ
c28gZG9lcyBpbmRlZWQgZ2l2ZSBhbiBlbGVtZW50IG9mDQo+Pj4gV09uZSAoeW91ciBCb3gpLCBi
dXQgdGhhdCBkb2VzIG5vdCBtYWtlIGEgbnVsbGFyeSBpbmR1Y3RpdmUNCj4+PiBoeXBvdGhlc2lz
IGFueSBlYXNpZXIgdG8gaW52b2tlLg0KPj4+IA0KPj4+IEknZCBxdWl0ZSBsaWtlIHRvIHNlZSB1
cyBkZWZpbmluZyBhIHR5cGUgdGhlb3J5IGluIHdoaWNoIHRoZQ0KPj4+IG9ubHkgY2hlY2tpbmcg
aXMgdHlwZSBjaGVja2luZywgdGhlbiB1c2luZyBpdCBhcyBhIHRhcmdldCBmb3INCj4+PiBlbGFi
b3JhdGlvbi4gRWxpbWluYXRvcnMgYXJlIG9uZSBjYW5kaWRhdGUsIGJ1dCB0aGVyZSBhcmUNCj4+
PiBvdGhlcnMuIFNpemVkIHR5cGVzIGFyZSBjZXJ0YWlubHkgYW5vdGhlciBzdHJvbmcgY2FuZGlk
YXRlLg0KPj4+IEknbSBhbHNvIGludGVyZXN0ZWQgdG8gc2VlIHdoZXRoZXIgdGhlcmUgYXJlICJs
b2NhbGx5IGNsb2NrZWQiDQo+Pj4gZXhwbGFuYXRpb25zIGZvciB0ZXJtaW5hdGlvbiwgYXMgdGhl
cmUgc2VlbSB0byBiZSBmb3INCj4+PiBwcm9kdWN0aXZpdHkuDQo+Pj4gDQo+Pj4gSW50ZXJlc3Rp
bmcgdGltZXMNCj4+PiANCj4+PiBDb25vcg0KPj4+IA0KPj4+IA0KPj4+Pj4gDQo+Pj4+PiBiYWQg
OiBaZXJvDQo+Pj4+PiBiYWQgPSBtb28gKHdyYXAgXCAoKSkNCj4+Pj4+IA0KPj4+Pj4gDQo+Pj4+
PiANCj4+Pj4+PiBULg0KPj4+Pj4+IA0KPj4+Pj4+PiBJIGFtIGFsc28gbm90IHN1cmUgaG93IHNw
ZWNpZmljIHRoZSBwcm9ibGVtIGlzIHRvIHVuaXZhbGVuY2UuIEFzDQo+Pj4+Pj4+Q29keQ0KPj4+
Pj4+PiBzYWlkLCBJIHdvdWxkIGV4cGVjdCB0byBmaW5kIHNvbWUgc2V0LXRoZW9yZXRpY2FsIG1v
ZGVscyB3aGVyZSB0aGUNCj4+Pj4+Pj4gZXF1YWxpdHkgaG9sZHMuIFNvIGJlaW5nIGFibGUgdG8g
cHJvdmUgdGhlIG5lZ2F0aW9uIGlzIGRpc3R1cmJpbmcuDQo+Pj4+Pj4+IA0KPj4+Pj4+PiBNYXhp
bWUuDQo+Pj4+Pj4+IA0KPj4+Pj4+PiBPbiAwMS8wNi8yMDE0IDA3OjIzIFBNLCBBYmhpc2hlayBB
bmFuZCB3cm90ZToNCj4+Pj4+Pj4+IEl0IGlzIGtub3duIHRoYXQgVUlQIGlzIGluY29uc2lzdGVu
dCB3aXRoIHVuaXZhbGVuY2UuDQo+Pj4+Pj4+PiBEb2VzIHRoaXMgdHlwZWNoZWNrIGV2ZW4gYWZ0
ZXIgZGlzYWJsaW5nIFVJUCg9PUsgYXhpb20/KSA/DQo+Pj4+Pj4+PiBJIG1pZ2h0IGJlIHdyb25n
LCBidXQgSSB0aGluayB0aGF0IFVJUCBpcyBiYWtlZCBpbnRvIHRoZQ0KPj4+Pj4+Pj50eXBlY2hl
Y2tlcg0KPj4+Pj4+Pj4gb2YgQWdkYS4NCj4+Pj4+Pj4+IEJ1dCwgVUlQIGNhbiBiZSBkaXNhYmxl
ZCBzb21laG93Pw0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+IC0tIEFiaGlzaGVrDQo+
Pj4+Pj4+PiBodHRwOi8vd3d3LmNzLmNvcm5lbGwuZWR1L35hYTc1NS8NCj4+Pj4+Pj4+IDxodHRw
Oi8vd3d3LmNzLmNvcm5lbGwuZWR1LyU3RWFhNzU1Lz4NCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gDQo+
Pj4+Pj4+PiBPbiBNb24sIEphbiA2LCAyMDE0IGF0IDM6NDIgUE0sIE1heGltZSBEqKZuqKhzIDxt
YWlsQG1heGltZWRlbmVzLmZyDQo+Pj4+Pj4+PiA8bWFpbHRvOm1haWxAbWF4aW1lZGVuZXMuZnI+
PiB3cm90ZToNCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gIEJpbmdvLCBBZ2RhIHNlZW1zIHRvIGhhdmUg
dGhlIHNhbWUgcHJvYmxlbToNCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gIG1vZHVsZSBUZXJtaW5hdGlv
biB3aGVyZQ0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgb3BlbiBpbXBvcnQgUmVsYXRpb24uQmluYXJ5
LkNvcmUNCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gIGRhdGEgRW1wdHkgOiBTZXQgd2hlcmUNCj4+Pj4+
Pj4+IA0KPj4+Pj4+Pj4gIGRhdGEgQm94IDogU2V0IHdoZXJlDQo+Pj4+Pj4+PiAgd3JhcCA6IChF
bXB0eSCh+iBCb3gpIKH6IEJveA0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgcG9zdHVsYXRlDQo+Pj4+
Pj4+PiAgaXNvIDogKEVtcHR5IKH6IEJveCkgodQgQm94DQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+ICBs
b29wIDogQm94IC0+IEVtcHR5DQo+Pj4+Pj4+PiAgbG9vcCAod3JhcCB4KSByZXdyaXRlIGlzbyA9
IGxvb3AgeA0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgZ2lmdCA6IEVtcHR5IKH6IEJveA0KPj4+Pj4+
Pj4gIGdpZnQgKCkNCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gIGJ1ZyA6IEVtcHR5DQo+Pj4+Pj4+PiAg
YnVnID0gbG9vcCAod3JhcCBnaWZ0KQ0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgSG93ZXZlciwgSSBt
YXkgYmUgbWlzc2luZyBzb21ldGhpbmcgZHVlIHRvIG15IGlnbm9yYW5jZSBvZiBBZ2RhLg0KPj4+
Pj4+Pj4gIEl0IG1heSBiZSB3ZWxsIGtub3duIHRoYXQgdGhlIGF4aW9tIEkgaW50cm9kdWNlZCBp
cyBpbmNvbnNpc3RlbnQuDQo+Pj4+Pj4+PiAgRm9yZ2l2ZSBtZSBpZiBpdCBpcyB0aGUgY2FzZS4N
Cj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gIE1heGltZS4NCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gDQo+Pj4+
Pj4+PiAgT24gMDEvMDYvMjAxNCAwMToxNSBQTSwgTWF4aW1lIESopm6oqHMgd3JvdGU6DQo+Pj4+
Pj4+PiANCj4+Pj4+Pj4+ICAgICAgVGhlIGFudGktZXh0ZW5zaW9uYWxpdHkgYnVnIGlzIGluZGVl
ZCByZWxhdGVkIHRvIHRlcm1pbmF0aW9uLg0KPj4+Pj4+Pj4gICAgICBNb3JlIHByZWNpc2VseSwg
aXQgaXMgdGhlIHN1YnRlcm0gcmVsYXRpb24gdXNlZCBieSB0aGUgZ3VhcmQNCj4+Pj4+Pj4+ICAg
ICAgY2hlY2tlciB3aGljaCBpcyBub3QgZGVmaW5lZCBxdWl0ZSB0aGUgcmlnaHQgd2F5IG9uIGRl
cGVuZGVudA0KPj4+Pj4+Pj4gICAgICBwYXR0ZXJuIG1hdGNoaW5nLg0KPj4+Pj4+Pj4gDQo+Pj4+
Pj4+PiAgICAgIEl0IGlzIG5vdCB0b28gaGFyZCB0byBmaXggKHdlIGhhdmUgYSBwYXRjaCksIGJ1
dCBkb2luZyBzbw0KPj4+Pj4+Pj4gICAgICB3aXRob3V0IHJ1bGluZyBvdXQgYW55IGludGVyZXN0
aW5nIGxlZ2l0aW1hdGUgZXhhbXBsZQ0KPj4+Pj4+Pj4oZGVhbGluZw0KPj4+Pj4+Pj4gICAgICB3
aXRoIHJlY3Vyc2lvbiBvbiBkZXBlbmRlbnRseSB0eXBlZCBkYXRhIHN0cnVjdHVyZXMpIGlzIG1v
cmUNCj4+Pj4+Pj4+ICAgICAgY2hhbGxlbmdpbmcuDQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+ICAgICAg
SSBhbSBhbHNvIGN1cmlvdXMgYXMgdG8gd2hldGhlciBBZ2RhIGlzIGltcGFjdGVkLiBMZXQncyB0
cnkNCj4+Pj4+Pj4+aXQNCj4+Pj4+Pj4+IDopDQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+ICAgICAgTWF4
aW1lLg0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgICAgIE9uIDAxLzA2LzIwMTQgMTI6NTkgUE0sIEFs
dGVua2lyY2ggVGhvcnN0ZW4gd3JvdGU6DQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+ICAgICAgICAgIFdo
aWNoIGJ1ZyB3YXMgdGhpcz8NCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gICAgICAgICAgSSBvbmx5IHNh
dyB0aGUgb25lIHdoaWNoIGFsbG93ZWQgeW91IHRvIHByb3ZlDQo+Pj4+Pj4+PiAgICAgICAgICBh
bnRpLWV4dGVuc2lvbmFsaXR5PyBCdXQNCj4+Pj4+Pj4+ICAgICAgICAgIHRoaXMgd2Fzbid0IHJl
bGF0ZWQgdG8gdGVybWluYXRpb24sIG9yPw0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgICAgICAgICBU
aG9yc3Rlbg0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgICAgICAgICBPbiAwNi8wMS8yMDE0IDE2OjU0
LCAiQ29keSBSb3V4Ig0KPj4+Pj4+Pj48Y29keS5yb3V4QGFuZHJldy5jbXUuZWR1DQo+Pj4+Pj4+
PiAgICAgICAgICA8bWFpbHRvOmNvZHkucm91eEBhbmRyZXcuY211LmVkdT4+IHdyb3RlOg0KPj4+
Pj4+Pj4gDQo+Pj4+Pj4+PiAgICAgICAgICAgICAgTmljZSBzdW1tYXJ5IQ0KPj4+Pj4+Pj4gDQo+
Pj4+Pj4+PiANCj4+Pj4+Pj4+ICAgICAgICAgICAgICBPbiAwMS8wNi8yMDE0IDA4OjQ5IEFNLCBB
bHRlbmtpcmNoIFRob3JzdGVuIHdyb3RlOg0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAgICAgICAgICAg
ICAgICAgIEFnZGEgZW5mb3JjZXMgdGVybWluYXRpb24gdmlhIGEgdGVybWluYXRpb24NCj4+Pj4+
Pj4+ICAgICAgICAgICAgICAgICAgY2hlY2tlciB3aGljaCBpcyBtb3JlDQo+Pj4+Pj4+PiAgICAg
ICAgICAgICAgICAgIGZsZXhpYmxlIGJ1dCBJIHRoaW5rIGxlc3MgcHJpbmNpcGxlZCB0aGFuIENv
cSdzDQo+Pj4+Pj4+PiAgICAgICAgICAgICAgICAgIGFwcHJvYWNoLg0KPj4+Pj4+Pj4gDQo+Pj4+
Pj4+PiAgICAgICAgICAgICAgVGhhdCdzIGEgYml0IHNjYXJ5IGdpdmVuIHRoYXQgdGhlcmUgd2Fz
IGFuDQo+Pj4+Pj4+PiAgICAgICAgICAgICAgaW5jb25zaXN0ZW5jeSBmb3VuZCBpbg0KPj4+Pj4+
Pj4gICAgICAgICAgICAgIHRoZSBDb3EgdGVybWluYXRpb24gY2hlY2tlciBqdXN0IGEgY291cGxl
IG9mIHdlZWtzDQo+Pj4+Pj4+PmFnbw0KPj4+Pj4+Pj4gOikNCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4g
ICAgICAgICAgICAgIEJUVywgaGFzIGFueW9uZSB0cmllZCByZXByb2R1Y2luZyB0aGUgYnVnIGlu
IEFnZGE/DQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gICAgICAgICAgICAgIENvZHkN
Cj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gICAgICAgICAgVGhpcyBtZXNzYWdlIGFuZCBhbnkgYXR0YWNo
bWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvcg0KPj4+Pj4+Pj4gICAgICAgICAgdGhlIGFkZHJl
c3NlZSBhbmQgbWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9ybWF0aW9uLg0KPj4+Pj4+Pj5J
Zg0KPj4+Pj4+Pj4gICAgICAgICAgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcyBtZXNzYWdlIGluIGVy
cm9yLCBwbGVhc2Ugc2VuZCBpdA0KPj4+Pj4+Pj4gICAgICAgICAgYmFjayB0byBtZSwgYW5kIGlt
bWVkaWF0ZWx5IGRlbGV0ZSBpdC4gUGxlYXNlIGRvIG5vdCB1c2UsDQo+Pj4+Pj4+PiAgICAgICAg
ICBjb3B5IG9yIGRpc2Nsb3NlIHRoZSBpbmZvcm1hdGlvbiBjb250YWluZWQgaW4gdGhpcw0KPj4+
Pj4+Pj5tZXNzYWdlDQo+Pj4+Pj4+PiAgICAgICAgICBvciBpbiBhbnkgYXR0YWNobWVudC4gQW55
IHZpZXdzIG9yIG9waW5pb25zIGV4cHJlc3NlZCBieQ0KPj4+Pj4+Pj4gICAgICAgICAgdGhlIGF1
dGhvciBvZiB0aGlzIGVtYWlsIGRvIG5vdCBuZWNlc3NhcmlseSByZWZsZWN0IHRoZQ0KPj4+Pj4+
Pj4gICAgICAgICAgdmlld3Mgb2YgdGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4NCj4+Pj4+
Pj4+IA0KPj4+Pj4+Pj4gICAgICAgICAgVGhpcyBtZXNzYWdlIGhhcyBiZWVuIGNoZWNrZWQgZm9y
IHZpcnVzZXMgYnV0IHRoZQ0KPj4+Pj4+Pj5jb250ZW50cw0KPj4+Pj4+Pj4gICAgICAgICAgb2Yg
YW4gYXR0YWNobWVudA0KPj4+Pj4+Pj4gICAgICAgICAgbWF5IHN0aWxsIGNvbnRhaW4gc29mdHdh
cmUgdmlydXNlcyB3aGljaCBjb3VsZCBkYW1hZ2UNCj4+Pj4+Pj4+eW91cg0KPj4+Pj4+Pj4gICAg
ICAgICAgY29tcHV0ZXIgc3lzdGVtLCB5b3UgYXJlIGFkdmlzZWQgdG8gcGVyZm9ybSB5b3VyIG93
bg0KPj4+Pj4+Pj4gICAgICAgICAgY2hlY2tzLiBFbWFpbCBjb21tdW5pY2F0aW9ucyB3aXRoIHRo
ZSBVbml2ZXJzaXR5IG9mDQo+Pj4+Pj4+PiAgICAgICAgICBOb3R0aW5naGFtIG1heSBiZSBtb25p
dG9yZWQgYXMgcGVybWl0dGVkIGJ5IFVLDQo+Pj4+Pj4+PiBsZWdpc2xhdGlvbi4NCj4+Pj4+Pj4+
IA0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+IA0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+PiAg
ICAgIF9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fDQo+Pj4+
Pj4+PiAgICAgIEFnZGEgbWFpbGluZyBsaXN0DQo+Pj4+Pj4+PiAgICAgIEFnZGFAbGlzdHMuY2hh
bG1lcnMuc2UgPG1haWx0bzpBZ2RhQGxpc3RzLmNoYWxtZXJzLnNlPg0KPj4+Pj4+Pj4gICAgICBo
dHRwczovL2xpc3RzLmNoYWxtZXJzLnNlL21haWxtYW4vbGlzdGluZm8vYWdkYQ0KPj4+Pj4+Pj4g
DQo+Pj4+Pj4+PiANCj4+Pj4+Pj4+ICBfX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fX19fXw0KPj4+Pj4+Pj4gIEFnZGEgbWFpbGluZyBsaXN0DQo+Pj4+Pj4+PiAgQWdk
YUBsaXN0cy5jaGFsbWVycy5zZSA8bWFpbHRvOkFnZGFAbGlzdHMuY2hhbG1lcnMuc2U+DQo+Pj4+
Pj4+PiAgaHR0cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xpc3RpbmZvL2FnZGENCj4+
Pj4+Pj4+IA0KPj4+Pj4+Pj4gDQo+Pj4+Pj4+IF9fX19fX19fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fDQo+Pj4+Pj4+IEFnZGEgbWFpbGluZyBsaXN0DQo+Pj4+Pj4+IEFn
ZGFAbGlzdHMuY2hhbG1lcnMuc2UNCj4+Pj4+Pj4gaHR0cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9t
YWlsbWFuL2xpc3RpbmZvL2FnZGENCj4+Pj4+PiBfX19fX19fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fXw0KPj4+Pj4+IEFnZGEgbWFpbGluZyBsaXN0DQo+Pj4+Pj4gQWdk
YUBsaXN0cy5jaGFsbWVycy5zZQ0KPj4+Pj4+IGh0dHBzOi8vbGlzdHMuY2hhbG1lcnMuc2UvbWFp
bG1hbi9saXN0aW5mby9hZ2RhDQo+Pj4+IA0KPj4+IA0KPj4gDQo+DQoNCg0K