From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDTLDGMZRMJBBDVA4LNQKGQEBPRECEY@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-oi0-x240.google.com (mail-oi0-x240.google.com [IPv6:2607:f8b0:4003:c06::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e251a3fb for ; Sat, 18 Aug 2018 21:30:55 +0000 (UTC) Received: by mail-oi0-x240.google.com with SMTP id w185-v6sf10525769oig.19 for ; Sat, 18 Aug 2018 14:30:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=8CKox+CzO32gB7DeazJIPzl5C2nBP2tGyYch/MVapUA=; b=Nja2o3n6f6wyb7X46HiPX6aICLS5bUmo9EPxQavaABdHgj3zGsuXz3HwKqMF3PhlzJ Hd57GdT6X9ZphOafFJ8MTqM7SF762hOMS09yGJCD0oYlcuGtuygrTPmsF3t5Ar3VOi+h 55Ry7VoEqtWI/isVJgHzrhf7f88//BfcwfvEvQOb7LTZJ4PAdlal8n72/lQJT44Z+y/E c/Z0f2CLBFGQ5BgwzDZXdw+POyDOhyquK6sHBTrxl9tXNobt0PjelxbW2R1adCqE5FpG fSGYZ4vI1/kakcHMzXrsDSb8KFqVBcU1EegkAWfwMF1L9E+yYpJPMv6FuOIRauf826aM SIAw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=8CKox+CzO32gB7DeazJIPzl5C2nBP2tGyYch/MVapUA=; b=SF3WnIJsQexmMEhtE8a+MDmicSohlT/jaRp/TTPOqm2Hoh0aGamB5GDpgTx9P+qCrs fhIi82/icFyBd0zInIU2P+3ViD70yur0/3CZ33mJCfslsrvhV6Wn3rk/krifyxhOLJRp jMG5TVoYGaKuO/22EqViRVh2CumLV+SytECTeXJyrvSthqpnt0Jy/GKuTHFaORgcA+Xu PDe+I/cjKXsb5xWOvtjzlsWXLiF5RMkLUgQTItcqy8/drZhlxBKt6Gzzhx6tgkJoQB0B u+EMklfP6CO8NSudkrWgnpWK4vkaGn14EoqN7FnSFbNeA1YRGIYrSBCaMZgElCbVs/ew 5PUg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=8CKox+CzO32gB7DeazJIPzl5C2nBP2tGyYch/MVapUA=; b=oJWXaqDGRorzFwZyhu82uozQBiVDSBKofBMjQmx+ClW0uK1SGtyRcXpN1louZO4Rh7 kxYIfY5AzIqX/WGNqdtFPbrFRB8bLfztAX+u0cBl10hHyW7naoMqDd4q5zVdbr/A2l+8 js0XEpSThtkfxZCmv5UtMObR8f/7WAYYOaCLuMmJih6qdnGbNMZ6zRb0sYC//STHBnQ5 nUPtQD7jN913dbJkCog2jyObj3Q5FDPWjKTYbHO5mFF8Q1QjqZPjzEJsPvaDS/irD4pN QCeBXESE8E2CrFKalITsUxSIOFYssbKrmdgW/JEJgRsJtQuLj9TYw1PaY75oM5QJYGGR 849w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFNvtXal6YphExn/LboT4xZaTvZywHeXyo4i2HcXkqkh3jadxoJ afn0w2FsLKKI9D4khUEK/YI= X-Google-Smtp-Source: AA+uWPy8I4uMx2PgYin2rG0sOr+oaC2ET+WdlSFhrGmTYO4u7ZQxyzoh06MOAoH43CV5XdBfIT0mRw== X-Received: by 2002:aca:4787:: with SMTP id u129-v6mr959041oia.4.1534627854273; Sat, 18 Aug 2018 14:30:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:8d0:: with SMTP id 199-v6ls1018559oii.9.gmail; Sat, 18 Aug 2018 14:30:54 -0700 (PDT) X-Received: by 2002:aca:75c9:: with SMTP id q192-v6mr934603oic.3.1534627853803; Sat, 18 Aug 2018 14:30:53 -0700 (PDT) Date: Sat, 18 Aug 2018 14:30:53 -0700 (PDT) From: Corlin Fardal To: Homotopy Type Theory Message-Id: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com> Subject: [HoTT] 1D Mu Type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1040_367336794.1534627853175" X-Original-Sender: fardalcorlin@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_1040_367336794.1534627853175 Content-Type: multipart/alternative; boundary="----=_Part_1041_1070182594.1534627853175" ------=_Part_1041_1070182594.1534627853175 Content-Type: text/plain; charset="UTF-8" I've managed to create a 1D Mu Type, essentially just a basis for creating any recursive higher inductive type with point and path constructors one could define. The construction is mainly based upon the paper "Higher Inductive Types in Programming," at http://www.cs.ru.nl/~herman/PUBS/HIT-programming.pdf. The construction reduces the path constructors to just one, by introducing a case term, and extends the polynomial functors to include function types, and introduces an application term and lambda term for the function types. To be able to deal with the new terms, the construction defines a type coercion function to make the path computation rule type check, but the way that it is defined makes it equal to the identity function, under case analysis that would compute down for any specific type. More details, of course, are in the Coq and Agda files attached to this post. With this type we have a starting point for many next steps, including exploring the semantics of this new type, including showing that it gives rise to a cell monad, and showing homotopy initiality. Another next step would be seeing if we can define this type through some clever use of quotient types, perhaps in a similar way to the construction of propositional truncation. I didn't write a paper about this, largely because it is just a fairly straight forward extension of an existing paper, and also because I'm not a terribly good writer, but I hope that this post suffices in sharing what little I've managed to accomplish. I also hope that this post doesn't seem too out of the ordinary for what's posted here, as this is the first thing I've ever posted, and I'm very new to this group in general, though I have read a good few things on here already, and from what I can tell, this doesn't seem too strange. I checked various cases of HITs with my Mu type, and while the various constructors and induction rules seem to align with my intuition for what they should be, I don't actually know of anywhere where the induction rules for various kinds of inductive types exist, so I'd like to know if the definitions are correct, or if I messed anything up. In general, I'd be interested in anyone's thoughts about this. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_1041_1070182594.1534627853175 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I've managed to create a 1D Mu Type, essentially just = a basis for creating any recursive higher inductive type with point and pat= h constructors one could define. The construction is mainly based upon the = paper "Higher Inductive Types in Programming," at=C2=A0http://www= .cs.ru.nl/~herman/PUBS/HIT-programming.pdf. The construction reduces the pa= th constructors to just one, by introducing a case term, and extends the po= lynomial functors to include function types, and introduces an application = term and lambda term for the function types. To be able to deal with the ne= w terms, the construction defines a type coercion function to make the path= computation rule type check, but the way that it is defined makes it equal= to the identity function, under case analysis that would compute down for = any specific type. More details, of course, are in the Coq and Agda files a= ttached to this post.

With this type we have a starting = point for many next steps, including exploring the semantics of this new ty= pe, including showing that it gives rise to a cell monad, and showing homot= opy initiality. Another next step would be seeing if we can define this typ= e through some clever use of quotient types, perhaps in a similar way to th= e construction of propositional truncation.

I didn= 't write a paper about this, largely because it is just a fairly straig= ht forward extension of an existing paper, and also because I'm not a t= erribly good writer, but I hope that this post suffices in sharing what lit= tle I've managed to accomplish. I also hope that this post doesn't = seem too out of the ordinary for what's posted here, as this is the fir= st thing I've ever posted, and I'm very new to this group in genera= l, though I have read a good few things on here already, and from what I ca= n tell, this doesn't seem too strange.

I check= ed various cases of HITs with my Mu type, and while the various constructor= s and induction rules seem to align with my intuition for what they should = be, I don't actually know of anywhere where the induction rules for var= ious kinds of inductive types exist, so I'd like to know if the definit= ions are correct, or if I messed anything up. In general, I'd be intere= sted in anyone's thoughts about this.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_1041_1070182594.1534627853175-- ------=_Part_1040_367336794.1534627853175 Content-Type: application/octet-stream; name=Mu1.agda Content-Transfer-Encoding: base64 Content-Disposition: attachment; filename=Mu1.agda X-Attachment-Id: e035a2f5-cc54-4c4b-8d69-68b985c19b71 Content-ID: ey0jIE9QVElPTlMgLS13aXRob3V0LUsgLS1yZXdyaXRpbmcgIy19DQpvcGVuIGltcG9ydCBBZ2Rh LlByaW1pdGl2ZQ0KDQpkYXRhIF/iiaFfIHthIDogTGV2ZWx9IHtBIDogU2V0IGF9ICh4IDogQSkg OiBBIOKGkiBTZXQgYSB3aGVyZQ0KIHJlZmwgOiB4IOKJoSB4DQp7LSMgQlVJTFRJTiBSRVdSSVRF IF/iiaFfICMtfQ0Key0jIEJVSUxUSU4gRVFVQUxJVFkgX+KJoV8gIy19DQp7LSMgQlVJTFRJTiBS RUZMIHJlZmwgIy19DQoNCmRhdGEgXytfIChBIEIgOiBTZXQpIDogU2V0IHdoZXJlDQogaW5sIDog QSDihpIgQSArIEINCiBpbnIgOiBCIOKGkiBBICsgQg0KDQpkYXRhIF/Dl18gKEEgQiA6IFNldCkg OiBTZXQgd2hlcmUNCiBfLF8gOiBBIOKGkiBCIOKGkiBBIMOXIEINCg0KZGF0YSBGQ29kZSA6IFNl dOKCgSB3aGVyZQ0KIElkIDogRkNvZGUNCiBDb25zdCA6IFNldCDihpIgRkNvZGUNCiBTdW0gOiBG Q29kZSDihpIgRkNvZGUg4oaSIEZDb2RlDQogUHJvZCA6IEZDb2RlIOKGkiBGQ29kZSDihpIgRkNv ZGUNCiBGdW5jIDogU2V0IOKGkiBGQ29kZSDihpIgRkNvZGUNCg0KRkludGVyIDogRkNvZGUg4oaS IFNldCDihpIgU2V0DQpGSW50ZXIgSWQgWCA9IFgNCkZJbnRlciAoQ29uc3QgQSkgWCA9IEENCkZJ bnRlciAoU3VtIEYgRykgWCA9IEZJbnRlciBGIFggKyBGSW50ZXIgRyBYDQpGSW50ZXIgKFByb2Qg RiBHKSBYID0gRkludGVyIEYgWCDDlyBGSW50ZXIgRyBYDQpGSW50ZXIgKEZ1bmMgQSBGKSBYID0g QSDihpIgRkludGVyIEYgWA0KDQpGTGlmdCA6IHtYIDogU2V0fSAoRiA6IEZDb2RlKSDihpIgKFgg 4oaSIFNldCkg4oaSIChGSW50ZXIgRiBYIOKGkiBTZXQpDQpGTGlmdCBJZCBQIHggPSBQIHgNCkZM aWZ0IChDb25zdCBBKSBQIF8gPSBBDQpGTGlmdCAoU3VtIEYgRykgUCAoaW5sIHgpID0gRkxpZnQg RiBQIHgNCkZMaWZ0IChTdW0gRiBHKSBQIChpbnIgeCkgPSBGTGlmdCBHIFAgeA0KRkxpZnQgKFBy b2QgRiBHKSBQICh4ICwgeSkgPSBGTGlmdCBGIFAgeCDDlyBGTGlmdCBHIFAgeQ0KRkxpZnQgKEZ1 bmMgQSBGKSBQIGYgPSAoeCA6IEEpIOKGkiBGTGlmdCBGIFAgKGYgeCkNCg0KYWxsIDoge1ggOiBT ZXR9IChGIDogRkNvZGUpIHtQIDogWCDihpIgU2V0fSAoZiA6ICh4IDogWCkg4oaSIFAgeCkgKHgg OiBGSW50ZXIgRiBYKSDihpIgRkxpZnQgRiBQIHgNCmFsbCBJZCBmIHggPSBmIHgNCmFsbCAoQ29u c3QgQSkgZiBhID0gYQ0KYWxsIChTdW0gRiBHKSBmIChpbmwgeCkgPSBhbGwgRiBmIHgNCmFsbCAo U3VtIEYgRykgZiAoaW5yIHgpID0gYWxsIEcgZiB4DQphbGwgKFByb2QgRiBHKSBmICh4ICwgeSkg PSAoYWxsIEYgZiB4ICwgYWxsIEcgZiB5KQ0KYWxsIChGdW5jIEEgRikgZiBmJyA9IM67IHgg4oaS IGFsbCBGIGYgKGYnIHgpDQoNCmRhdGEgVENvZGUgWCBGIChjIDogRkludGVyIEYgWCDihpIgWCkg OiBGQ29kZSDihpIgRkNvZGUg4oaSIFNldOKCgSB3aGVyZQ0KIGlkIDoge0cgOiBGQ29kZX0g4oaS IFRDb2RlIFggRiBjIEcgRw0KIGNvbnN0IDoge0cgOiBGQ29kZX0ge0EgOiBTZXR9IOKGkiBBIOKG kiBUQ29kZSBYIEYgYyBHIChDb25zdCBBKQ0KIGNvbiA6IHtHIDogRkNvZGV9IOKGkiBUQ29kZSBY IEYgYyBHIEYg4oaSIFRDb2RlIFggRiBjIEcgSWQNCiBwaSA6IHtHIEggSSA6IEZDb2RlfSDihpIg VENvZGUgWCBGIGMgRyAoUHJvZCBIIEkpIOKGkiBUQ29kZSBYIEYgYyBHIEgNCiBwaScgOiB7RyBI IEkgOiBGQ29kZX0g4oaSIFRDb2RlIFggRiBjIEcgKFByb2QgSCBJKSDihpIgVENvZGUgWCBGIGMg RyBJDQogcGFpciA6IHtHIEggSSA6IEZDb2RlfSDihpIgVENvZGUgWCBGIGMgRyBIIOKGkiBUQ29k ZSBYIEYgYyBHIEkg4oaSIFRDb2RlIFggRiBjIEcgKFByb2QgSCBJKQ0KIGsgOiB7RyBIIEkgOiBG Q29kZX0g4oaSIFRDb2RlIFggRiBjIEcgSCDihpIgVENvZGUgWCBGIGMgRyAoU3VtIEggSSkNCiBr JyA6IHtHIEggSSA6IEZDb2RlfSDihpIgVENvZGUgWCBGIGMgRyBJIOKGkiBUQ29kZSBYIEYgYyBH IChTdW0gSCBJKQ0KIGNhc2UgOiB7RyBIIEkgSiA6IEZDb2RlfSDihpIgVENvZGUgWCBGIGMgRyAo U3VtIEggSSkg4oaSIFRDb2RlIFggRiBjIChQcm9kIEcgSCkgSiDihpIgVENvZGUgWCBGIGMgKFBy b2QgRyBJKSBKIOKGkiBUQ29kZSBYIEYgYyBHIEoNCiBhcHAgOiB7RyBIIDogRkNvZGV9IHtBIDog U2V0fSDihpIgVENvZGUgWCBGIGMgRyAoRnVuYyBBIEgpIOKGkiBUQ29kZSBYIEYgYyBHIChDb25z dCBBKSDihpIgVENvZGUgWCBGIGMgRyBIDQogbGFtIDoge0cgSCA6IEZDb2RlfSB7QSA6IFNldH0g 4oaSIFRDb2RlIFggRiBjIChQcm9kIEcgKENvbnN0IEEpKSBIIOKGkiBUQ29kZSBYIEYgYyBHIChG dW5jIEEgSCkNCg0KVEludGVyIDoge1ggOiBTZXR9IHtGIDogRkNvZGV9IChjIDogRkludGVyIEYg WCDihpIgWCkge0cgSCA6ICBGQ29kZX0g4oaSIFRDb2RlIFggRiBjIEcgSCDihpIgRkludGVyIEcg WCDihpIgRkludGVyIEggWA0KVEludGVyIGMgaWQgeCA9IHgNClRJbnRlciBjIChjb25zdCBhKSBf ID0gYQ0KVEludGVyIGMgKGNvbiB0KSB4ID0gYyAoVEludGVyIGMgdCB4KQ0KVEludGVyIGMgKHBp IHQpIHggd2l0aCBUSW50ZXIgYyB0IHgNCi4uLiAgICAgICAgICAgICAgICAgICAgICAgICAgfCAo dCcgLCBfKSA9IHQnDQpUSW50ZXIgYyAocGknIHQpIHggd2l0aCBUSW50ZXIgYyB0IHgNCi4uLiAg ICAgICAgICAgICAgICAgICAgICAgICAgfCAoXyAsIHQnKSA9IHQnDQpUSW50ZXIgYyAocGFpciB0 IHQnKSB4ID0gKFRJbnRlciBjIHQgeCAsIFRJbnRlciBjIHQnIHgpDQpUSW50ZXIgYyAoayB0KSB4 ID0gaW5sIChUSW50ZXIgYyB0IHgpDQpUSW50ZXIgYyAoaycgdCkgeCA9IGluciAoVEludGVyIGMg dCB4KQ0KVEludGVyIGMgKGNhc2UgdCBmIGcpIHggd2l0aCBUSW50ZXIgYyB0IHgNCi4uLiAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgfCBpbmwgdCcgPSBUSW50ZXIgYyBmICh4ICwg dCcpDQouLi4gICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIHwgaW5yIHQnID0gVElu dGVyIGMgZyAoeCAsIHQnKQ0KVEludGVyIGMgKGFwcCBmIHkpIHggPSAoVEludGVyIGMgZiB4KSAo VEludGVyIGMgeSB4KQ0KVEludGVyIGMgKGxhbSBmKSB4ID0gzrsgeSDihpIgVEludGVyIGMgZiAo eCAsIHkpDQoNClRMaWZ0IDoge1ggOiBTZXR9IHtGIDogRkNvZGV9IChjIDogRkludGVyIEYgWCDi hpIgWCkge1AgOiBYIOKGkiBTZXR9IChQYyA6ICh4IDogRkludGVyIEYgWCkg4oaSIEZMaWZ0IEYg UCB4IOKGkiBQIChjIHgpKSB7RyBIIDogRkNvZGV9ICh0IDogVENvZGUgWCBGIGMgRyBIKSAoeCA6 IEZJbnRlciBHIFgpIChQeCA6IEZMaWZ0IEcgUCB4KSDihpIgRkxpZnQgSCBQIChUSW50ZXIgYyB0 IHgpDQpUTGlmdCBjIFBjIGlkIHggUHggPSBQeA0KVExpZnQgYyBQYyAoY29uc3QgYSkgeCBQeCA9 IGENClRMaWZ0IGMgUGMgKGNvbiB0KSB4IFB4ID0gUGMgKFRJbnRlciBjIHQgeCkgKFRMaWZ0IGMg UGMgdCB4IFB4KQ0KVExpZnQgYyBQYyAocGkgdCkgeCBQeCB3aXRoIFRJbnRlciBjIHQgeCB8IFRM aWZ0IGMgUGMgdCB4IFB4DQouLi4gICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICB8ICh0 JyAsIF8pICAgICAgICAgfCAoUHQnICwgXykgPSBQdCcNClRMaWZ0IGMgUGMgKHBpJyB0KSB4IFB4 IHdpdGggVEludGVyIGMgdCB4IHwgVExpZnQgYyBQYyB0IHggUHgNCi4uLiAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICB8IChfICwgdCcpICAgICAgICAgfCAoXyAsIFB0JykgPSBQdCcN ClRMaWZ0IGMgUGMgKHBhaXIgdCB0JykgeCBQeCA9IChUTGlmdCBjIFBjIHQgeCBQeCAsIFRMaWZ0 IGMgUGMgdCcgeCBQeCkNClRMaWZ0IGMgUGMgKGsgdCkgeCBQeCA9IFRMaWZ0IGMgUGMgdCB4IFB4 DQpUTGlmdCBjIFBjIChrJyB0KSB4IFB4ID0gVExpZnQgYyBQYyB0IHggUHgNClRMaWZ0IGMgUGMg KGNhc2UgdCBmIGcpIHggUHggd2l0aCBUSW50ZXIgYyB0IHggfCBUTGlmdCBjIFBjIHQgeCBQeA0K Li4uICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIHwgaW5sIHQnICAg ICAgICAgICB8IFB0JyA9IFRMaWZ0IGMgUGMgZiAoeCAsIHQnKSAoUHggLCBQdCcpDQouLi4gICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgfCBpbnIgdCcgICAgICAgICAg fCBQdCcgPSBUTGlmdCBjIFBjIGcgKHggLCB0JykgKFB4ICwgUHQnKQ0KVExpZnQgYyBQYyAoYXBw IGYgeSkgeCBQeCA9IFRMaWZ0IGMgUGMgZiB4IFB4IChUSW50ZXIgYyB5IHgpDQpUTGlmdCBjIFBj IChsYW0gZikgeCBQeCA9IM67IHkg4oaSIFRMaWZ0IGMgUGMgZiAoeCAsIHkpIChQeCAsIHkpDQoN CnBvc3R1bGF0ZSBFeHQgOiAoQSA6IFNldCkgKEIgOiBBIOKGkiBTZXQpIChmIGcgOiAoeCA6IEEp IOKGkiBCIHgpIOKGkiAoKHggOiBBKSDihpIgZiB4IOKJoSBnIHgpIOKGkiBmIOKJoSBnIA0KcG9z dHVsYXRlIEV4dC1pbnYtaGFwcGx5IDogKEEgOiBfKSAoQiA6IF8pIChmIDogXykg4oaSIEV4dCBB IEIgZiBmICjOuyBfIOKGkiByZWZsKSDiiaEgcmVmbA0Key0jIFJFV1JJVEUgRXh0LWludi1oYXBw bHkgIy19DQoNCmNvZXJjZS1lcSA6IHtYIDogU2V0fSB7RiA6IEZDb2RlfSAoYyA6IEZJbnRlciBG IFgg4oaSIFgpIHtQIDogWCDihpIgU2V0fSAoZiA6ICh4IDogWCkg4oaSIFAgeCkgKFBjIDogKHgg OiBGSW50ZXIgRiBYKSDihpIgRkxpZnQgRiBQIHgg4oaSIFAgKGMgeCkpIChmYyA6ICh4IDogRklu dGVyIEYgWCkg4oaSIGYgKGMgeCkg4omhIFBjIHggKGFsbCBGIGYgeCkpIHtHIEggOiBGQ29kZX0g KHQgOiBUQ29kZSBYIEYgYyBHIEgpICh4IDogRkludGVyIEcgWCkg4oaSIFRMaWZ0IGMgUGMgdCB4 IChhbGwgRyBmIHgpIOKJoSBhbGwgSCBmIChUSW50ZXIgYyB0IHgpDQpjb2VyY2UtZXEgYyBmIFBj IGZjIGlkIHggPSByZWZsDQpjb2VyY2UtZXEgYyBmIFBjIGZjIChjb25zdCBhKSB4ID0gcmVmbA0K Y29lcmNlLWVxIGMgZiBQYyBmYyAoY29uIHQpIHggcmV3cml0ZSBmYyAoVEludGVyIGMgdCB4KSB8 IGNvZXJjZS1lcSBjIGYgUGMgZmMgdCB4ID0gcmVmbA0KY29lcmNlLWVxIGMgZiBQYyBmYyAocGkg dCkgeCByZXdyaXRlIGNvZXJjZS1lcSBjIGYgUGMgZmMgdCB4IHdpdGggVEludGVyIGMgdCB4DQou Li4gICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICB8ICh0JyAsIF8pID0gcmVmbA0KY29l cmNlLWVxIGMgZiBQYyBmYyAocGknIHQpIHggcmV3cml0ZSBjb2VyY2UtZXEgYyBmIFBjIGZjIHQg eCB3aXRoIFRJbnRlciBjIHQgeA0KLi4uICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg IHwgKF8gLCB0JykgPSByZWZsDQpjb2VyY2UtZXEgYyBmIFBjIGZjIChwYWlyIHQgdCcpIHggcmV3 cml0ZSBjb2VyY2UtZXEgYyBmIFBjIGZjIHQgeCB8IGNvZXJjZS1lcSBjIGYgUGMgZmMgdCcgeCA9 IHJlZmwNCmNvZXJjZS1lcSBjIGYgUGMgZmMgKGsgdCkgeCByZXdyaXRlIGNvZXJjZS1lcSBjIGYg UGMgZmMgdCB4ID0gcmVmbA0KY29lcmNlLWVxIGMgZiBQYyBmYyAoaycgdCkgeCByZXdyaXRlIGNv ZXJjZS1lcSBjIGYgUGMgZmMgdCB4ID0gcmVmbA0KY29lcmNlLWVxIGMgZiBQYyBmYyAoY2FzZSB0 IGYnIGcpIHggcmV3cml0ZSBjb2VyY2UtZXEgYyBmIFBjIGZjIHQgeCB3aXRoIFRJbnRlciBjIHQg eA0KLi4uICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICB8IGlubCB0 JyByZXdyaXRlIGNvZXJjZS1lcSBjIGYgUGMgZmMgZicgKHggLCB0JykgPSByZWZsDQouLi4gICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIHwgaW5yIHQnIHJld3JpdGUg Y29lcmNlLWVxIGMgZiBQYyBmYyBnICh4ICwgdCcpID0gcmVmbA0KY29lcmNlLWVxIGMgZiBQYyBm YyAoYXBwIGYnIHkpIHggcmV3cml0ZSBjb2VyY2UtZXEgYyBmIFBjIGZjIGYnIHggPSByZWZsDQpj b2VyY2UtZXEgYyBmIFBjIGZjIChsYW0gZicpIHggPSBFeHQgXyBfIF8gXyAozrsgeSDihpIgY29l cmNlLWVxIGMgZiBQYyBmYyBmJyAoeCAsIHkpKQ0KDQp0cmFuc3AgOiB7WCA6IFNldH0gKFAgOiBY IOKGkiBTZXQpIHt4IHkgOiBYfSDihpIgeCDiiaEgeSDihpIgUCB4IOKGkiBQIHkNCnRyYW5zcCBQ IHJlZmwgUHggPSBQeA0KDQpfLF89W19dPV8gOiB7WCA6IFNldH0gKFAgOiBYIOKGkiBTZXQpIHt4 IHkgOiBYfSDihpIgUCB4IOKGkiB4IOKJoSB5IOKGkiBQIHkg4oaSIFNldA0KUCAsIFB4ID1bIHAg XT0gUHkgPSB0cmFuc3AgUCBwIFB4IOKJoSBQeQ0KDQphcCA6IHtYIDogU2V0fSB7UCA6IFgg4oaS IFNldH0gKGYgOiAoeCA6IFgpIOKGkiBQIHgpIHt4IHkgOiBYfSAocCA6IHgg4omhIHkpIOKGkiBQ ICwgZiB4ID1bIHAgXT0gZiB5DQphcCBmIHJlZmwgPSByZWZsDQoNCmNvZXJjZSA6IHtYIDogU2V0 fSB7RiA6IEZDb2RlfSAoYyA6IEZJbnRlciBGIFgg4oaSIFgpIHtQIDogWCDihpIgU2V0fSAoZiA6 ICh4IDogWCkg4oaSIFAgeCkgKFBjIDogKHggOiBGSW50ZXIgRiBYKSDihpIgRkxpZnQgRiBQIHgg 4oaSIFAgKGMgeCkpIChmYyA6ICh4IDogRkludGVyIEYgWCkg4oaSIGYgKGMgeCkg4omhIFBjIHgg KGFsbCBGIGYgeCkpIHtHIDogRkNvZGV9IChyIHQgOiBUQ29kZSBYIEYgYyBHIElkKSAoZSA6ICh4 IDogRkludGVyIEcgWCkg4oaSIFRJbnRlciBjIHIgeCDiiaEgVEludGVyIGMgdCB4KSAoeCA6IEZJ bnRlciBHIFgpIOKGkiBQICwgVExpZnQgYyBQYyByIHggKGFsbCBHIGYgeCkgPVsgZSB4IF09IFRM aWZ0IGMgUGMgdCB4IChhbGwgRyBmIHgpIOKGkiBQICwgZiAoVEludGVyIGMgciB4KSA9WyBlIHgg XT0gZiAoVEludGVyIGMgdCB4KQ0KY29lcmNlIGMgZiBQYyBmYyByIHQgZSB4IGggcmV3cml0ZSBj b2VyY2UtZXEgYyBmIFBjIGZjIHIgeCB8IGNvZXJjZS1lcSBjIGYgUGMgZmMgdCB4ID0gaA0KDQpw b3N0dWxhdGUgTXUxIDogKEYgRyA6IEZDb2RlKSAociB0IDogKFggOiBTZXQpIChjIDogRkludGVy IEYgWCDihpIgWCkg4oaSIFRDb2RlIFggRiBjIEcgSWQpIOKGkiBTZXQNCnBvc3R1bGF0ZSBjIDog KEYgRyA6IF8pIChyIHQgOiBfKSDihpIgRkludGVyIEYgKE11MSBGIEcgciB0KSDihpIgTXUxIEYg RyByIHQNCnBvc3R1bGF0ZSBlIDogKEYgRyA6IF8pIChyIHQgOiBfKSAoeCA6IEZJbnRlciBHIChN dTEgRiBHIHIgdCkpIOKGkiBUSW50ZXIgKGMgRiBHIHIgdCkgKHIgXyBfKSB4IOKJoSBUSW50ZXIg KGMgRiBHIHIgdCkgKHQgXyBfKSB4DQoNCnBvc3R1bGF0ZSBNdTEtaW5kIDogKEYgRyA6IF8pIChy IHQgOiBfKSAoUCA6IE11MSBGIEcgciB0IOKGkiBTZXQpIChQYyA6ICh4IDogRkludGVyIEYgKE11 MSBGIEcgciB0KSkg4oaSIEZMaWZ0IEYgUCB4IOKGkiBQIChjIF8gXyBfIF8geCkpIChQZSA6ICh4 IDogRkludGVyIEcgKE11MSBGIEcgciB0KSkgKFB4IDogRkxpZnQgRyBQIHgpIOKGkiBQICwgVExp ZnQgKGMgXyBfIF8gXykgUGMgKHIgXyBfKSB4IFB4ICA9WyBlIF8gXyBfIF8geCBdPSBUTGlmdCAo YyBfIF8gXyBfKSBQYyAodCBfIF8pIHggUHgpICh4IDogTXUxIEYgRyByIHQpIOKGkiBQIHgNCnBv c3R1bGF0ZSBNdTEtaW5kLWMgOiAoRiBHIDogXykgKHIgdCA6IF8pIChQIDogXykgKFBjIDogXykg KFBlIDogXykgKHggOiBfKSDihpIgTXUxLWluZCBGIEcgciB0IFAgUGMgUGUgKGMgXyBfIF8gXyB4 KSDiiaEgUGMgeCAoYWxsIEYgKE11MS1pbmQgRiBHIHIgdCBQIFBjIFBlKSB4KQ0Key0jIFJFV1JJ VEUgTXUxLWluZC1jICMtfQ0KcG9zdHVsYXRlIE11MS1pbmQtZSA6IChGIEcgOiBfKSAociB0IDog XykgKFAgOiBfKSAoUGMgOiBfKSAoUGUgOiBfKSAoeCA6IF8pIOKGkiBhcCAoTXUxLWluZCBGIEcg ciB0IFAgUGMgUGUpIChlIF8gXyBfIF8geCkg4omhIGNvZXJjZSAoYyBfIF8gXyBfKSAoTXUxLWlu ZCBGIEcgciB0IFAgUGMgUGUpIFBjICjOuyB4IOKGkiByZWZsKSAociBfIF8pICh0ICBfIF8pIChl IF8gXyBfIF8pIHggKFBlIHggKGFsbCBHIChNdTEtaW5kIEYgRyByIHQgUCBQYyBQZSkgeCkpDQp7 LSMgUkVXUklURSBNdTEtaW5kLWUgIy19DQo= ------=_Part_1040_367336794.1534627853175 Content-Type: application/octet-stream; name=Mu1.v Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=Mu1.v X-Attachment-Id: b5c5f63e-c9ba-4fdc-85f7-36fc5d21232d Content-ID: Open Scope type. Inductive FCode := |Id : FCode |Const : Type -> FCode |Sum : FCode -> FCode -> FCode |Prod : FCode -> FCode -> FCode |Func : Type -> FCode -> FCode. Definition FInter (F : FCode) (X : Type) : Type. induction F. exact X. exact T. exact (IHF1 + IHF2). exact (IHF1 * IHF2). exact (T -> IHF). Defined. Definition FLift {X} (F : FCode) (P : X -> Type) (x : FInter F X) : Type. induction F. exact (P x). exact T. destruct x. exact (IHF1 f). exact (IHF2 f). destruct x. exact (IHF1 f * IHF2 f0). exact (forall y, IHF (x y)). Defined. Definition all {X} (F : FCode) {P} (f : forall x : X, P x) x : FLift F P x. induction F. apply f. exact x. destruct x. apply IHF1. apply IHF2. destruct x. split. apply IHF1. apply IHF2. intro y. apply IHF. Defined. Inductive TCode {X F} (c : FInter F X -> X) : FCode -> FCode -> Type := |id : forall {G}, TCode c G G |const : forall {G A}, A -> TCode c G (Const A) |con : forall {G}, TCode c G F -> TCode c G Id |pi : forall {G H I}, TCode c G (Prod H I) -> TCode c G H |pi' : forall {G H I}, TCode c G (Prod H I) -> TCode c G I |pair : forall {G H I}, TCode c G H -> TCode c G I -> TCode c G (Prod H I) |k : forall {G H I}, TCode c G H -> TCode c G (Sum H I) |k' : forall {G H I}, TCode c G I -> TCode c G (Sum H I) |case : forall {G H I J}, TCode c G (Sum H I) -> TCode c (Prod G H) J -> TCode c (Prod G I) J -> TCode c G J |app : forall {G H A}, TCode c G (Func A H) -> TCode c G (Const A) -> TCode c G H |lam : forall {G H A}, TCode c (Prod G (Const A)) H -> TCode c G (Func A H). Definition TInter {X F} (c : FInter F X -> X) {G H} (r : TCode c G H) (x : FInter G X) : FInter H X. induction r. exact x. exact a. apply c. apply IHr. exact x. destruct (IHr x). exact f. destruct (IHr x). exact f0. split. apply IHr1. exact x. apply IHr2. exact x. left. apply IHr. exact x. right. apply IHr. exact x. destruct (IHr1 x). apply IHr2. split. exact x. exact f. apply IHr3. split. exact x. exact f. apply (IHr1 x). exact (IHr2 x). intro y. apply IHr. split. exact x. exact y. Defined. Definition TLift {X F} (c : FInter F X -> X) {P} (Pc : forall x, FLift F P x -> P (c x)) {G H} (r : TCode c G H) x (Px : FLift G P x) : FLift H P (TInter c r x). induction r. exact Px. exact a. apply Pc. apply IHr. exact Px. assert (FLift (Prod H I) P (TInter c r x)). apply IHr. exact Px. simpl. destruct (TInter c r x). destruct X0. exact f1. assert (FLift (Prod H I) P (TInter c r x)). apply IHr. apply Px. simpl. destruct (TInter c r x). destruct X0. exact f2. split. apply IHr1. exact Px. apply IHr2. exact Px. apply IHr. exact Px. apply IHr. exact Px. assert (FLift (Sum H I) P (TInter c r1 x)). apply IHr1. exact Px. simpl. destruct (TInter c r1 x). apply IHr2. split. exact Px. exact X0. apply IHr3. split. exact Px. exact X0. apply IHr1. exact Px. intro y. apply IHr. split. exact Px. exact y. Defined. Axiom Ext : forall A B (f g : forall x : A, B x), (forall x, f x = g x) -> f = g. Definition coerce_eq {X F} (c : FInter F X -> X) {P} (f : forall x : X, P x) (Pc : forall x, FLift F P x -> P (c x)) (fc : forall x, f (c x) = Pc x (all F f x)) {G H} (r : TCode c G H) x : TLift c Pc r x (all G f x) = all H f (TInter c r x). induction r. reflexivity. reflexivity. simpl. rewrite fc. rewrite IHr. reflexivity. simpl. rewrite IHr. simpl. destruct (TInter c r x). reflexivity. simpl. rewrite IHr. simpl. destruct (TInter c r x). reflexivity. simpl. rewrite IHr1. rewrite IHr2. reflexivity. simpl. rewrite IHr. reflexivity. simpl. rewrite IHr. reflexivity. simpl. rewrite IHr1. simpl. destruct (TInter c r1 x). simpl. rewrite IHr2. reflexivity. simpl. rewrite IHr3. reflexivity. simpl. rewrite IHr1. reflexivity. simpl. apply Ext;intros. rewrite IHr. reflexivity. Defined. Axiom Ext_inv_happly : forall A B f, Ext A B f f (fun _ => eq_refl) = eq_refl. Definition transp {X P} {x y : X} (p : x = y) (Px : P x) : P y := match p with |eq_refl => Px end. Definition depeq {X P} {x y : X} (p : x = y) (px : P x) (py : P y) := transp p px = py. Notation "px =[ p ]= py" := (depeq p px py) (at level 50). Definition ap {X P} (f : forall x : X, P x) {x y} (p : x = y) : f x =[p]= f y := match p with |eq_refl => eq_refl end. Definition coerce {X F} (c : FInter F X -> X) {P} (f : forall x : X, P x) (Pc : forall x, FLift F P x -> P (c x)) (fc : forall x, f (c x) = Pc x (all F f x)) {G} (r t : TCode c G Id) (e : forall x, TInter c r x = TInter c t x) x : TLift c Pc r x (all G f x) =[e x]= TLift c Pc t x (all G f x) -> f (TInter c r x) =[e x]= f (TInter c t x). rewrite coerce_eq. rewrite coerce_eq. simpl. intros;assumption. exact fc. exact fc. Defined. Axiom Mu1 : forall (F G : FCode) (r t : forall {X} {c : FInter F X -> X}, TCode c G Id), Type. Axiom c : forall F G r t, FInter F (Mu1 F G r t) -> Mu1 F G r t. Axiom e : forall F G r t (x : FInter G (Mu1 F G r t)), TInter (c _ _ _ _) (r _ _) x = TInter (c _ _ _ _) (t _ _) x. Axiom Mu1_ind : forall F G r t (P : Mu1 F G r t -> Type) (Pc : forall x, FLift F P x -> P (c _ _ _ _ x)) (Pe : forall x (Px : FLift G P x), TLift (c _ _ _ _) Pc (r _ _) x Px =[e _ _ _ _ x]= TLift (c _ _ _ _) Pc (t _ _) x Px) x, P x. Axiom Mu1_ind_c : forall F G r t P Pc Pe x, Mu1_ind F G r t P Pc Pe (c _ _ _ _ x) = Pc x (all F (Mu1_ind F G r t P Pc Pe) x). Axiom Mu1_ind_e : forall F G r t P Pc Pe x, ap (Mu1_ind F G r t P Pc Pe) (e _ _ _ _ x) = coerce (c _ _ _ _) (Mu1_ind F G r t P Pc Pe) Pc (Mu1_ind_c F G r t P Pc Pe) (r _ _) (t _ _) (e _ _ _ _) x (Pe x (all G (Mu1_ind F G r t P Pc Pe) x)). ------=_Part_1040_367336794.1534627853175--