Re: [TYPES] Equivalence invariance for MLTT (reference request)
Jon Sterling <[email protected]> Tue, 13 Jun 2023 15:50:07 +0200
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
WyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVwZW5uLmVkdS9tYWlsbWFuL2xp c3RpbmZvL3R5cGVzLWxpc3QgXQoKRGVhciBBbmRyZWosCgpJIGFtIG5vdCBjb21wbGV0ZWx5IHN1 cmUgYmVjYXVzZSBpdCBpcyBhIHdoaWxlIHNpbmNlIEkgaGFkIHdhdGNoZWQgdGhpcywgYnV0IEkg dGhpbmsgdGhpcyBtaWdodCBiZSByZWxhdGVkIHRvIHRoZSB0b3BpYyBvZiBQZXIgTWFydGluLUzD tmYncyAyMDEzIEVhcm5lc3QgTmFnZWwgTGVjdHVyZSDigJxJbnZhcmlhbmNlIFVuZGVyIElzb21v cnBoaXNtIGFuZCBEZWZpbmFiaWxpdHnigJ0sIHdoaWNoIHlvdSBjYW4gZmluZCBoZXJlOiBodHRw czovL3VybGRlZmVuc2UuY29tL3YzL19faHR0cHM6Ly93d3cuY211LmVkdS9kaWV0cmljaC9waGls b3NvcGh5L2V2ZW50cy9uYWdlbC1sZWN0dXJlcy9wYXN0LWxlY3R1cmVzLmh0bWxfXzshIUlCeldM VXMhV2JROFN4cTl1T2hjLUg0MC1JOElnQThqRkVzWDlGSzdrSTBHV1BuQ3NqV3FFVzNBOVRoeDdI MTVyU21VQlp5SE92SVpFeG53YjhUSnJkOUNFN3p6ZVAySFd4OCQgLiBCdXQgSSBkb24ndCByZWNh bGwgaWYgUGVyIHByb3ZlcyB0aGUgZXhhY3QgdGhlb3JlbSB5b3Ugd2FudDsgaXQgbWlnaHQgYmUg YSBsaXR0bGUgZGlmZmVyZW50LCBqdWRnaW5nIGZyb20gdGhlIGFic3RyYWN0LgoKQmVzdCwKSm9u CgoKT24gMTIgSnVuIDIwMjMsIGF0IDIwOjU2LCBhbmRyZWouYmF1ZXJAYW5kcmVqLmNvbSB3cm90 ZToKCj4gWyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVwZW5uLmVkdS9tYWls bWFuL2xpc3RpbmZvL3R5cGVzLWxpc3QgXQo+Cj4gRGVhciBhbGwsCj4KPiBpbiBwcmVwYXJhdGlv biBmb3IgbXkgVFlQRVMgMjAyMyB0YWxrIEkgcmVhbGl6ZWQgSSBkb27igJl0IGFjdHVhbGx5IGtu b3cgb2YgYW55b25lIGhhdmluZyBwcm92ZWQgdGhlIGZvbGxvd2luZyBhYm91dCBNTFRUICjOoyAr IM6gICsgSWQgKyBOYXQpLgo+Cj4gRVFVSVZBTEVOQ0UgSU5WQVJJQU5DRTogTGV0IFAgYmUgYSB3 ZWxsLWZvcm1lZCB0eXBlIGV4cHJlc3Npb24gd2l0aCBhIHR5cGUgbWV0YS12YXJpYWJsZSBYLiBJ ZiBBIGFuZCBCIGFyZSBjbG9zZWQgdHlwZSBleHByZXNzaW9ucyBhbmQgZSA6IEEg4omDIEIgYW4g ZXF1aXZhbGVuY2UgYmV0d2VlbiB0aGVtLCB0aGVuIHRoZSB0eXBlIG9mIGVxdWl2YWxlbmNlcyBQ W0EvWF0g4omDIFBbQi9YXSBpcyBpbmhhYml0ZWQuCj4KPiBUaGVyZSBhcmUgbWFueSBwb3NzaWJs ZSB2YXJpYW50cywgb2YgY291cnNlLCBhbmQgSeKAmWQgYmUgaW50ZXJlc3RlZCBpbiBsZWFybmlu ZyBhYm91dCBhbnkgcmVzdWx0cyBpbiB0aGlzIGRpcmVjdGlvbiwgZXNwZWNpYWxseSBvbmVzIHRo YXQgZG9u4oCZdCB0aHJvdyBpbiBhbnkgYXhpb21zLgo+Cj4gSSBhbSB2YWd1ZWx5IHJlbWViZXJp bmcgdGhhdCBpdCBoYXMgYmVlbiBkb25lIGZvciBDaHVyY2jigJlzIHNpbXBsZSB0eXBlIHRoZW9y eSwgd2hpY2ggYWN0dWFsbHkgc291bmRzLCB3ZWxsLCBzaW1wbGUuIERvZXMgYW55b25lIGtub3cg YSByZWZlcmVuY2U/Cj4KPiBJIHRoaW5rIHRoZXJlIG1pZ2h0IGhhdmUgYmVlbiBzb21lIHdvcmsg YnkgQm9iIEhhcnBlciAmIERhbiBMaWNhdGEgKGh0dHBzOi8vdXJsZGVmZW5zZS5jb20vdjMvX19o dHRwczovL3d3dy5jcy5jbXUuZWR1LypkcmwvcHVicy9saDExMnR0L2xoMTIydHQtZmluYWwucGRm X187ZmchIUlCeldMVXMhV3c0WHJGeGpkU1VWRkdqVGdEM01Ub2xlRDg1VFJ3TFJHRkl5X3hqa1Fx dlN3M251cWE5Zld4TU54QVdZUFQ1RnlTMFJyOWhDY1d2OHAwNWJBNlhjM1pkRmlid2lLMHVsWW5z JCApLCBhbmQgYW5vdGhlciBieSBOaWNvbGFzIFRhYmFyZWF1ICYgTWF0dGhpZXUgU296ZWF1ICho dHRwczovL3VybGRlZmVuc2UuY29tL3YzL19faHR0cHM6Ly9kb2kub3JnLzEwLjExNDUvMzIzNjc4 N19fOyEhSUJ6V0xVcyFXdzRYckZ4amRTVVZGR2pUZ0QzTVRvbGVEODVUUndMUkdGSXlfeGprUXF2 U3czbnVxYTlmV3hNTnhBV1lQVDVGeVMwUnI5aENjV3Y4cDA1YkE2WGMzWmRGaWJ3aW4xWlNMekkk ICksIHdoaWNoIGN1dHMgdGhpbmcgb2ZmIGF0IHRoZSBncm91cG9pZCBsZXZlbC4gSSBhbSBub3Qg ZXZlbiBzdXJlIGlmIHRoZXkgcmVhbGx5IHByb3ZlIGFuIGFuYWxvZ3VlIG9mIHRoZSBwcmluY2lw bGUgc3RhdGVkIGFib3ZlLgo+Cj4gQnV0IGhvdyBhYm91dCBwdXJlIE1MVFQsIGhhcyBhbnlvbmUg ZG9uZSBpdD8KPgo+IFdpdGgga2luZCByZWdhcmRzLAo+Cj4gQW5kcmVqCg==