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

[Altenkirch Thorsten]

SGkgTWF4aW1lLA0KDQp5b3VyIHBvc3R1bGF0ZSBzZWVtcyBjb3JyZWN0IHNpbmNlIGNlcnRhaW5s
eSBFbXB0eSCh+iBCb3ggYW5kIEJveCBhcmUNCmlzb21vcnBoaWMgYW5kIGhlbmNlIGVxdWFsIGFz
IGEgY29uc2VxdWVuY2Ugb2YgdW5pdmFsZW5jZS4NCg0KSG93ZXZlciwgSSB0aGluayB0aGUgZGVm
aW5pdGlvbiBvZiBsb29wIGxvb2tzIHN1c3BpY2lvdXMgaW4gdGhlIHByZXNlbmNlDQpvZiBwcm9v
Zi1yZWxldmFudCBlcXVhbGl0eTogaWYgd2UgcmVwbGFjZSByZXdyaXRlIGJ5IGFuIGV4cGxpY2l0
IHVzZSBvZg0Kc3Vic3QsIGxvb3AgaXNuJ3Qgc3RydWN0dXJhbCByZWN1cnNpdmUgYW55bW9yZS4g
SGVuY2UgbXkgZGlhZ25vc2lzIHdvdWxkDQpiZSB0aGF0IHJld3JpdGUgaXMgc2ltcGx5IGluY29t
cGF0aWJsZSB3aXRoIHVuaXZhbGVuY2UuDQoNCkNoZWVycywNClRob3JzdGVuDQoNCk9uIDA2LzAx
LzIwMTQgMjA6NDIsICJNYXhpbWUgRKimbqiocyIgPG1haWxAbWF4aW1lZGVuZXMuZnI+IHdyb3Rl
Og0KDQo+QmluZ28sIEFnZGEgc2VlbXMgdG8gaGF2ZSB0aGUgc2FtZSBwcm9ibGVtOg0KPg0KPm1v
ZHVsZSBUZXJtaW5hdGlvbiB3aGVyZQ0KPg0KPm9wZW4gaW1wb3J0IFJlbGF0aW9uLkJpbmFyeS5D
b3JlDQo+DQo+ZGF0YSBFbXB0eSA6IFNldCB3aGVyZQ0KPg0KPmRhdGEgQm94IDogU2V0IHdoZXJl
DQo+d3JhcCA6IChFbXB0eSCh+iBCb3gpIKH6IEJveA0KPg0KPnBvc3R1bGF0ZQ0KPmlzbyA6IChF
bXB0eSCh+iBCb3gpIKHUIEJveA0KPg0KPmxvb3AgOiBCb3ggLT4gRW1wdHkNCj5sb29wICh3cmFw
IHgpIHJld3JpdGUgaXNvID0gbG9vcCB4DQo+DQo+Z2lmdCA6IEVtcHR5IKH6IEJveA0KPmdpZnQg
KCkNCj4NCj5idWcgOiBFbXB0eQ0KPmJ1ZyA9IGxvb3AgKHdyYXAgZ2lmdCkNCj4NCj5Ib3dldmVy
LCBJIG1heSBiZSBtaXNzaW5nIHNvbWV0aGluZyBkdWUgdG8gbXkgaWdub3JhbmNlIG9mIEFnZGEu
IEl0IG1heQ0KPmJlIHdlbGwga25vd24gdGhhdCB0aGUgYXhpb20gSSBpbnRyb2R1Y2VkIGlzIGlu
Y29uc2lzdGVudC4gRm9yZ2l2ZSBtZSBpZg0KPml0IGlzIHRoZSBjYXNlLg0KPg0KPk1heGltZS4N
Cj4NCj5PbiAwMS8wNi8yMDE0IDAxOjE1IFBNLCBNYXhpbWUgRKimbqiocyB3cm90ZToNCj4+IFRo
ZSBhbnRpLWV4dGVuc2lvbmFsaXR5IGJ1ZyBpcyBpbmRlZWQgcmVsYXRlZCB0byB0ZXJtaW5hdGlv
bi4gTW9yZQ0KPj4gcHJlY2lzZWx5LCBpdCBpcyB0aGUgc3VidGVybSByZWxhdGlvbiB1c2VkIGJ5
IHRoZSBndWFyZCBjaGVja2VyIHdoaWNoDQo+PiBpcyBub3QgZGVmaW5lZCBxdWl0ZSB0aGUgcmln
aHQgd2F5IG9uIGRlcGVuZGVudCBwYXR0ZXJuIG1hdGNoaW5nLg0KPj4NCj4+IEl0IGlzIG5vdCB0
b28gaGFyZCB0byBmaXggKHdlIGhhdmUgYSBwYXRjaCksIGJ1dCBkb2luZyBzbyB3aXRob3V0DQo+
PiBydWxpbmcgb3V0IGFueSBpbnRlcmVzdGluZyBsZWdpdGltYXRlIGV4YW1wbGUgKGRlYWxpbmcg
d2l0aCByZWN1cnNpb24NCj4+IG9uIGRlcGVuZGVudGx5IHR5cGVkIGRhdGEgc3RydWN0dXJlcykg
aXMgbW9yZSBjaGFsbGVuZ2luZy4NCj4+DQo+PiBJIGFtIGFsc28gY3VyaW91cyBhcyB0byB3aGV0
aGVyIEFnZGEgaXMgaW1wYWN0ZWQuIExldCdzIHRyeSBpdCA6KQ0KPj4NCj4+IE1heGltZS4NCj4+
DQo+PiBPbiAwMS8wNi8yMDE0IDEyOjU5IFBNLCBBbHRlbmtpcmNoIFRob3JzdGVuIHdyb3RlOg0K
Pj4+IFdoaWNoIGJ1ZyB3YXMgdGhpcz8NCj4+Pg0KPj4+IEkgb25seSBzYXcgdGhlIG9uZSB3aGlj
aCBhbGxvd2VkIHlvdSB0byBwcm92ZSBhbnRpLWV4dGVuc2lvbmFsaXR5PyBCdXQNCj4+PiB0aGlz
IHdhc24ndCByZWxhdGVkIHRvIHRlcm1pbmF0aW9uLCBvcj8NCj4+Pg0KPj4+IFRob3JzdGVuDQo+
Pj4NCj4+PiBPbiAwNi8wMS8yMDE0IDE2OjU0LCAiQ29keSBSb3V4IiA8Y29keS5yb3V4QGFuZHJl
dy5jbXUuZWR1PiB3cm90ZToNCj4+Pg0KPj4+PiBOaWNlIHN1bW1hcnkhDQo+Pj4+DQo+Pj4+DQo+
Pj4+IE9uIDAxLzA2LzIwMTQgMDg6NDkgQU0sIEFsdGVua2lyY2ggVGhvcnN0ZW4gd3JvdGU6DQo+
Pj4+PiBBZ2RhIGVuZm9yY2VzIHRlcm1pbmF0aW9uIHZpYSBhIHRlcm1pbmF0aW9uIGNoZWNrZXIg
d2hpY2ggaXMgbW9yZQ0KPj4+Pj4gZmxleGlibGUgYnV0IEkgdGhpbmsgbGVzcyBwcmluY2lwbGVk
IHRoYW4gQ29xJ3MgYXBwcm9hY2guDQo+Pj4+IFRoYXQncyBhIGJpdCBzY2FyeSBnaXZlbiB0aGF0
IHRoZXJlIHdhcyBhbiBpbmNvbnNpc3RlbmN5IGZvdW5kIGluDQo+Pj4+IHRoZSBDb3EgdGVybWlu
YXRpb24gY2hlY2tlciBqdXN0IGEgY291cGxlIG9mIHdlZWtzIGFnbyA6KQ0KPj4+Pg0KPj4+PiBC
VFcsIGhhcyBhbnlvbmUgdHJpZWQgcmVwcm9kdWNpbmcgdGhlIGJ1ZyBpbiBBZ2RhPw0KPj4+Pg0K
Pj4+Pg0KPj4+PiBDb2R5DQo+Pj4gVGhpcyBtZXNzYWdlIGFuZCBhbnkgYXR0YWNobWVudCBhcmUg
aW50ZW5kZWQgc29sZWx5IGZvciB0aGUgYWRkcmVzc2VlDQo+Pj4gYW5kIG1heSBjb250YWluIGNv
bmZpZGVudGlhbCBpbmZvcm1hdGlvbi4gSWYgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcw0KPj4+IG1l
c3NhZ2UgaW4gZXJyb3IsIHBsZWFzZSBzZW5kIGl0IGJhY2sgdG8gbWUsIGFuZCBpbW1lZGlhdGVs
eSBkZWxldGUNCj4+PiBpdC4gUGxlYXNlIGRvIG5vdCB1c2UsIGNvcHkgb3IgZGlzY2xvc2UgdGhl
IGluZm9ybWF0aW9uIGNvbnRhaW5lZCBpbg0KPj4+IHRoaXMgbWVzc2FnZSBvciBpbiBhbnkgYXR0
YWNobWVudC4gQW55IHZpZXdzIG9yIG9waW5pb25zIGV4cHJlc3NlZCBieQ0KPj4+IHRoZSBhdXRo
b3Igb2YgdGhpcyBlbWFpbCBkbyBub3QgbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUgdmlld3Mgb2Yg
dGhlDQo+Pj4gVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtLg0KPj4+DQo+Pj4gVGhpcyBtZXNzYWdl
IGhhcyBiZWVuIGNoZWNrZWQgZm9yIHZpcnVzZXMgYnV0IHRoZSBjb250ZW50cyBvZiBhbg0KPj4+
IGF0dGFjaG1lbnQNCj4+PiBtYXkgc3RpbGwgY29udGFpbiBzb2Z0d2FyZSB2aXJ1c2VzIHdoaWNo
IGNvdWxkIGRhbWFnZSB5b3VyIGNvbXB1dGVyDQo+Pj4gc3lzdGVtLCB5b3UgYXJlIGFkdmlzZWQg
dG8gcGVyZm9ybSB5b3VyIG93biBjaGVja3MuIEVtYWlsDQo+Pj4gY29tbXVuaWNhdGlvbnMgd2l0
aCB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQgYXMNCj4+PiBw
ZXJtaXR0ZWQgYnkgVUsgbGVnaXNsYXRpb24uDQo+Pj4NCj4+Pg0KPj4+DQo+Pj4NCj4+DQo+PiBf
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fXw0KPj4gQWdkYSBt
YWlsaW5nIGxpc3QNCj4+IEFnZGFAbGlzdHMuY2hhbG1lcnMuc2UNCj4+IGh0dHBzOi8vbGlzdHMu
Y2hhbG1lcnMuc2UvbWFpbG1hbi9saXN0aW5mby9hZ2RhDQo+DQoNCg==