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

[Altenkirch Thorsten]

DQoNCk9uIDA3LzAxLzIwMTQgMDA6NTAsICJNYXhpbWUgRKimbqiocyIgPG1haWxAbWF4aW1lZGVu
ZXMuZnI+IHdyb3RlOg0KDQo+V2VsbCwgbXkgZXhhbXBsZSBkb2VzIG5vdCB0eXBlY2hlY2sgd2l0
aCB0aGUgLS13aXRob3V0LUsgZmxhZy4NCj4NCj5Ib3dldmVyLCB0aGUgc2FtZSB0aGluZyBjYW4g
YmUgcHJvdmVuIGluIENvcSB3aXRob3V0IEssIHNvIEkgYW0gbm90IHN1cmUNCj5pZiBpdCBpcyBi
ZWNhdXNlIHRoZSBmbGFnIGlzIHRvbyByZXN0cmljdGl2ZSBvciBiZWNhdXNlIEFnZGEncyBwYXR0
ZXJuDQo+bWF0Y2hpbmcgaXMgZGlmZmVyZW50Lg0KDQpWZXJ5IGdvb2QuIEFnZGEgaXMgcmlnaHQg
YW5kIENvcSBnb3QgaXQgd3JvbmcuIEFzIEkgc2FpZCBwcmV2aW9zdWx5IHRoZQ0KZGVmaW5pdGlv
biBvZiBsb29wIGltcGxpY2l0ZWx5IHVzZXMgSy4NCg0KVC4NCg0KPg0KPkkgYW0gYWxzbyBub3Qg
c3VyZSBob3cgc3BlY2lmaWMgdGhlIHByb2JsZW0gaXMgdG8gdW5pdmFsZW5jZS4gQXMgQ29keQ0K
PnNhaWQsIEkgd291bGQgZXhwZWN0IHRvIGZpbmQgc29tZSBzZXQtdGhlb3JldGljYWwgbW9kZWxz
IHdoZXJlIHRoZQ0KPmVxdWFsaXR5IGhvbGRzLiBTbyBiZWluZyBhYmxlIHRvIHByb3ZlIHRoZSBu
ZWdhdGlvbiBpcyBkaXN0dXJiaW5nLg0KPg0KPk1heGltZS4NCj4NCj5PbiAwMS8wNi8yMDE0IDA3
OjIzIFBNLCBBYmhpc2hlayBBbmFuZCB3cm90ZToNCj4+IEl0IGlzIGtub3duIHRoYXQgVUlQIGlz
IGluY29uc2lzdGVudCB3aXRoIHVuaXZhbGVuY2UuDQo+PiBEb2VzIHRoaXMgdHlwZWNoZWNrIGV2
ZW4gYWZ0ZXIgZGlzYWJsaW5nIFVJUCg9PUsgYXhpb20/KSA/DQo+PiBJIG1pZ2h0IGJlIHdyb25n
LCBidXQgSSB0aGluayB0aGF0IFVJUCBpcyBiYWtlZCBpbnRvIHRoZSB0eXBlY2hlY2tlcg0KPj4g
b2YgQWdkYS4NCj4+IEJ1dCwgVUlQIGNhbiBiZSBkaXNhYmxlZCBzb21laG93Pw0KPj4NCj4+DQo+
PiAtLSBBYmhpc2hlaw0KPj4gaHR0cDovL3d3dy5jcy5jb3JuZWxsLmVkdS9+YWE3NTUvIDxodHRw
Oi8vd3d3LmNzLmNvcm5lbGwuZWR1LyU3RWFhNzU1Lz4NCj4+DQo+Pg0KPj4gT24gTW9uLCBKYW4g
NiwgMjAxNCBhdCAzOjQyIFBNLCBNYXhpbWUgRKimbqiocyA8bWFpbEBtYXhpbWVkZW5lcy5mcg0K
Pj4gPG1haWx0bzptYWlsQG1heGltZWRlbmVzLmZyPj4gd3JvdGU6DQo+Pg0KPj4gICAgIEJpbmdv
LCBBZ2RhIHNlZW1zIHRvIGhhdmUgdGhlIHNhbWUgcHJvYmxlbToNCj4+DQo+PiAgICAgbW9kdWxl
IFRlcm1pbmF0aW9uIHdoZXJlDQo+Pg0KPj4gICAgIG9wZW4gaW1wb3J0IFJlbGF0aW9uLkJpbmFy
eS5Db3JlDQo+Pg0KPj4gICAgIGRhdGEgRW1wdHkgOiBTZXQgd2hlcmUNCj4+DQo+PiAgICAgZGF0
YSBCb3ggOiBTZXQgd2hlcmUNCj4+ICAgICB3cmFwIDogKEVtcHR5IKH6IEJveCkgofogQm94DQo+
Pg0KPj4gICAgIHBvc3R1bGF0ZQ0KPj4gICAgIGlzbyA6IChFbXB0eSCh+iBCb3gpIKHUIEJveA0K
Pj4NCj4+ICAgICBsb29wIDogQm94IC0+IEVtcHR5DQo+PiAgICAgbG9vcCAod3JhcCB4KSByZXdy
aXRlIGlzbyA9IGxvb3AgeA0KPj4NCj4+ICAgICBnaWZ0IDogRW1wdHkgofogQm94DQo+PiAgICAg
Z2lmdCAoKQ0KPj4NCj4+ICAgICBidWcgOiBFbXB0eQ0KPj4gICAgIGJ1ZyA9IGxvb3AgKHdyYXAg
Z2lmdCkNCj4+DQo+PiAgICAgSG93ZXZlciwgSSBtYXkgYmUgbWlzc2luZyBzb21ldGhpbmcgZHVl
IHRvIG15IGlnbm9yYW5jZSBvZiBBZ2RhLg0KPj4gICAgIEl0IG1heSBiZSB3ZWxsIGtub3duIHRo
YXQgdGhlIGF4aW9tIEkgaW50cm9kdWNlZCBpcyBpbmNvbnNpc3RlbnQuDQo+PiAgICAgRm9yZ2l2
ZSBtZSBpZiBpdCBpcyB0aGUgY2FzZS4NCj4+DQo+PiAgICAgTWF4aW1lLg0KPj4NCj4+DQo+PiAg
ICAgT24gMDEvMDYvMjAxNCAwMToxNSBQTSwgTWF4aW1lIESopm6oqHMgd3JvdGU6DQo+Pg0KPj4g
ICAgICAgICBUaGUgYW50aS1leHRlbnNpb25hbGl0eSBidWcgaXMgaW5kZWVkIHJlbGF0ZWQgdG8g
dGVybWluYXRpb24uDQo+PiAgICAgICAgIE1vcmUgcHJlY2lzZWx5LCBpdCBpcyB0aGUgc3VidGVy
bSByZWxhdGlvbiB1c2VkIGJ5IHRoZSBndWFyZA0KPj4gICAgICAgICBjaGVja2VyIHdoaWNoIGlz
IG5vdCBkZWZpbmVkIHF1aXRlIHRoZSByaWdodCB3YXkgb24gZGVwZW5kZW50DQo+PiAgICAgICAg
IHBhdHRlcm4gbWF0Y2hpbmcuDQo+Pg0KPj4gICAgICAgICBJdCBpcyBub3QgdG9vIGhhcmQgdG8g
Zml4ICh3ZSBoYXZlIGEgcGF0Y2gpLCBidXQgZG9pbmcgc28NCj4+ICAgICAgICAgd2l0aG91dCBy
dWxpbmcgb3V0IGFueSBpbnRlcmVzdGluZyBsZWdpdGltYXRlIGV4YW1wbGUgKGRlYWxpbmcNCj4+
ICAgICAgICAgd2l0aCByZWN1cnNpb24gb24gZGVwZW5kZW50bHkgdHlwZWQgZGF0YSBzdHJ1Y3R1
cmVzKSBpcyBtb3JlDQo+PiAgICAgICAgIGNoYWxsZW5naW5nLg0KPj4NCj4+ICAgICAgICAgSSBh
bSBhbHNvIGN1cmlvdXMgYXMgdG8gd2hldGhlciBBZ2RhIGlzIGltcGFjdGVkLiBMZXQncyB0cnkg
aXQNCj4+OikNCj4+DQo+PiAgICAgICAgIE1heGltZS4NCj4+DQo+PiAgICAgICAgIE9uIDAxLzA2
LzIwMTQgMTI6NTkgUE0sIEFsdGVua2lyY2ggVGhvcnN0ZW4gd3JvdGU6DQo+Pg0KPj4gICAgICAg
ICAgICAgV2hpY2ggYnVnIHdhcyB0aGlzPw0KPj4NCj4+ICAgICAgICAgICAgIEkgb25seSBzYXcg
dGhlIG9uZSB3aGljaCBhbGxvd2VkIHlvdSB0byBwcm92ZQ0KPj4gICAgICAgICAgICAgYW50aS1l
eHRlbnNpb25hbGl0eT8gQnV0DQo+PiAgICAgICAgICAgICB0aGlzIHdhc24ndCByZWxhdGVkIHRv
IHRlcm1pbmF0aW9uLCBvcj8NCj4+DQo+PiAgICAgICAgICAgICBUaG9yc3Rlbg0KPj4NCj4+ICAg
ICAgICAgICAgIE9uIDA2LzAxLzIwMTQgMTY6NTQsICJDb2R5IFJvdXgiIDxjb2R5LnJvdXhAYW5k
cmV3LmNtdS5lZHUNCj4+ICAgICAgICAgICAgIDxtYWlsdG86Y29keS5yb3V4QGFuZHJldy5jbXUu
ZWR1Pj4gd3JvdGU6DQo+Pg0KPj4gICAgICAgICAgICAgICAgIE5pY2Ugc3VtbWFyeSENCj4+DQo+
Pg0KPj4gICAgICAgICAgICAgICAgIE9uIDAxLzA2LzIwMTQgMDg6NDkgQU0sIEFsdGVua2lyY2gg
VGhvcnN0ZW4gd3JvdGU6DQo+Pg0KPj4gICAgICAgICAgICAgICAgICAgICBBZ2RhIGVuZm9yY2Vz
IHRlcm1pbmF0aW9uIHZpYSBhIHRlcm1pbmF0aW9uDQo+PiAgICAgICAgICAgICAgICAgICAgIGNo
ZWNrZXIgd2hpY2ggaXMgbW9yZQ0KPj4gICAgICAgICAgICAgICAgICAgICBmbGV4aWJsZSBidXQg
SSB0aGluayBsZXNzIHByaW5jaXBsZWQgdGhhbiBDb3Encw0KPj4gICAgICAgICAgICAgICAgICAg
ICBhcHByb2FjaC4NCj4+DQo+PiAgICAgICAgICAgICAgICAgVGhhdCdzIGEgYml0IHNjYXJ5IGdp
dmVuIHRoYXQgdGhlcmUgd2FzIGFuDQo+PiAgICAgICAgICAgICAgICAgaW5jb25zaXN0ZW5jeSBm
b3VuZCBpbg0KPj4gICAgICAgICAgICAgICAgIHRoZSBDb3EgdGVybWluYXRpb24gY2hlY2tlciBq
dXN0IGEgY291cGxlIG9mIHdlZWtzIGFnbw0KPj46KQ0KPj4NCj4+ICAgICAgICAgICAgICAgICBC
VFcsIGhhcyBhbnlvbmUgdHJpZWQgcmVwcm9kdWNpbmcgdGhlIGJ1ZyBpbiBBZ2RhPw0KPj4NCj4+
DQo+PiAgICAgICAgICAgICAgICAgQ29keQ0KPj4NCj4+ICAgICAgICAgICAgIFRoaXMgbWVzc2Fn
ZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJlIGludGVuZGVkIHNvbGVseSBmb3INCj4+ICAgICAgICAg
ICAgIHRoZSBhZGRyZXNzZWUgYW5kIG1heSBjb250YWluIGNvbmZpZGVudGlhbCBpbmZvcm1hdGlv
bi4gSWYNCj4+ICAgICAgICAgICAgIHlvdSBoYXZlIHJlY2VpdmVkIHRoaXMgbWVzc2FnZSBpbiBl
cnJvciwgcGxlYXNlIHNlbmQgaXQNCj4+ICAgICAgICAgICAgIGJhY2sgdG8gbWUsIGFuZCBpbW1l
ZGlhdGVseSBkZWxldGUgaXQuIFBsZWFzZSBkbyBub3QgdXNlLA0KPj4gICAgICAgICAgICAgY29w
eSBvciBkaXNjbG9zZSB0aGUgaW5mb3JtYXRpb24gY29udGFpbmVkIGluIHRoaXMgbWVzc2FnZQ0K
Pj4gICAgICAgICAgICAgb3IgaW4gYW55IGF0dGFjaG1lbnQuIEFueSB2aWV3cyBvciBvcGluaW9u
cyBleHByZXNzZWQgYnkNCj4+ICAgICAgICAgICAgIHRoZSBhdXRob3Igb2YgdGhpcyBlbWFpbCBk
byBub3QgbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUNCj4+ICAgICAgICAgICAgIHZpZXdzIG9mIHRo
ZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0uDQo+Pg0KPj4gICAgICAgICAgICAgVGhpcyBtZXNz
YWdlIGhhcyBiZWVuIGNoZWNrZWQgZm9yIHZpcnVzZXMgYnV0IHRoZSBjb250ZW50cw0KPj4gICAg
ICAgICAgICAgb2YgYW4gYXR0YWNobWVudA0KPj4gICAgICAgICAgICAgbWF5IHN0aWxsIGNvbnRh
aW4gc29mdHdhcmUgdmlydXNlcyB3aGljaCBjb3VsZCBkYW1hZ2UgeW91cg0KPj4gICAgICAgICAg
ICAgY29tcHV0ZXIgc3lzdGVtLCB5b3UgYXJlIGFkdmlzZWQgdG8gcGVyZm9ybSB5b3VyIG93bg0K
Pj4gICAgICAgICAgICAgY2hlY2tzLiBFbWFpbCBjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2
ZXJzaXR5IG9mDQo+PiAgICAgICAgICAgICBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQgYXMg
cGVybWl0dGVkIGJ5IFVLIGxlZ2lzbGF0aW9uLg0KPj4NCj4+DQo+Pg0KPj4NCj4+DQo+PiAgICAg
ICAgIF9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fDQo+PiAg
ICAgICAgIEFnZGEgbWFpbGluZyBsaXN0DQo+PiAgICAgICAgIEFnZGFAbGlzdHMuY2hhbG1lcnMu
c2UgPG1haWx0bzpBZ2RhQGxpc3RzLmNoYWxtZXJzLnNlPg0KPj4gICAgICAgICBodHRwczovL2xp
c3RzLmNoYWxtZXJzLnNlL21haWxtYW4vbGlzdGluZm8vYWdkYQ0KPj4NCj4+DQo+PiAgICAgX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18NCj4+ICAgICBBZ2Rh
IG1haWxpbmcgbGlzdA0KPj4gICAgIEFnZGFAbGlzdHMuY2hhbG1lcnMuc2UgPG1haWx0bzpBZ2Rh
QGxpc3RzLmNoYWxtZXJzLnNlPg0KPj4gICAgIGh0dHBzOi8vbGlzdHMuY2hhbG1lcnMuc2UvbWFp
bG1hbi9saXN0aW5mby9hZ2RhDQo+Pg0KPj4NCj4NCj5fX19fX19fX19fX19fX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fXw0KPkFnZGEgbWFpbGluZyBsaXN0DQo+QWdkYUBsaXN0cy5j
aGFsbWVycy5zZQ0KPmh0dHBzOi8vbGlzdHMuY2hhbG1lcnMuc2UvbWFpbG1hbi9saXN0aW5mby9h
Z2RhDQoNCg==