Re: [TYPES] Equivalence invariance for MLTT (reference request)
[email protected] Tue, 13 Jun 2023 20:47:23 +0200
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
WyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVwZW5uLmVkdS9tYWlsbWFuL2xp c3RpbmZvL3R5cGVzLWxpc3QgXQoKRGVhciBKb24sCgpJIG11c3QgaGF2ZSBzZWVuIGFuIGVhcmx5 IHZlcnNpb24gb2YgUGVy4oCZcyBOYWdlbCBsZWN0dXJlIHNvbWV3aGVyZS4gSSBkZWZpbml0ZWx5 IHdhc27igJl0IGF0IENNVSBpbiAyMDEzLiBJdCBsb29rcyBsaWtlIHRoZSB0aGluZyBJIHdhcyBs b29raW5nIGZvci4gSeKAmWxsIHRyeSB0byBjYWpvbGUgc29tZSB5b3VuZyBtaW5kcyBoZXJlIGF0 IFRZUEVTIDIwMjMgdG8gZm9ybWFsaXplIHRoZSBsZWN0dXJlcy4KCldpdGgga2luZCByZWdhcmRz LAoKQW5kcmVqCgo+IE9uIDEzIEp1biAyMDIzLCBhdCAxNTo1MCwgSm9uIFN0ZXJsaW5nIDxqb25A am9ubXN0ZXJsaW5nLmNvbT4gd3JvdGU6Cj4gCj4gRGVhciBBbmRyZWosCj4gCj4gSSBhbSBub3Qg Y29tcGxldGVseSBzdXJlIGJlY2F1c2UgaXQgaXMgYSB3aGlsZSBzaW5jZSBJIGhhZCB3YXRjaGVk IHRoaXMsIGJ1dCBJIHRoaW5rIHRoaXMgbWlnaHQgYmUgcmVsYXRlZCB0byB0aGUgdG9waWMgb2Yg UGVyIE1hcnRpbi1Mw7ZmJ3MgMjAxMyBFYXJuZXN0IE5hZ2VsIExlY3R1cmUg4oCcSW52YXJpYW5j ZSBVbmRlciBJc29tb3JwaGlzbSBhbmQgRGVmaW5hYmlsaXR54oCdLCB3aGljaCB5b3UgY2FuIGZp bmQgaGVyZTogaHR0cHM6Ly91cmxkZWZlbnNlLmNvbS92My9fX2h0dHBzOi8vd3d3LmNtdS5lZHUv ZGlldHJpY2gvcGhpbG9zb3BoeS9ldmVudHMvbmFnZWwtbGVjdHVyZXMvcGFzdC1sZWN0dXJlcy5o dG1sX187ISFJQnpXTFVzIVdYWXBrTlVWNXRZSmxWWHVpWlFJOTdDOGhYRVlaVmNvaGtMWXpvLXBu XzRWTkwxRDZlejZyVjF4Zjh2c2dlNE1OMzZBZjRmRF9pZWl2Z2F3cm1Dekh3d1o1TVhZbFowM29l cyQgLiBCdXQgSSBkb24ndCByZWNhbGwgaWYgUGVyIHByb3ZlcyB0aGUgZXhhY3QgdGhlb3JlbSB5 b3Ugd2FudDsgaXQgbWlnaHQgYmUgYSBsaXR0bGUgZGlmZmVyZW50LCBqdWRnaW5nIGZyb20gdGhl IGFic3RyYWN0Lgo+IAo+IEJlc3QsCj4gSm9uCj4gCj4gCj4gT24gMTIgSnVuIDIwMjMsIGF0IDIw OjU2LCBhbmRyZWouYmF1ZXJAYW5kcmVqLmNvbSA8bWFpbHRvOmFuZHJlai5iYXVlckBhbmRyZWou Y29tPiB3cm90ZToKPiAKPj4gWyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVw ZW5uLmVkdS9tYWlsbWFuL2xpc3RpbmZvL3R5cGVzLWxpc3QgXQo+PiAKPj4gRGVhciBhbGwsCj4+ IAo+PiBpbiBwcmVwYXJhdGlvbiBmb3IgbXkgVFlQRVMgMjAyMyB0YWxrIEkgcmVhbGl6ZWQgSSBk b27igJl0IGFjdHVhbGx5IGtub3cgb2YgYW55b25lIGhhdmluZyBwcm92ZWQgdGhlIGZvbGxvd2lu ZyBhYm91dCBNTFRUICjOoyArIM6gICsgSWQgKyBOYXQpLgo+PiAKPj4gRVFVSVZBTEVOQ0UgSU5W QVJJQU5DRTogTGV0IFAgYmUgYSB3ZWxsLWZvcm1lZCB0eXBlIGV4cHJlc3Npb24gd2l0aCBhIHR5 cGUgbWV0YS12YXJpYWJsZSBYLiBJZiBBIGFuZCBCIGFyZSBjbG9zZWQgdHlwZSBleHByZXNzaW9u cyBhbmQgZSA6IEEg4omDIEIgYW4gZXF1aXZhbGVuY2UgYmV0d2VlbiB0aGVtLCB0aGVuIHRoZSB0 eXBlIG9mIGVxdWl2YWxlbmNlcyBQW0EvWF0g4omDIFBbQi9YXSBpcyBpbmhhYml0ZWQuCj4+IAo+ PiBUaGVyZSBhcmUgbWFueSBwb3NzaWJsZSB2YXJpYW50cywgb2YgY291cnNlLCBhbmQgSeKAmWQg YmUgaW50ZXJlc3RlZCBpbiBsZWFybmluZyBhYm91dCBhbnkgcmVzdWx0cyBpbiB0aGlzIGRpcmVj dGlvbiwgZXNwZWNpYWxseSBvbmVzIHRoYXQgZG9u4oCZdCB0aHJvdyBpbiBhbnkgYXhpb21zLgo+ PiAKPj4gSSBhbSB2YWd1ZWx5IHJlbWViZXJpbmcgdGhhdCBpdCBoYXMgYmVlbiBkb25lIGZvciBD aHVyY2jigJlzIHNpbXBsZSB0eXBlIHRoZW9yeSwgd2hpY2ggYWN0dWFsbHkgc291bmRzLCB3ZWxs LCBzaW1wbGUuIERvZXMgYW55b25lIGtub3cgYSByZWZlcmVuY2U/Cj4+IAo+PiBJIHRoaW5rIHRo ZXJlIG1pZ2h0IGhhdmUgYmVlbiBzb21lIHdvcmsgYnkgQm9iIEhhcnBlciAmIERhbiBMaWNhdGEg KGh0dHBzOi8vdXJsZGVmZW5zZS5jb20vdjMvX19odHRwczovL3d3dy5jcy5jbXUuZWR1Lypkcmwv cHVicy9saDExMnR0L2xoMTIydHQtZmluYWwucGRmX187ZmchIUlCeldMVXMhV3c0WHJGeGpkU1VW RkdqVGdEM01Ub2xlRDg1VFJ3TFJHRkl5X3hqa1FxdlN3M251cWE5Zld4TU54QVdZUFQ1RnlTMFJy OWhDY1d2OHAwNWJBNlhjM1pkRmlid2lLMHVsWW5zJCApLCBhbmQgYW5vdGhlciBieSBOaWNvbGFz IFRhYmFyZWF1ICYgTWF0dGhpZXUgU296ZWF1IChodHRwczovL3VybGRlZmVuc2UuY29tL3YzL19f aHR0cHM6Ly9kb2kub3JnLzEwLjExNDUvMzIzNjc4N19fOyEhSUJ6V0xVcyFXdzRYckZ4amRTVVZG R2pUZ0QzTVRvbGVEODVUUndMUkdGSXlfeGprUXF2U3czbnVxYTlmV3hNTnhBV1lQVDVGeVMwUnI5 aENjV3Y4cDA1YkE2WGMzWmRGaWJ3aW4xWlNMekkkICksIHdoaWNoIGN1dHMgdGhpbmcgb2ZmIGF0 IHRoZSBncm91cG9pZCBsZXZlbC4gSSBhbSBub3QgZXZlbiBzdXJlIGlmIHRoZXkgcmVhbGx5IHBy b3ZlIGFuIGFuYWxvZ3VlIG9mIHRoZSBwcmluY2lwbGUgc3RhdGVkIGFib3ZlLgo+PiAKPj4gQnV0 IGhvdyBhYm91dCBwdXJlIE1MVFQsIGhhcyBhbnlvbmUgZG9uZSBpdD8KPj4gCj4+IFdpdGgga2lu ZCByZWdhcmRzLAo+PiAKPj4gQW5kcmVqCgo=