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

[Altenkirch Thorsten]

DQoNCk9uIDA3LzAxLzIwMTQgMTA6MDEsICJGcqimZKimcmljIEJsYW5xdWkiIDxmcmVkZXJpYy5i
bGFucXVpQGlucmlhLmZyPiB3cm90ZToNCg0KPkhlbGxvIFRob3JzdGVuLg0KPg0KPkxlIDA3LzAx
LzIwMTQgMTA6MTksIEFsdGVua2lyY2ggVGhvcnN0ZW4gYSCopmNyaXQgOg0KPj4NCj4+IE9uIDA2
LzAxLzIwMTQgMjM6NDUsICJDb2R5IFJvdXgiIDxjb2R5LnJvdXhAYW5kcmV3LmNtdS5lZHU+IHdy
b3RlOg0KPj4NCj4+PiBPbiAwMS8wNi8yMDE0IDA2OjM2IFBNLCBWbGFkaW1pciBWb2V2b2Rza3kg
d3JvdGU6DQo+Pj4+IEluIG15IG9waW5pb24gb25seSB0aG9zZSBjb25zdHJ1Y3Rpb25zIHdoaWNo
IGNhbiBiZSBleHByZXNzZWQgdGhyb3VnaA0KPj4+PiBlbGltaW5hdG9ycyBhcmUgdHJ1c3R3b3J0
aHkuIFRoZXJlIGlzIHJlYWxseSBubyBvdGhlciB3YXkgdG8gc3VwcGx5DQo+Pj4+IHJpZ29yb3Vz
bmVzcyB0byBpbmR1Y3RpdmUgdHlwZXMgd2l0aCAgcHNldWRvLXBhcmFtZXRlcnMgKG9yIHdoYXRl
dmVyDQo+Pj4+IHRoZXkgYXJlIG5vdyBjYWxsZWQpIHN1Y2ggYXMgSWQtdHlwZXMuDQo+Pj4gVGhp
cyBpcyBzaW1wbHkgbm90IHRydWUsIHRoZXJlIGFyZSB3aG9sZSBQaERzIGRlZGljYXRlZCB0byBk
ZXNjcmliaW5nDQo+Pj4gc3lzdGVtcyB3aGljaCBjYW4gZG8gYmV0dGVyIHRoYW4gZWxpbWluYXRv
cnMuIEFuZHJlYXMgbWVudGlvbmVkDQo+Pj4gc2l6ZWQtdHlwZXMsIHdoaWNoIGFyZSBJTU8gdGhl
IG1vc3QgbWF0dXJlIGNhbmRpZGF0ZS4NCj4+IEEgY29udmluY2luZyB3YXkgdG8ganVzdGlmeSB0
aG9zZSBzeXN0ZW1zIHdvdWxkIGJlIHRvIHByb3ZpZGUgYQ0KPj4gdHJhbnNsYXRpb24gaW50byBl
bGltaW5hdG9ycy4gSSBzdWdnZXN0ZWQgdGhpcyB0byBBbmRyZWFzIGEgd2hpbGUgYWdvLg0KPj4+
IFRoZSBmYWN0IHRoYXQgdGhlIGltcGxlbWVudGF0aW9uIGlzIGJlaGluZCB0aGUgdGhlb3JldGlj
YWwgY2FwYWJpbGl0aWVzDQo+Pj4gaXMganVzdCB0aGF0LCBhbiBpbXBsZW1lbnRhdGlvbiBwcm9i
bGVtLg0KPj4gVGhlIGVsaW1pbmF0b3JzIGFyZSBsaWtlIGF4aW9tcyBpbiBzZXQgdGhlb3J5IGFu
ZCBpdCBpcyB3b3J0aHdoaWxlIHRvDQo+PiB0cmFuc2xhdGUgYW55IGV4dGVuc2lvbiBieSByZWR1
Y2luZyB0aGVtIHRvIHRoZSBheGlvbSBpbnN0ZWFkIG9mIGFkZGluZw0KPj4gbmV3IG9uZXMgZXZl
biB0aG91Z2ggdGhleSBtYXkgYmUgc2VtYW50aWNhbGx5IGp1c3RpZmllZC4NCj4NCj5Ob3dhZGF5
cywgb25lIGNhbiBhdXRvbWF0aWNhbGx5IGNlcnRpZnkgaW4gcHJvb2YgYXNzaXN0YW50cyBsaWtl
IENvcSBvcg0KPklzYWJlbGxlL0hPTCBxdWl0ZSBjb21wbGV4IHRlcm1pbmF0aW9uIHByb29mcyAo
c2VlIHRoZSB3ZWJzaXRlIG9mIHRoZQ0KPnRlcm1pbmF0aW9uIGNvbXBldGl0aW9uIGh0dHA6Ly90
ZXJtY29tcC51aWJrLmFjLmF0L3Rlcm1jb21wL2hvbWUuc2VhbSkuDQo+U28sIGl0IHdvdWxkIGJl
IGEgcGl0eSBub3QgdG8gdGFrZSBhZHZhbnRhZ2Ugb2YgdGhpcyBmb3IgbWFraW5nIHRoZSBsaWZl
DQo+b2YgcHJvb2YgYXNzaXN0YW50cyB1c2VycyBlYXNpZXIsIGFuZCBhbGxvdyB0aGVtIHRvIGRl
ZmluZSBmdW5jdGlvbnMgKG9yDQo+ZW5yaWNoIHRoZSBlcXVpdmFsZW5jZSBvbiB0eXBlcykgaW4g
d2F5cyB0aGF0IGNhbiBoYXJkbHkgKG9yIGNhbm5vdCkgYmUNCj50cmFuc2xhdGVkIGludG8gZWxp
bWluYXRvcnMuDQoNCldoYXQgdGVybWluYXRpb24gYXJndW1lbnRzIGFyZSBub3QgcHJvdmFibGUg
aW4gVHlwZSBUaGVvcnk/DQoNCk9rLCBJIGJ1eSB0aGUgYXJndW1lbnQgdGhhdCB3ZSB3YW50IHRv
IG1ha2UgY29udmVyc2lvbiBzdHJvbmdlci4gVGhlcmUgaXMNCnlvdXIgd29yayB3aXRoIEplYW4t
UGllcnJlIGFuZCBtb3JlIHJlY2VudGx5IENvbm9yJ3MgcHJvcG9zYWwgaG93IHRvIGFkZA0KZXF1
YXRpb25zIHRvIGNvbnZlcnNpb24uDQoNCkhvd2V2ZXIsIHRoZSBlcXVhdGlvbnMgd2UgYWRkIGFy
ZSBvbiBlbGVtZW50cyBvZiBTZXRzICg9IDAtdHJ1bmNhdGVkIHR5cGVzDQppbiB0aGUgc2Vuc2Ug
b2YgSG9UVCkgYW5kIHByb3ZhYmxlIHVzaW5nIHRoZSBlbGltaW5hdG9ycy4gSGVuY2UgSSB3b3Vs
ZA0KZ3Vlc3MgdGhhdCB0aGVyZSBzaG91bGQgYmUgYSB3YXkgdG8gcmVkdWNlIHRoZSBlbnJpY2hl
ZCB0aGVvcnkgdG8gdGhlDQpiYXNpYyB0aGVvcnkuIFRoYXQgaXMgZm9yIGFueSB0aGVvcmVtIHlv
dSBjYW4gcHJvdmUgaW4gdGhlIGVucmljaGVkIHRoZW9yeQ0KdGhlcmUgaXMgYSBjb3JyZXNwb25k
aW5nIG9uZSBpbiB0aGUgYmFzaWMgdGhlb3J5IHdoaWNoIHVzZXMgc29tZQ0KYWRkaXRpb25hbCBl
cXVhbGl0eSBjb2VyY2lvbnMuIEkgYW0gdGhpbmtpbmcgb2YgYSByZXN1bHQgc2ltaWxhciB0bw0K
TWFydGluLUhvZm1hbm4ncyBjb25zZXJ2YXRpdml0eSByZXN1bHQgZm9yIGV4dGVuc2lvbmFsIHR5
cGUgdGhlb3J5Lg0KDQpIZW5jZSwgSSBkbyB0aGluayB0aGF0IHN1Y2ggZXh0ZW5zaW9ucyBjYW4g
YmUganVzdGlmaWVkIGJ5IGEgdHJhbnNsYXRpb24NCmludG8gYmFzaWMgcmVjdXJzb3JzLg0KDQo+
VGhpcyBpcyBmb3IgaW5zdGFuY2UgdGhlIGNhc2Ugb2YgZnVuY3Rpb24NCj5kZWZpbml0aW9ucyBi
YXNlZCBvbiBnZW5lcmFsIHJld3JpdGluZyB0aGVvcnkuIFRoaXMgb2YgY291cnNlIG1heSByYWlz
ZQ0KPnByb2JsZW1zIGZvciBtYWtpbmcgc3VyZSB0aGF0IHN1Y2ggZGVmaW5pdGlvbnMgYXJlIGNv
bnNpc3RlbnQsIGJ1dCBpdCBpcw0KPmFub3RoZXIgKGludGVyZXN0aW5nKSBwcm9ibGVtLg0KDQpZ
ZXMsIGFuZCBvbmUgd2F5IHRvIHRoZW0gY29uc2lzdGVudCBpcyBieSB0cmFuc2xhdGluZyB0aGVt
IHRvIGJhc2ljDQpyZWN1cnNvcnMuDQoNClRob3JzdGVuDQoNCj4NCj5SZWdhcmRzLA0KPg0KPkZy
qKZkqKZyaWMuDQo+DQo+PiBUaG9yc3Rlbg0KPj4NCj4+DQo+Pj4gQmVzdCwNCj4+Pg0KPj4+IENv
ZHkNCj4+Pg0KPj4+DQo+Pj4+IFYuDQo+Pj4+DQo+Pj4+DQo+Pj4+IE9uIEphbiA2LCAyMDE0LCBh
dCA2OjI3IFBNLCBDb2R5IFJvdXggPGNvZHkucm91eEBhbmRyZXcuY211LmVkdT4NCj4+Pj53cm90
ZToNCj4+Pj4NCj4+Pj4+IFRoZSB0aGluZyBhYm91dCBDb3EgaXMgdGhhdCBpdCdzIHZlcnkgZGlz
dHVyYmluZyBub3QgdG8gaGF2ZSBhDQo+Pj4+PiBTZXQtdGhlb3JldGljIGludGVycHJldGF0aW9u
IHdoZXJlIFByb3AgaXMgdGhlIHNldCBvZiBCb29sZWFucyB7VHJ1ZSwNCj4+Pj4+IEZhbHNlfS4g
QWdkYSBvZiBjb3Vyc2UgZG9lc24ndCBoYXZlIHRoZXNlIHF1YWxtcywgYnV0IHRoZSBmYWN0IHRo
YXQNCj4+Pj4+IHRoaXMNCj4+Pj4+IGlzc3VlIGFwcGVhcnMgaW4gQ29xIHdpdGhvdXQgdXNlIG9m
IGFueXRoaW5nIGZhbmN5IChpbXByZWRpY2F0aXZpdHksDQo+Pj4+PiBldGMpIG1ha2VzIG1lIHN0
aWxsIGEgYml0IHdvcnJpZWQuIEluIHBhcnRpY3VsYXIgdGhlcmUgc2hvdWxkIGJlIGENCj4+Pj4+
IFNldC10aGVvcmV0aWMgbW9kZWwgZm9yIEFnZGEgd2hlcmUgRW1wdHkgLT4gQm94IGFuZCBCb3gg
LWFyZS0gZXF1YWw6DQo+Pj4+PiB3aXRoIGEgc3VmZmljaWVudGx5IGNsZXZlciBpbnRlcnByZXRh
dGlvbiBvZiBpbmR1Y3RpdmVzLCBJIGJlbGlldmUgSQ0KPj4+Pj4gY2FuDQo+Pj4+PiBnZXQgW1tF
bXB0eSAtPiBCb3ggXV0gPSBbW0JveF1dID0geyB7fSB9ICh3aGVyZSB7fSBpcyBqdXN0IHRoZSBl
bXB0eQ0KPj4+Pj4gc2V0KS4gQ2FuIHNvbWVvbmUgd2l0aCBtb3JlIEFnZGEga25vd2xlZGdlIHRy
eSB0byB0eXBlIHRoZSBvcmlnaW5hbA0KPj4+Pj4gcHJvYmxlbWF0aWMgdGVybT8NCj4+Pj4+DQo+
Pj4+Pg0KPj4+Pj4gSHlwb3RoZXNpcyBIZXEgOiAoRmFsc2UgLT4gRmFsc2UpID0gVHJ1ZS4NCj4+
Pj4+DQo+Pj4+PiBGaXhwb2ludCBjb250cmFkaWN0aW9uICh1IDogVHJ1ZSkgOiBGYWxzZSA6PQ0K
Pj4+Pj4gY29udHJhZGljdGlvbiAoDQo+Pj4+PiBtYXRjaCBIZXEgaW4gKF8gPSBUKSByZXR1cm4g
VCB3aXRoDQo+Pj4+PiB8IGVxX3JlZmwgPT4gZnVuIGY6RmFsc2UgPT4gbWF0Y2ggZiB3aXRoIGVu
ZA0KPj4+Pj4gZW5kDQo+Pj4+PiApLg0KPj4+Pj4NCj4+Pj4+DQo+Pj4+Pg0KPj4+Pj4gT24gMDEv
MDYvMjAxNCAwNjoxMiBQTSwgQWx0ZW5raXJjaCBUaG9yc3RlbiB3cm90ZToNCj4+Pj4+PiBIaSBN
YXhpbWUsDQo+Pj4+Pj4NCj4+Pj4+PiB5b3VyIHBvc3R1bGF0ZSBzZWVtcyBjb3JyZWN0IHNpbmNl
IGNlcnRhaW5seSBFbXB0eSCh+iBCb3ggYW5kIEJveCBhcmUNCj4+Pj4+PiBpc29tb3JwaGljIGFu
ZCBoZW5jZSBlcXVhbCBhcyBhIGNvbnNlcXVlbmNlIG9mIHVuaXZhbGVuY2UuDQo+Pj4+Pj4NCj4+
Pj4+PiBIb3dldmVyLCBJIHRoaW5rIHRoZSBkZWZpbml0aW9uIG9mIGxvb3AgbG9va3Mgc3VzcGlj
aW91cyBpbiB0aGUNCj4+Pj4+PiBwcmVzZW5jZQ0KPj4+Pj4+IG9mIHByb29mLXJlbGV2YW50IGVx
dWFsaXR5OiBpZiB3ZSByZXBsYWNlIHJld3JpdGUgYnkgYW4gZXhwbGljaXQgdXNlDQo+Pj4+Pj4g
b2YNCj4+Pj4+PiBzdWJzdCwgbG9vcCBpc24ndCBzdHJ1Y3R1cmFsIHJlY3Vyc2l2ZSBhbnltb3Jl
LiBIZW5jZSBteSBkaWFnbm9zaXMNCj4+Pj4+PiB3b3VsZA0KPj4+Pj4+IGJlIHRoYXQgcmV3cml0
ZSBpcyBzaW1wbHkgaW5jb21wYXRpYmxlIHdpdGggdW5pdmFsZW5jZS4NCj4+Pj4+Pg0KPj4+Pj4+
IENoZWVycywNCj4+Pj4+PiBUaG9yc3Rlbg0KPj4+Pj4+DQo+Pj4+Pj4gT24gMDYvMDEvMjAxNCAy
MDo0MiwgIk1heGltZSBEqKZuqKhzIiA8bWFpbEBtYXhpbWVkZW5lcy5mcj4gd3JvdGU6DQo+Pj4+
Pj4NCj4+Pj4+Pj4gQmluZ28sIEFnZGEgc2VlbXMgdG8gaGF2ZSB0aGUgc2FtZSBwcm9ibGVtOg0K
Pj4+Pj4+Pg0KPj4+Pj4+PiBtb2R1bGUgVGVybWluYXRpb24gd2hlcmUNCj4+Pj4+Pj4NCj4+Pj4+
Pj4gb3BlbiBpbXBvcnQgUmVsYXRpb24uQmluYXJ5LkNvcmUNCj4+Pj4+Pj4NCj4+Pj4+Pj4gZGF0
YSBFbXB0eSA6IFNldCB3aGVyZQ0KPj4+Pj4+Pg0KPj4+Pj4+PiBkYXRhIEJveCA6IFNldCB3aGVy
ZQ0KPj4+Pj4+PiB3cmFwIDogKEVtcHR5IKH6IEJveCkgofogQm94DQo+Pj4+Pj4+DQo+Pj4+Pj4+
IHBvc3R1bGF0ZQ0KPj4+Pj4+PiBpc28gOiAoRW1wdHkgofogQm94KSCh1CBCb3gNCj4+Pj4+Pj4N
Cj4+Pj4+Pj4gbG9vcCA6IEJveCAtPiBFbXB0eQ0KPj4+Pj4+PiBsb29wICh3cmFwIHgpIHJld3Jp
dGUgaXNvID0gbG9vcCB4DQo+Pj4+Pj4+DQo+Pj4+Pj4+IGdpZnQgOiBFbXB0eSCh+iBCb3gNCj4+
Pj4+Pj4gZ2lmdCAoKQ0KPj4+Pj4+Pg0KPj4+Pj4+PiBidWcgOiBFbXB0eQ0KPj4+Pj4+PiBidWcg
PSBsb29wICh3cmFwIGdpZnQpDQo+Pj4+Pj4+DQo+Pj4+Pj4+IEhvd2V2ZXIsIEkgbWF5IGJlIG1p
c3Npbmcgc29tZXRoaW5nIGR1ZSB0byBteSBpZ25vcmFuY2Ugb2YgQWdkYS4gSXQNCj4+Pj4+Pj4g
bWF5DQo+Pj4+Pj4+IGJlIHdlbGwga25vd24gdGhhdCB0aGUgYXhpb20gSSBpbnRyb2R1Y2VkIGlz
IGluY29uc2lzdGVudC4gRm9yZ2l2ZQ0KPj4+Pj4+PiBtZSBpZg0KPj4+Pj4+PiBpdCBpcyB0aGUg
Y2FzZS4NCj4+Pj4+Pj4NCj4+Pj4+Pj4gTWF4aW1lLg0KPj4+Pj4+Pg0KPj4+Pj4+PiBPbiAwMS8w
Ni8yMDE0IDAxOjE1IFBNLCBNYXhpbWUgRKimbqiocyB3cm90ZToNCj4+Pj4+Pj4+IFRoZSBhbnRp
LWV4dGVuc2lvbmFsaXR5IGJ1ZyBpcyBpbmRlZWQgcmVsYXRlZCB0byB0ZXJtaW5hdGlvbi4gTW9y
ZQ0KPj4+Pj4+Pj4gcHJlY2lzZWx5LCBpdCBpcyB0aGUgc3VidGVybSByZWxhdGlvbiB1c2VkIGJ5
IHRoZSBndWFyZCBjaGVja2VyDQo+Pj4+Pj4+PiB3aGljaA0KPj4+Pj4+Pj4gaXMgbm90IGRlZmlu
ZWQgcXVpdGUgdGhlIHJpZ2h0IHdheSBvbiBkZXBlbmRlbnQgcGF0dGVybiBtYXRjaGluZy4NCj4+
Pj4+Pj4+DQo+Pj4+Pj4+PiBJdCBpcyBub3QgdG9vIGhhcmQgdG8gZml4ICh3ZSBoYXZlIGEgcGF0
Y2gpLCBidXQgZG9pbmcgc28gd2l0aG91dA0KPj4+Pj4+Pj4gcnVsaW5nIG91dCBhbnkgaW50ZXJl
c3RpbmcgbGVnaXRpbWF0ZSBleGFtcGxlIChkZWFsaW5nIHdpdGgNCj4+Pj4+Pj4+IHJlY3Vyc2lv
bg0KPj4+Pj4+Pj4gb24gZGVwZW5kZW50bHkgdHlwZWQgZGF0YSBzdHJ1Y3R1cmVzKSBpcyBtb3Jl
IGNoYWxsZW5naW5nLg0KPj4+Pj4+Pj4NCj4+Pj4+Pj4+IEkgYW0gYWxzbyBjdXJpb3VzIGFzIHRv
IHdoZXRoZXIgQWdkYSBpcyBpbXBhY3RlZC4gTGV0J3MgdHJ5IGl0IDopDQo+Pj4+Pj4+Pg0KPj4+
Pj4+Pj4gTWF4aW1lLg0KPj4+Pj4+Pj4NCj4+Pj4+Pj4+IE9uIDAxLzA2LzIwMTQgMTI6NTkgUE0s
IEFsdGVua2lyY2ggVGhvcnN0ZW4gd3JvdGU6DQo+Pj4+Pj4+Pj4gV2hpY2ggYnVnIHdhcyB0aGlz
Pw0KPj4+Pj4+Pj4+DQo+Pj4+Pj4+Pj4gSSBvbmx5IHNhdyB0aGUgb25lIHdoaWNoIGFsbG93ZWQg
eW91IHRvIHByb3ZlDQo+Pj4+Pj4+Pj5hbnRpLWV4dGVuc2lvbmFsaXR5Pw0KPj4+Pj4+Pj4+IEJ1
dA0KPj4+Pj4+Pj4+IHRoaXMgd2Fzbid0IHJlbGF0ZWQgdG8gdGVybWluYXRpb24sIG9yPw0KPj4+
Pj4+Pj4+DQo+Pj4+Pj4+Pj4gVGhvcnN0ZW4NCj4+Pj4+Pj4+Pg0KPj4+Pj4+Pj4+IE9uIDA2LzAx
LzIwMTQgMTY6NTQsICJDb2R5IFJvdXgiIDxjb2R5LnJvdXhAYW5kcmV3LmNtdS5lZHU+DQo+Pj4+
Pj4+Pj53cm90ZToNCj4+Pj4+Pj4+Pg0KPj4+Pj4+Pj4+PiBOaWNlIHN1bW1hcnkhDQo+Pj4+Pj4+
Pj4+DQo+Pj4+Pj4+Pj4+DQo+Pj4+Pj4+Pj4+IE9uIDAxLzA2LzIwMTQgMDg6NDkgQU0sIEFsdGVu
a2lyY2ggVGhvcnN0ZW4gd3JvdGU6DQo+Pj4+Pj4+Pj4+PiBBZ2RhIGVuZm9yY2VzIHRlcm1pbmF0
aW9uIHZpYSBhIHRlcm1pbmF0aW9uIGNoZWNrZXIgd2hpY2ggaXMNCj4+Pj4+Pj4+Pj4+bW9yZQ0K
Pj4+Pj4+Pj4+Pj4gZmxleGlibGUgYnV0IEkgdGhpbmsgbGVzcyBwcmluY2lwbGVkIHRoYW4gQ29x
J3MgYXBwcm9hY2guDQo+Pj4+Pj4+Pj4+IFRoYXQncyBhIGJpdCBzY2FyeSBnaXZlbiB0aGF0IHRo
ZXJlIHdhcyBhbiBpbmNvbnNpc3RlbmN5IGZvdW5kDQo+Pj4+Pj4+Pj4+aW4NCj4+Pj4+Pj4+Pj4g
dGhlIENvcSB0ZXJtaW5hdGlvbiBjaGVja2VyIGp1c3QgYSBjb3VwbGUgb2Ygd2Vla3MgYWdvIDop
DQo+Pj4+Pj4+Pj4+DQo+Pj4+Pj4+Pj4+IEJUVywgaGFzIGFueW9uZSB0cmllZCByZXByb2R1Y2lu
ZyB0aGUgYnVnIGluIEFnZGE/DQo+Pj4+Pj4+Pj4+DQo+Pj4+Pj4+Pj4+DQo+Pj4+Pj4+Pj4+IENv
ZHkNCj4+Pj4+Pj4+PiBUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRhY2htZW50IGFyZSBpbnRlbmRl
ZCBzb2xlbHkgZm9yIHRoZQ0KPj4+Pj4+Pj4+IGFkZHJlc3NlZQ0KPj4+Pj4+Pj4+IGFuZCBtYXkg
Y29udGFpbiBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlvdSBoYXZlIHJlY2VpdmVkDQo+
Pj4+Pj4+Pj50aGlzDQo+Pj4+Pj4+Pj4gbWVzc2FnZSBpbiBlcnJvciwgcGxlYXNlIHNlbmQgaXQg
YmFjayB0byBtZSwgYW5kIGltbWVkaWF0ZWx5DQo+Pj4+Pj4+Pj5kZWxldGUNCj4+Pj4+Pj4+PiBp
dC4gUGxlYXNlIGRvIG5vdCB1c2UsIGNvcHkgb3IgZGlzY2xvc2UgdGhlIGluZm9ybWF0aW9uIGNv
bnRhaW5lZA0KPj4+Pj4+Pj4+IGluDQo+Pj4+Pj4+Pj4gdGhpcyBtZXNzYWdlIG9yIGluIGFueSBh
dHRhY2htZW50LiBBbnkgdmlld3Mgb3Igb3BpbmlvbnMNCj4+Pj4+Pj4+PmV4cHJlc3NlZA0KPj4+
Pj4+Pj4+IGJ5DQo+Pj4+Pj4+Pj4gdGhlIGF1dGhvciBvZiB0aGlzIGVtYWlsIGRvIG5vdCBuZWNl
c3NhcmlseSByZWZsZWN0IHRoZSB2aWV3cyBvZg0KPj4+Pj4+Pj4+IHRoZQ0KPj4+Pj4+Pj4+IFVu
aXZlcnNpdHkgb2YgTm90dGluZ2hhbS4NCj4+Pj4+Pj4+Pg0KPj4+Pj4+Pj4+IFRoaXMgbWVzc2Fn
ZSBoYXMgYmVlbiBjaGVja2VkIGZvciB2aXJ1c2VzIGJ1dCB0aGUgY29udGVudHMgb2YgYW4NCj4+
Pj4+Pj4+PiBhdHRhY2htZW50DQo+Pj4+Pj4+Pj4gbWF5IHN0aWxsIGNvbnRhaW4gc29mdHdhcmUg
dmlydXNlcyB3aGljaCBjb3VsZCBkYW1hZ2UgeW91cg0KPj4+Pj4+Pj4+Y29tcHV0ZXINCj4+Pj4+
Pj4+PiBzeXN0ZW0sIHlvdSBhcmUgYWR2aXNlZCB0byBwZXJmb3JtIHlvdXIgb3duIGNoZWNrcy4g
RW1haWwNCj4+Pj4+Pj4+PiBjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5v
dHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZA0KPj4+Pj4+Pj4+IGFzDQo+Pj4+Pj4+Pj4gcGVybWl0
dGVkIGJ5IFVLIGxlZ2lzbGF0aW9uLg0KPj4+Pj4+Pj4+DQo+Pj4+Pj4+Pj4NCj4+Pj4+Pj4+Pg0K
Pj4+Pj4+Pj4+DQo+Pj4+Pj4+PiBfX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fXw0KPj4+Pj4+Pj4gQWdkYSBtYWlsaW5nIGxpc3QNCj4+Pj4+Pj4+IEFnZGFAbGlz
dHMuY2hhbG1lcnMuc2UNCj4+Pj4+Pj4+IGh0dHBzOi8vbGlzdHMuY2hhbG1lcnMuc2UvbWFpbG1h
bi9saXN0aW5mby9hZ2RhDQo+DQo+LS0NCj5Zb3UgcmVjZWl2ZWQgdGhpcyBtZXNzYWdlIGJlY2F1
c2UgeW91IGFyZSBzdWJzY3JpYmVkIHRvIHRoZSBHb29nbGUgR3JvdXBzDQo+IkhvbW90b3B5IFR5
cGUgVGhlb3J5IiBncm91cC4NCj5UbyB1bnN1YnNjcmliZSBmcm9tIHRoaXMgZ3JvdXAgYW5kIHN0
b3AgcmVjZWl2aW5nIGVtYWlscyBmcm9tIGl0LCBzZW5kIGFuDQo+ZW1haWwgdG8gSG9tb3RvcHlU
eXBlVGhlb3J5K3Vuc3Vic2NyaWJlQGdvb2dsZWdyb3Vwcy5jb20uDQo+Rm9yIG1vcmUgb3B0aW9u
cywgdmlzaXQgaHR0cHM6Ly9ncm91cHMuZ29vZ2xlLmNvbS9ncm91cHMvb3B0X291dC4NCg0K