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

[Altenkirch Thorsten]

SGkgQ29ub3IsDQoNCkkgYW0gc3VyZSB0aGlzIG11c3QgYmUgYSBzdHVwaWQgcXVlc3Rpb24gYnV0
IHdoeSBpcyB0aGlzIG5vdCBjb3ZlcmVkDQpieSB5b3VyIHJlc3VsdCB0aGF0IHBhdHRlcm4gbWF0
Y2hpbmcgY2FuIGJlIHJlZHVjZWQgdG8gZWxpbWluYXRvcnMgKyBLPw0KDQpDaGVlcnMsDQpUaG9y
c3Rlbg0KDQpPbiAwNy8wMS8yMDE0IDE3OjI1LCAiQ29ub3IgTWNCcmlkZSIgPGNvbm9yQHN0cmlj
dGx5cG9zaXRpdmUub3JnPiB3cm90ZToNCg0KPkhpIE1heGltZQ0KPg0KPk9uIDcgSmFuIDIwMTQs
IGF0IDE2OjU2LCBNYXhpbWUgRKimbqiocyA8bWFpbEBtYXhpbWVkZW5lcy5mcj4gd3JvdGU6DQo+
DQo+PiBTdGlsbCwgSSBkb24ndCB1bmRlcnN0YW5kIHdoeSByZXBsYWNpbmcgdGhlIHBhdHRlcm4g
bWF0Y2hpbmcgaW4gbXkNCj4+IGV4YW1wbGUgYnkgYSBjYWxsIHRvIHN1YnN0IG1ha2VzIHRoZSB0
ZXJtaW5hdGlvbiBjaGVjayBmYWlsLg0KPg0KPkEgY2FsbCB0byBzdWJzdCBkZXN0cm95cyB0aGUg
InByb3BlciBzdWJ0ZXJtIiBzdGF0dXMsIHdoZXJlYXMNCj5wYXR0ZXJuIG1hdGNoaW5nIG5haXZl
bHkgcHJlc2VydmVzIGl0Lg0KPg0KPj4gDQo+PiBNYXhpbWUuDQo+DQo+Pj4gey0jIE9QVElPTlMg
LS13aXRob3V0LUsgIy19DQo+Pj4gDQo+Pj4gbW9kdWxlIEJhZFdpdGhvdXRLIHdoZXJlDQo+Pj4g
DQo+Pj4gZGF0YSBaZXJvIDogU2V0IHdoZXJlDQo+Pj4gDQo+Pj4gZGF0YSBXT25lIDogU2V0IHdo
ZXJlDQo+Pj4gIHdyYXAgOiAoWmVybyAtPiBXT25lKSAtPiBXT25lDQo+Pj4gDQo+Pj4gZGF0YSBf
PC0+XyAoWCA6IFNldCkgOiBTZXQgLT4gU2V0IHdoZXJlDQo+Pj4gIFJlZmwgOiBYIDwtPiBYDQo+
Pj4gDQo+Pj4gcG9zdHVsYXRlDQo+Pj4gIG15SXNvIDogV09uZSA8LT4gKFplcm8gLT4gV09uZSkN
Cj4+PiANCj4+PiBtb28gOiBXT25lIC0+IFplcm8NCj4+PiBub28gOiAoWCA6IFNldCkgLT4gKFdP
bmUgPC0+IFgpIC0+IFggLT4gWmVybw0KPj4+IA0KPj4+IG1vbyAod3JhcCBmKSA9IG5vbyAoWmVy
byAtPiBXT25lKSBteUlzbyBmDQo+Pj4gbm9vIC5XT25lIFJlZmwgeCA9IG1vbyB4DQo+DQo+bW9v
J3MgaW5wdXQgaXMgYmlnZ2VyIHRoYW4gdGhlIHRoaXJkIGFyZ3VtZW50IGluIGl0cyBub28gY2Fs
bA0KPm5vbydzIHRoaXJkIGlucHV0IGlzIHRoZSBzYW1lIGFzIHRoZSBhcmd1bWVudCBpbiBpdHMg
bW9vIGNhbGwNCj4NCj5TaXplLWNoYW5nZSB0ZXJtaW5hdGlvbiwgaG93IGFyZSB5ZT8NCj4NCj5X
aGVuIHlvdSBkbyB0aGUgdHJhbnNsYXRpb24gdG8gZWxpbWluYXRvcnMsIHlvdSdyZSBvYmxpZ2Vk
IHRvDQo+c2hvdyBob3cgcmVjdXJzaXZlIGNhbGxzIGNvcnJlc3BvbmQgdG8gaW52b2NhdGlvbnMg
b2YgdGhlDQo+aW5kdWN0aXZlIGh5cG90aGVzaXM6IGhlcmUgdGhhdCdzIGp1c3Qgbm90IGdvaW5n
IHRvIGhhcHBlbi4NCj5UcmFuc3BvcnRpbmcgZiBhY3Jvc3MgbXlJc28gZG9lcyBpbmRlZWQgZ2l2
ZSBhbiBlbGVtZW50IG9mDQo+V09uZSAoeW91ciBCb3gpLCBidXQgdGhhdCBkb2VzIG5vdCBtYWtl
IGEgbnVsbGFyeSBpbmR1Y3RpdmUNCj5oeXBvdGhlc2lzIGFueSBlYXNpZXIgdG8gaW52b2tlLg0K
Pg0KPkknZCBxdWl0ZSBsaWtlIHRvIHNlZSB1cyBkZWZpbmluZyBhIHR5cGUgdGhlb3J5IGluIHdo
aWNoIHRoZQ0KPm9ubHkgY2hlY2tpbmcgaXMgdHlwZSBjaGVja2luZywgdGhlbiB1c2luZyBpdCBh
cyBhIHRhcmdldCBmb3INCj5lbGFib3JhdGlvbi4gRWxpbWluYXRvcnMgYXJlIG9uZSBjYW5kaWRh
dGUsIGJ1dCB0aGVyZSBhcmUNCj5vdGhlcnMuIFNpemVkIHR5cGVzIGFyZSBjZXJ0YWlubHkgYW5v
dGhlciBzdHJvbmcgY2FuZGlkYXRlLg0KPkknbSBhbHNvIGludGVyZXN0ZWQgdG8gc2VlIHdoZXRo
ZXIgdGhlcmUgYXJlICJsb2NhbGx5IGNsb2NrZWQiDQo+ZXhwbGFuYXRpb25zIGZvciB0ZXJtaW5h
dGlvbiwgYXMgdGhlcmUgc2VlbSB0byBiZSBmb3INCj5wcm9kdWN0aXZpdHkuDQo+DQo+SW50ZXJl
c3RpbmcgdGltZXMNCj4NCj5Db25vcg0KPg0KPg0KPj4+IA0KPj4+IGJhZCA6IFplcm8NCj4+PiBi
YWQgPSBtb28gKHdyYXAgXCAoKSkNCj4+PiANCj4+PiANCj4+PiANCj4+Pj4gVC4NCj4+Pj4gDQo+
Pj4+PiBJIGFtIGFsc28gbm90IHN1cmUgaG93IHNwZWNpZmljIHRoZSBwcm9ibGVtIGlzIHRvIHVu
aXZhbGVuY2UuIEFzIENvZHkNCj4+Pj4+IHNhaWQsIEkgd291bGQgZXhwZWN0IHRvIGZpbmQgc29t
ZSBzZXQtdGhlb3JldGljYWwgbW9kZWxzIHdoZXJlIHRoZQ0KPj4+Pj4gZXF1YWxpdHkgaG9sZHMu
IFNvIGJlaW5nIGFibGUgdG8gcHJvdmUgdGhlIG5lZ2F0aW9uIGlzIGRpc3R1cmJpbmcuDQo+Pj4+
PiANCj4+Pj4+IE1heGltZS4NCj4+Pj4+IA0KPj4+Pj4gT24gMDEvMDYvMjAxNCAwNzoyMyBQTSwg
QWJoaXNoZWsgQW5hbmQgd3JvdGU6DQo+Pj4+Pj4gSXQgaXMga25vd24gdGhhdCBVSVAgaXMgaW5j
b25zaXN0ZW50IHdpdGggdW5pdmFsZW5jZS4NCj4+Pj4+PiBEb2VzIHRoaXMgdHlwZWNoZWNrIGV2
ZW4gYWZ0ZXIgZGlzYWJsaW5nIFVJUCg9PUsgYXhpb20/KSA/DQo+Pj4+Pj4gSSBtaWdodCBiZSB3
cm9uZywgYnV0IEkgdGhpbmsgdGhhdCBVSVAgaXMgYmFrZWQgaW50byB0aGUgdHlwZWNoZWNrZXIN
Cj4+Pj4+PiBvZiBBZ2RhLg0KPj4+Pj4+IEJ1dCwgVUlQIGNhbiBiZSBkaXNhYmxlZCBzb21laG93
Pw0KPj4+Pj4+IA0KPj4+Pj4+IA0KPj4+Pj4+IC0tIEFiaGlzaGVrDQo+Pj4+Pj4gaHR0cDovL3d3
dy5jcy5jb3JuZWxsLmVkdS9+YWE3NTUvDQo+Pj4+Pj48aHR0cDovL3d3dy5jcy5jb3JuZWxsLmVk
dS8lN0VhYTc1NS8+DQo+Pj4+Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4gT24gTW9uLCBKYW4gNiwgMjAx
NCBhdCAzOjQyIFBNLCBNYXhpbWUgRKimbqiocyA8bWFpbEBtYXhpbWVkZW5lcy5mcg0KPj4+Pj4+
IDxtYWlsdG86bWFpbEBtYXhpbWVkZW5lcy5mcj4+IHdyb3RlOg0KPj4+Pj4+IA0KPj4+Pj4+ICAg
QmluZ28sIEFnZGEgc2VlbXMgdG8gaGF2ZSB0aGUgc2FtZSBwcm9ibGVtOg0KPj4+Pj4+IA0KPj4+
Pj4+ICAgbW9kdWxlIFRlcm1pbmF0aW9uIHdoZXJlDQo+Pj4+Pj4gDQo+Pj4+Pj4gICBvcGVuIGlt
cG9ydCBSZWxhdGlvbi5CaW5hcnkuQ29yZQ0KPj4+Pj4+IA0KPj4+Pj4+ICAgZGF0YSBFbXB0eSA6
IFNldCB3aGVyZQ0KPj4+Pj4+IA0KPj4+Pj4+ICAgZGF0YSBCb3ggOiBTZXQgd2hlcmUNCj4+Pj4+
PiAgIHdyYXAgOiAoRW1wdHkgofogQm94KSCh+iBCb3gNCj4+Pj4+PiANCj4+Pj4+PiAgIHBvc3R1
bGF0ZQ0KPj4+Pj4+ICAgaXNvIDogKEVtcHR5IKH6IEJveCkgodQgQm94DQo+Pj4+Pj4gDQo+Pj4+
Pj4gICBsb29wIDogQm94IC0+IEVtcHR5DQo+Pj4+Pj4gICBsb29wICh3cmFwIHgpIHJld3JpdGUg
aXNvID0gbG9vcCB4DQo+Pj4+Pj4gDQo+Pj4+Pj4gICBnaWZ0IDogRW1wdHkgofogQm94DQo+Pj4+
Pj4gICBnaWZ0ICgpDQo+Pj4+Pj4gDQo+Pj4+Pj4gICBidWcgOiBFbXB0eQ0KPj4+Pj4+ICAgYnVn
ID0gbG9vcCAod3JhcCBnaWZ0KQ0KPj4+Pj4+IA0KPj4+Pj4+ICAgSG93ZXZlciwgSSBtYXkgYmUg
bWlzc2luZyBzb21ldGhpbmcgZHVlIHRvIG15IGlnbm9yYW5jZSBvZiBBZ2RhLg0KPj4+Pj4+ICAg
SXQgbWF5IGJlIHdlbGwga25vd24gdGhhdCB0aGUgYXhpb20gSSBpbnRyb2R1Y2VkIGlzIGluY29u
c2lzdGVudC4NCj4+Pj4+PiAgIEZvcmdpdmUgbWUgaWYgaXQgaXMgdGhlIGNhc2UuDQo+Pj4+Pj4g
DQo+Pj4+Pj4gICBNYXhpbWUuDQo+Pj4+Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4gICBPbiAwMS8wNi8y
MDE0IDAxOjE1IFBNLCBNYXhpbWUgRKimbqiocyB3cm90ZToNCj4+Pj4+PiANCj4+Pj4+PiAgICAg
ICBUaGUgYW50aS1leHRlbnNpb25hbGl0eSBidWcgaXMgaW5kZWVkIHJlbGF0ZWQgdG8gdGVybWlu
YXRpb24uDQo+Pj4+Pj4gICAgICAgTW9yZSBwcmVjaXNlbHksIGl0IGlzIHRoZSBzdWJ0ZXJtIHJl
bGF0aW9uIHVzZWQgYnkgdGhlIGd1YXJkDQo+Pj4+Pj4gICAgICAgY2hlY2tlciB3aGljaCBpcyBu
b3QgZGVmaW5lZCBxdWl0ZSB0aGUgcmlnaHQgd2F5IG9uIGRlcGVuZGVudA0KPj4+Pj4+ICAgICAg
IHBhdHRlcm4gbWF0Y2hpbmcuDQo+Pj4+Pj4gDQo+Pj4+Pj4gICAgICAgSXQgaXMgbm90IHRvbyBo
YXJkIHRvIGZpeCAod2UgaGF2ZSBhIHBhdGNoKSwgYnV0IGRvaW5nIHNvDQo+Pj4+Pj4gICAgICAg
d2l0aG91dCBydWxpbmcgb3V0IGFueSBpbnRlcmVzdGluZyBsZWdpdGltYXRlIGV4YW1wbGUgKGRl
YWxpbmcNCj4+Pj4+PiAgICAgICB3aXRoIHJlY3Vyc2lvbiBvbiBkZXBlbmRlbnRseSB0eXBlZCBk
YXRhIHN0cnVjdHVyZXMpIGlzIG1vcmUNCj4+Pj4+PiAgICAgICBjaGFsbGVuZ2luZy4NCj4+Pj4+
PiANCj4+Pj4+PiAgICAgICBJIGFtIGFsc28gY3VyaW91cyBhcyB0byB3aGV0aGVyIEFnZGEgaXMg
aW1wYWN0ZWQuIExldCdzIHRyeSBpdA0KPj4+Pj4+IDopDQo+Pj4+Pj4gDQo+Pj4+Pj4gICAgICAg
TWF4aW1lLg0KPj4+Pj4+IA0KPj4+Pj4+ICAgICAgIE9uIDAxLzA2LzIwMTQgMTI6NTkgUE0sIEFs
dGVua2lyY2ggVGhvcnN0ZW4gd3JvdGU6DQo+Pj4+Pj4gDQo+Pj4+Pj4gICAgICAgICAgIFdoaWNo
IGJ1ZyB3YXMgdGhpcz8NCj4+Pj4+PiANCj4+Pj4+PiAgICAgICAgICAgSSBvbmx5IHNhdyB0aGUg
b25lIHdoaWNoIGFsbG93ZWQgeW91IHRvIHByb3ZlDQo+Pj4+Pj4gICAgICAgICAgIGFudGktZXh0
ZW5zaW9uYWxpdHk/IEJ1dA0KPj4+Pj4+ICAgICAgICAgICB0aGlzIHdhc24ndCByZWxhdGVkIHRv
IHRlcm1pbmF0aW9uLCBvcj8NCj4+Pj4+PiANCj4+Pj4+PiAgICAgICAgICAgVGhvcnN0ZW4NCj4+
Pj4+PiANCj4+Pj4+PiAgICAgICAgICAgT24gMDYvMDEvMjAxNCAxNjo1NCwgIkNvZHkgUm91eCIg
PGNvZHkucm91eEBhbmRyZXcuY211LmVkdQ0KPj4+Pj4+ICAgICAgICAgICA8bWFpbHRvOmNvZHku
cm91eEBhbmRyZXcuY211LmVkdT4+IHdyb3RlOg0KPj4+Pj4+IA0KPj4+Pj4+ICAgICAgICAgICAg
ICAgTmljZSBzdW1tYXJ5IQ0KPj4+Pj4+IA0KPj4+Pj4+IA0KPj4+Pj4+ICAgICAgICAgICAgICAg
T24gMDEvMDYvMjAxNCAwODo0OSBBTSwgQWx0ZW5raXJjaCBUaG9yc3RlbiB3cm90ZToNCj4+Pj4+
PiANCj4+Pj4+PiAgICAgICAgICAgICAgICAgICBBZ2RhIGVuZm9yY2VzIHRlcm1pbmF0aW9uIHZp
YSBhIHRlcm1pbmF0aW9uDQo+Pj4+Pj4gICAgICAgICAgICAgICAgICAgY2hlY2tlciB3aGljaCBp
cyBtb3JlDQo+Pj4+Pj4gICAgICAgICAgICAgICAgICAgZmxleGlibGUgYnV0IEkgdGhpbmsgbGVz
cyBwcmluY2lwbGVkIHRoYW4gQ29xJ3MNCj4+Pj4+PiAgICAgICAgICAgICAgICAgICBhcHByb2Fj
aC4NCj4+Pj4+PiANCj4+Pj4+PiAgICAgICAgICAgICAgIFRoYXQncyBhIGJpdCBzY2FyeSBnaXZl
biB0aGF0IHRoZXJlIHdhcyBhbg0KPj4+Pj4+ICAgICAgICAgICAgICAgaW5jb25zaXN0ZW5jeSBm
b3VuZCBpbg0KPj4+Pj4+ICAgICAgICAgICAgICAgdGhlIENvcSB0ZXJtaW5hdGlvbiBjaGVja2Vy
IGp1c3QgYSBjb3VwbGUgb2Ygd2Vla3MgYWdvDQo+Pj4+Pj4gOikNCj4+Pj4+PiANCj4+Pj4+PiAg
ICAgICAgICAgICAgIEJUVywgaGFzIGFueW9uZSB0cmllZCByZXByb2R1Y2luZyB0aGUgYnVnIGlu
IEFnZGE/DQo+Pj4+Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4gICAgICAgICAgICAgICBDb2R5DQo+Pj4+
Pj4gDQo+Pj4+Pj4gICAgICAgICAgIFRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJl
IGludGVuZGVkIHNvbGVseSBmb3INCj4+Pj4+PiAgICAgICAgICAgdGhlIGFkZHJlc3NlZSBhbmQg
bWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9ybWF0aW9uLiBJZg0KPj4+Pj4+ICAgICAgICAg
ICB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzIG1lc3NhZ2UgaW4gZXJyb3IsIHBsZWFzZSBzZW5kIGl0
DQo+Pj4+Pj4gICAgICAgICAgIGJhY2sgdG8gbWUsIGFuZCBpbW1lZGlhdGVseSBkZWxldGUgaXQu
IFBsZWFzZSBkbyBub3QgdXNlLA0KPj4+Pj4+ICAgICAgICAgICBjb3B5IG9yIGRpc2Nsb3NlIHRo
ZSBpbmZvcm1hdGlvbiBjb250YWluZWQgaW4gdGhpcyBtZXNzYWdlDQo+Pj4+Pj4gICAgICAgICAg
IG9yIGluIGFueSBhdHRhY2htZW50LiBBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5
DQo+Pj4+Pj4gICAgICAgICAgIHRoZSBhdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QgbmVjZXNz
YXJpbHkgcmVmbGVjdCB0aGUNCj4+Pj4+PiAgICAgICAgICAgdmlld3Mgb2YgdGhlIFVuaXZlcnNp
dHkgb2YgTm90dGluZ2hhbS4NCj4+Pj4+PiANCj4+Pj4+PiAgICAgICAgICAgVGhpcyBtZXNzYWdl
IGhhcyBiZWVuIGNoZWNrZWQgZm9yIHZpcnVzZXMgYnV0IHRoZSBjb250ZW50cw0KPj4+Pj4+ICAg
ICAgICAgICBvZiBhbiBhdHRhY2htZW50DQo+Pj4+Pj4gICAgICAgICAgIG1heSBzdGlsbCBjb250
YWluIHNvZnR3YXJlIHZpcnVzZXMgd2hpY2ggY291bGQgZGFtYWdlIHlvdXINCj4+Pj4+PiAgICAg
ICAgICAgY29tcHV0ZXIgc3lzdGVtLCB5b3UgYXJlIGFkdmlzZWQgdG8gcGVyZm9ybSB5b3VyIG93
bg0KPj4+Pj4+ICAgICAgICAgICBjaGVja3MuIEVtYWlsIGNvbW11bmljYXRpb25zIHdpdGggdGhl
IFVuaXZlcnNpdHkgb2YNCj4+Pj4+PiAgICAgICAgICAgTm90dGluZ2hhbSBtYXkgYmUgbW9uaXRv
cmVkIGFzIHBlcm1pdHRlZCBieSBVSw0KPj4+Pj4+bGVnaXNsYXRpb24uDQo+Pj4+Pj4gDQo+Pj4+
Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4gICAgICAgX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18NCj4+Pj4+PiAgICAgICBBZ2RhIG1h
aWxpbmcgbGlzdA0KPj4+Pj4+ICAgICAgIEFnZGFAbGlzdHMuY2hhbG1lcnMuc2UgPG1haWx0bzpB
Z2RhQGxpc3RzLmNoYWxtZXJzLnNlPg0KPj4+Pj4+ICAgICAgIGh0dHBzOi8vbGlzdHMuY2hhbG1l
cnMuc2UvbWFpbG1hbi9saXN0aW5mby9hZ2RhDQo+Pj4+Pj4gDQo+Pj4+Pj4gDQo+Pj4+Pj4gICBf
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fXw0KPj4+Pj4+ICAg
QWdkYSBtYWlsaW5nIGxpc3QNCj4+Pj4+PiAgIEFnZGFAbGlzdHMuY2hhbG1lcnMuc2UgPG1haWx0
bzpBZ2RhQGxpc3RzLmNoYWxtZXJzLnNlPg0KPj4+Pj4+ICAgaHR0cHM6Ly9saXN0cy5jaGFsbWVy
cy5zZS9tYWlsbWFuL2xpc3RpbmZvL2FnZGENCj4+Pj4+PiANCj4+Pj4+PiANCj4+Pj4+IF9fX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fDQo+Pj4+PiBBZ2RhIG1h
aWxpbmcgbGlzdA0KPj4+Pj4gQWdkYUBsaXN0cy5jaGFsbWVycy5zZQ0KPj4+Pj4gaHR0cHM6Ly9s
aXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xpc3RpbmZvL2FnZGENCj4+Pj4gX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18NCj4+Pj4gQWdkYSBtYWlsaW5nIGxp
c3QNCj4+Pj4gQWdkYUBsaXN0cy5jaGFsbWVycy5zZQ0KPj4+PiBodHRwczovL2xpc3RzLmNoYWxt
ZXJzLnNlL21haWxtYW4vbGlzdGluZm8vYWdkYQ0KPj4gDQo+DQoNCg0K