Re: [TYPES] Equivalence invariance for MLTT (reference request)
[email protected] Mon, 26 Jun 2023 10:14:03 +0200
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
WyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVwZW5uLmVkdS9tYWlsbWFuL2xp c3RpbmZvL3R5cGVzLWxpc3QgXQoKRGVhciBTdGV2ZSwKCnRoYW5rcyBmb3IgdGhlIHJlZmVyZW5j ZXMuIEluIG15IFRZUEVTIHRhbGsgSSAgbWVudGlvbmVkIGJvdGggTGluZWRhbmJhdW0gJiBUYXJz a2kgYW5kIFBlci1NYXJ0aW4gTMO2ZiAoYXMgd2VsbCBhcyB5b3VyIGludmFyaWFuY2UgcHJvcGVy dHksIGJ1dCBpdCBkb2VzbuKAmXQgc2hvdyB1cCBvbiB0aGUgc2xpZGVzIGV4cGxpY2l0bHksIEkg dGhpbmssIGl04oCZcyBpbiB0aGUgc3BlYWtlciBub3RlcyDigJMgSSBzaG91bGQgcHVibGlzaCB0 aGUgc2xpZGVzKS4gQXQgVFlQRVMgSSBsZWFybmVkIGFib3V0CgrigJxFeHRlcm5hbCB1bml2YWxl bmNlIGZvciBzZWNvbmQtb3JkZXIgZ2VuZXJhbGl6ZWQgYWxnZWJyYWljIHRoZW9yaWVz4oCdLCBS YWZhw6tsIEJvY3F1ZXQsIGh0dHBzOi8vdXJsZGVmZW5zZS5jb20vdjMvX19odHRwczovL2FyeGl2 Lm9yZy9hYnMvMjIxMS4wNzQ4N19fOyEhSUJ6V0xVcyFTRFpJNkgwVU03UHVPbE1JZTl4dHlvMEFv LWlWd1dYVl96bENXMHBaTFR0cENwbHdJV3RmU0F0UlltNGdhWXZjcDFOWUIzN2s0Q2RfeXkyX1Fq ak9BZ3JtYVJwV3RLY2JjZHMkIAoKVGhpcyB3b3JrIGdlbmVyYWxpemVzIHByZXZpb3VzIHJlc3Vs dHMsIGluY2x1ZGluZyBQZXItTWFydGluIEzDtmbigJlzIE5hZ2VsIGxlY3R1cmUuCgpXaXRoIGtp bmQgcmVnYXJkcywKCkFuZHJlagoKCgo+IE9uIDI1IEp1biAyMDIzLCBhdCAwODowOSwgU3RldmUg QXdvZGV5IDxhd29kZXlAYW5kcmV3LmNtdS5lZHU+IHdyb3RlOgo+IAo+IEdlbnRzLAo+IAo+IFRo aXMgaW52YXJpYW5jZSBwcm9wZXJ0eSB3YXMgbWVudGlvbmVkIGluIG15IDIwMTMgcGFwZXI6Cj4g Cj4gaHR0cHM6Ly91cmxkZWZlbnNlLmNvbS92My9fX2h0dHBzOi8vd3d3LmFuZHJldy5jbXUuZWR1 L3VzZXIvYXdvZGV5L3ByZXByaW50cy9zaXUucGRmX187ISFJQnpXTFVzIVNEWkk2SDBVTTdQdU9s TUllOXh0eW8wQW8taVZ3V1hWX3psQ1cwcFpMVHRwQ3Bsd0lXdGZTQXRSWW00Z2FZdmNwMU5ZQjM3 azRDZF95eTJfUWpqT0Fncm1hUnBXelhCQXVzZyQgCj4gCj4gYW5kIGlzIGRpc2N1c3NlZCBpbiBt b3JlIGRldGFpbCBpbiB0aGlzIG9uZSBmcm9tIDIwMTg6Cj4gCj4gaHR0cHM6Ly91cmxkZWZlbnNl LmNvbS92My9fX2h0dHBzOi8vd3d3LmFuZHJldy5jbXUuZWR1L3VzZXIvYXdvZGV5L3ByZXByaW50 cy91YXBsLnBkZl9fOyEhSUJ6V0xVcyFTRFpJNkgwVU03UHVPbE1JZTl4dHlvMEFvLWlWd1dYVl96 bENXMHBaTFR0cENwbHdJV3RmU0F0UlltNGdhWXZjcDFOWUIzN2s0Q2RfeXkyX1Fqak9BZ3JtYVJw V2s3dDRjTnMkIAo+IAo+IEludmFyaWFuY2UgdW5kZXIgZXF1aXZhbGVuY2UgaW4gTUxUVCBvZiBj b3Vyc2UgZ2VuZXJhbGl6ZXMgaXNvbW9ycGhpc20gaW52YXJpYW5jZSBpbiAqc2ltcGxlKiB0eXBl IHRoZW9yeSwgCj4gd2hpY2ggd2FzIHByb3ZlZCBieSBMaW5kZW5iYXVtICYgVGFyc2tpIGluIDE5 MzUuCj4gCj4gUGVy4oCZcyAyMDEzIE5hZ2VsIExlY3R1cmUgYXQgQ01VIHdhcyBvbiBhIHJlbGF0 ZWQgYnV0IGRpZmZlcmVudCB0b3BpYywgbmFtZWx5ICpyZWxhdGlvbmFsIGludmFyaWFuY2UqIOKA lCAgaS5lLiDigJxwYXJhbWV0cmljaXR54oCdIOKAlCBhbmQgZXNzZW50aWFsbHkgc2tldGNoZXMg YSByZWxhdGlvbmFsIG1vZGVsIG9mIFRUIChhIG1vZGVsIGluIFNldF5HIGZvciB0aGUgZ3JhcGgg Y2F0ZWdvcnkgRyA9ICogXHJpZ2h0cmlnaHRhcnJvd3MgKikuCj4gCj4gSW4gdGhlIHBhcGVycyBj aXRlZCBhYm92ZSwgSSBtYWRlIHRoZSBwb2ludCB0aGF0IFZW4oCZcyBtb2RlbCBvZiB1bml2YWxl bmNlIGltcGxpZXMgdGhhdCB0aGVyZSBjYW5ub3QgYmUgYSBjbG9zZWQgdHlwZSBcWC5QKFgpIHdp dGggWCA6IFUgdGhhdOKAmXMgKm5vdCogZXF1aXZhbGVuY2UgaW52YXJpYW50LCBlbHNlIGdpdmVu IEEgfiBCIGFuZCBQKEEpIHdlIHdvdWxkIGhhdmUgYm90aCBQKEIpIGZyb20gdW5pdmFsZW5jZSBh bmQgdHJhbnNwb3J0LCBidXQgbm90IFAoQiksIGJ5IGFzc3VtcHRpb24uICBJIHRoaW5rIFBldGVy IEwuIG9ic2VydmVkIHRoYXQgdGhpcyBzZW1hbnRpYyBhcmd1bWVudCBzdGlsbCBhZG1pdHMgdGhl IHBvc3NpYmlsaXR5IHRoYXQgaW4gTUxUVCB3L28gVUEgdGhlcmUgZXhpc3QgY2xvc2VkIHRlcm1z Cj4gCj4gfC0gZSA6IEEgfiBCCj4gfC0gYSA6IFAoQSkKPiAKPiBidXQgbm8gY2xvc2VkIHRlcm0g Cj4gCj4gfC0gYiA6IFAoQikuCj4gCj4gT2YgY291cnNlLCBvbmUgY2FuIGFsc28gZ2l2ZSBhIGRp cmVjdCBzeW50YWN0aWMgcHJvb2Ygb2YgZXF1aXZhbGVuY2UgaW52YXJpYW5jZSBieSBpbmR1Y3Rp b24gb24gdGhlIHR5cGUgc3RydWN0dXJlIC0gdGhlIGNhc2VzIG9mIHdoaWNoIGFyZSBlc3NlbnRp YWxseSBkb25lIGluIENoYXB0ZXIgMiBvZiB0aGUgSG9UVCBCb29rLgo+IAo+IE15IChyaGV0b3Jp Y2FsKSBpbnRlcmVzdCBpbiB0aGlzIGludmFyaWFuY2UgcHJvcGVydHkgd2FzIFRhcnNraSdzIDE5 NjYgcHJvcG9zYWwgdG8gdGFrZSBpc29tb3JwaGlzbSBpbnZhcmlhbmNlIG9mIGNvbmNlcHRzIGlu IHNpbXBsZSB0eXBlIHRoZW9yeSBhcyBhbiBleHBsaWNhdGlvbiBvZiBhIOKAnGxvZ2ljYWwgY29u Y2VwdOKAnSwgZXh0ZW5kaW5nIEZlbGl4IEtsZWlu4oCZcyBjaGFyYWN0ZXJpemF0aW9uIG9mIGRp ZmZlcmVudCBnZW9tZXRyaWMgbm90aW9ucy4gIE15IHBvaW50IHdhcyB0aGF0IGVxdWl2YWxlbmNl IGludmFyaWFuY2UgaW4gTUxUVCBpcyBhbiBldmVuIHdpZGVyIHJlbGF0aW9uIHRoYW4gaXNvbW9y cGhpc20gaW52YXJpYW5jZSBpbiBTVFQsIGFuZCB0aHVzIGRldGVtaW5lcyBhbiBldmVuIG1vcmUg Z2VuZXJhbCBjbGFzcyBvZiBjb25jZXB0cyB0aGF0IGNhbiBiZSByZWdhcmRlZCBhcyDigJxsb2dp Y2Fs4oCdLiAgQnV0IHBlcmhhcHMgdGhleSBzaG91bGQgaW5zdGVhZCBiZSByZWdhcmRlZCBhcyBz b21ldGhpbmcgZXZlbiBtb3JlIGdlbmVyYWwsIHN1Y2ggYXMgImNvbnN0cnVjdGlibGXigJ0/Cj4g Cj4gQmVzdCB3aXNoZXMsCj4gCj4gU3RldmUKPiAKPiAKPj4gT24gSnVuIDI0LCAyMDIzLCBhdCAx MDoyMSBQTSwgdHlwZXMtbGlzdC1yZXF1ZXN0QGxpc3RzLnNlYXMudXBlbm4uZWR1IDx0eXBlcy1s aXN0LXJlcXVlc3RATElTVFMuU0VBUy5VUEVOTi5FRFU+IHdyb3RlOgo+PiAKPj4gTWVzc2FnZTog Mwo+PiBEYXRlOiBUdWUsIDEzIEp1biAyMDIzIDE1OjUwOjA3ICswMjAwCj4+IEZyb206IEpvbiBT dGVybGluZyA8am9uQGpvbm1zdGVybGluZy5jb20+Cj4+IFRvOiBhbmRyZWouYmF1ZXJAYW5kcmVq LmNvbQo+PiBDYzogdHlwZXMtbGlzdEBsaXN0cy5zZWFzLnVwZW5uLmVkdQo+PiBTdWJqZWN0OiBS ZTogW1RZUEVTXSBFcXVpdmFsZW5jZSBpbnZhcmlhbmNlIGZvciBNTFRUIChyZWZlcmVuY2UKPj4g cmVxdWVzdCkKPj4gTWVzc2FnZS1JRDogPDI5QTc0QzMxLTYxOTUtNDU2Ny1BQzg2LTg5RDcwQkY0 OUE1QkBqb25tc3RlcmxpbmcuY29tPgo+PiBDb250ZW50LVR5cGU6IHRleHQvcGxhaW47IGNoYXJz ZXQ9IlVURi04Igo+PiAKPj4gRGVhciBBbmRyZWosCj4+IAo+PiBJIGFtIG5vdCBjb21wbGV0ZWx5 IHN1cmUgYmVjYXVzZSBpdCBpcyBhIHdoaWxlIHNpbmNlIEkgaGFkIHdhdGNoZWQgdGhpcywgYnV0 IEkgdGhpbmsgdGhpcyBtaWdodCBiZSByZWxhdGVkIHRvIHRoZSB0b3BpYyBvZiBQZXIgTWFydGlu LUw/ZidzIDIwMTMgRWFybmVzdCBOYWdlbCBMZWN0dXJlID9JbnZhcmlhbmNlIFVuZGVyIElzb21v cnBoaXNtIGFuZCBEZWZpbmFiaWxpdHk/LCB3aGljaCB5b3UgY2FuIGZpbmQgaGVyZTogaHR0cHM6 Ly91cmxkZWZlbnNlLmNvbS92My9fX2h0dHBzOi8vd3d3LmNtdS5lZHUvZGlldHJpY2gvcGhpbG9z b3BoeS9ldmVudHMvbmFnZWwtbGVjdHVyZXMvcGFzdC1sZWN0dXJlcy5odG1sX187ISFJQnpXTFVz IVdiUThTeHE5dU9oYy1INDAtSThJZ0E4akZFc1g5Rks3a0kwR1dQbkNzaldxRVczQTlUaHg3SDE1 clNtVUJaeUhPdklaRXhud2I4VEpyZDlDRTd6emVQMkhXeDgkIC4gQnV0IEkgZG9uJ3QgcmVjYWxs IGlmIFBlciBwcm92ZXMgdGhlIGV4YWN0IHRoZW9yZW0geW91IHdhbnQ7IGl0IG1pZ2h0IGJlIGEg bGl0dGxlIGRpZmZlcmVudCwganVkZ2luZyBmcm9tIHRoZSBhYnN0cmFjdC4KPj4gCj4+IEJlc3Qs Cj4+IEpvbgo+PiAKPj4gCj4+IE9uIDEyIEp1biAyMDIzLCBhdCAyMDo1NiwgYW5kcmVqLmJhdWVy QGFuZHJlai5jb20gd3JvdGU6Cj4+IAo+Pj4gWyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0 cy5zZWFzLnVwZW5uLmVkdS9tYWlsbWFuL2xpc3RpbmZvL3R5cGVzLWxpc3QgXQo+Pj4gCj4+PiBE ZWFyIGFsbCwKPj4+IAo+Pj4gaW4gcHJlcGFyYXRpb24gZm9yIG15IFRZUEVTIDIwMjMgdGFsayBJ IHJlYWxpemVkIEkgZG9uP3QgYWN0dWFsbHkga25vdyBvZiBhbnlvbmUgaGF2aW5nIHByb3ZlZCB0 aGUgZm9sbG93aW5nIGFib3V0IE1MVFQgKD8gKyA/ICsgSWQgKyBOYXQpLgo+Pj4gCj4+PiBFUVVJ VkFMRU5DRSBJTlZBUklBTkNFOiBMZXQgUCBiZSBhIHdlbGwtZm9ybWVkIHR5cGUgZXhwcmVzc2lv biB3aXRoIGEgdHlwZSBtZXRhLXZhcmlhYmxlIFguIElmIEEgYW5kIEIgYXJlIGNsb3NlZCB0eXBl IGV4cHJlc3Npb25zIGFuZCBlIDogQSA/IEIgYW4gZXF1aXZhbGVuY2UgYmV0d2VlbiB0aGVtLCB0 aGVuIHRoZSB0eXBlIG9mIGVxdWl2YWxlbmNlcyBQW0EvWF0gPyBQW0IvWF0gaXMgaW5oYWJpdGVk Lgo+Pj4gCj4+PiBUaGVyZSBhcmUgbWFueSBwb3NzaWJsZSB2YXJpYW50cywgb2YgY291cnNlLCBh bmQgST9kIGJlIGludGVyZXN0ZWQgaW4gbGVhcm5pbmcgYWJvdXQgYW55IHJlc3VsdHMgaW4gdGhp cyBkaXJlY3Rpb24sIGVzcGVjaWFsbHkgb25lcyB0aGF0IGRvbj90IHRocm93IGluIGFueSBheGlv bXMuCj4+PiAKPj4+IEkgYW0gdmFndWVseSByZW1lYmVyaW5nIHRoYXQgaXQgaGFzIGJlZW4gZG9u ZSBmb3IgQ2h1cmNoP3Mgc2ltcGxlIHR5cGUgdGhlb3J5LCB3aGljaCBhY3R1YWxseSBzb3VuZHMs IHdlbGwsIHNpbXBsZS4gRG9lcyBhbnlvbmUga25vdyBhIHJlZmVyZW5jZT8KPj4+IAo+Pj4gSSB0 aGluayB0aGVyZSBtaWdodCBoYXZlIGJlZW4gc29tZSB3b3JrIGJ5IEJvYiBIYXJwZXIgJiBEYW4g TGljYXRhIChodHRwczovL3VybGRlZmVuc2UuY29tL3YzL19faHR0cHM6Ly93d3cuY3MuY211LmVk dS8qZHJsL3B1YnMvbGgxMTJ0dC9saDEyMnR0LWZpbmFsLnBkZl9fO2ZnISFJQnpXTFVzIVd3NFhy RnhqZFNVVkZHalRnRDNNVG9sZUQ4NVRSd0xSR0ZJeV94amtRcXZTdzNudXFhOWZXeE1OeEFXWVBU NUZ5UzBScjloQ2NXdjhwMDViQTZYYzNaZEZpYndpSzB1bFlucyQgKSwgYW5kIGFub3RoZXIgYnkg Tmljb2xhcyBUYWJhcmVhdSAmIE1hdHRoaWV1IFNvemVhdSAoaHR0cHM6Ly91cmxkZWZlbnNlLmNv bS92My9fX2h0dHBzOi8vZG9pLm9yZy8xMC4xMTQ1LzMyMzY3ODdfXzshIUlCeldMVXMhV3c0WHJG eGpkU1VWRkdqVGdEM01Ub2xlRDg1VFJ3TFJHRkl5X3hqa1FxdlN3M251cWE5Zld4TU54QVdZUFQ1 RnlTMFJyOWhDY1d2OHAwNWJBNlhjM1pkRmlid2luMVpTTHpJJCApLCB3aGljaCBjdXRzIHRoaW5n IG9mZiBhdCB0aGUgZ3JvdXBvaWQgbGV2ZWwuIEkgYW0gbm90IGV2ZW4gc3VyZSBpZiB0aGV5IHJl YWxseSBwcm92ZSBhbiBhbmFsb2d1ZSBvZiB0aGUgcHJpbmNpcGxlIHN0YXRlZCBhYm92ZS4KPj4+ IAo+Pj4gQnV0IGhvdyBhYm91dCBwdXJlIE1MVFQsIGhhcyBhbnlvbmUgZG9uZSBpdD8KPj4+IAo+ Pj4gV2l0aCBraW5kIHJlZ2FyZHMsCj4+PiAKPj4+IEFuZHJlago+PiAKPiAKCg==