From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCRPTME774CRBAXH57NQKGQE6N5GCIY@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-x23e.google.com (mail-oi0-x23e.google.com [IPv6:2607:f8b0:4003:c06::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 710217eb for ; Tue, 21 Aug 2018 11:12:04 +0000 (UTC) Received: by mail-oi0-x23e.google.com with SMTP id e23-v6sf16963967oii.10 for ; Tue, 21 Aug 2018 04:12:04 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=KkdFIB+MU4EGdxYMJlDwIl5zmL9/PSkrgg+bd4XJlec=; b=oBN/Jiendp/SxwsRlESp2zelqTW9LhSvpi0UmB1R0fwm4zfvPoATfzCZT4bSfA8d4u b9lZI8sYBbAphyYiNIr/Lyo62zfER3YJ/mVayj4EbbZitCH7t8LPsNUnSpCOJgeQ1t13 lOOp/DkPjaggB1bxvWfUHapJ7wjrwlgncAPm6QSAyrd7tpQ+59Ua3mOpiXDGwUcxdqnS 0X5PKNfT3n8FqVDMnjWCNKzEqGrdwlkg1bhOd4aldTxbPsrig/fAPEUhloffZ0RKSgNi 25CvTMjBN5KmJGyRiHW08vmP9vFbZaF4Ao4KJLHgBQCcdCZ+0ojmszcx7J4qgwuWep5O 0aJw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=KkdFIB+MU4EGdxYMJlDwIl5zmL9/PSkrgg+bd4XJlec=; b=c0EqTqBaodjqKTLJ45wASwtpuBEwh/NMm4HVJFomzaKEueLmakrYiyJ5hYdhpEcir0 eojs1cnmQo7kwAbjNUPxHTWD0B4fhi0lLPcTxA3lLvGEyiSGLf0lUZ00ADp8YUMKVJzI IGIivzktUe49718nkKYSIjRbT2F65R/OUSWJVUPd7mSEMg7PO45WE4jBC+2uxevUqkRL 72gd8O1pQfu0EU6LDiYADbbiJi/+qQOlzuRFzZt4McAoMhWiFFxJ8rAsudCHQXpiu3wL DVel9u2bTKToFCgyUUKys4sYI0gaMWNlEubdKkFvuu+K14nicONd8VdLYMarCzssX2yZ eoeQ== 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:in-reply-to :references: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=KkdFIB+MU4EGdxYMJlDwIl5zmL9/PSkrgg+bd4XJlec=; b=I9Cc+tPDRgvstyJZcWV21m/UdpNtw3yWZUi3jkWe4c/n2kf1SL15lFfTcGaAzFgavB 4YI3ekuvaQrEhbw1vc5rEP1PZVG6CVtjQRmiUiWzJ6wwEgP72kkBdkkGGEfD6QQA1dEk hLws1f354r/xW7dYsW2IZjYlRNljlMCeup1Mo+4ILw4ptOJo4DoT2Bmb44l5sK9vhfyQ 3d2aEIr9ga8TdY/c2C4HG0obcXsDMgVyBtminbTJpcJhrLjmkLAy+oMeF63aR6CJfWdt m7nWzyyA8b0HaPIzkT//ZR8vX9VvXOGpc0S4b4ZhOtdo/s4O2cf91Am+5IUzhPal3NyC CeXg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFqgL1UE/8/VOBl8597Xj6NB4ZqhLGDcbnHJpl9Z2t0+ed7b7eq NAgeSL0bSvegYxn7OqU8gB0= X-Google-Smtp-Source: AA+uWPycC/c2v31J/o2+ScDBQETwkWc3kLzdtFUmSY/4JBLHu+QvJ2z9aYVwR+w5zdARh8SEog7XjA== X-Received: by 2002:aca:75c9:: with SMTP id q192-v6mr1096898oic.3.1534849922510; Tue, 21 Aug 2018 04:12:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:c6c4:: with SMTP id w187-v6ls4678213oif.3.gmail; Tue, 21 Aug 2018 04:12:02 -0700 (PDT) X-Received: by 2002:aca:af15:: with SMTP id y21-v6mr47024oie.6.1534849921975; Tue, 21 Aug 2018 04:12:01 -0700 (PDT) Date: Tue, 21 Aug 2018 04:12:01 -0700 (PDT) From: Niels van der Weide To: Homotopy Type Theory Message-Id: In-Reply-To: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com> References: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com> Subject: [HoTT] Re: 1D Mu Type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1792_1546997684.1534849921330" X-Original-Sender: nnmvdw@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_1792_1546997684.1534849921330 Content-Type: multipart/alternative; boundary="----=_Part_1793_396209963.1534849921330" ------=_Part_1793_396209963.1534849921330 Content-Type: text/plain; charset="UTF-8" Looks interesting! > 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. I think this is might be a special case of the work by Kaposi/Kovacs on HIITs. See http://drops.dagstuhl.de/opus/volltexte/2018/9190/pdf/LIPIcs-FSCD-2018-20.pdf They gave a syntax allowing both higher paths and function types. 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. In addition, see the paper 'Quotient Inductive Inductive Types' by Altenkrich, Capriotti, Dijkstra, Kraus and Forsberg. Not all HITs are constructible as quotients, because that would require AC. This is because function types are added to the syntax. Section 9.1 in Lumsdaine&Shulman's Semantics of Higher Inductive Types also gives a counter example. Again note that they use a function type in the constructor sup. On Saturday, August 18, 2018 at 11:30:53 PM UTC+2, Corlin Fardal wrote: > > 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_1793_396209963.1534849921330 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Looks interesting!
=C2=A0
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 path constr= uctors 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.
I think this is might be a = special case of the work by Kaposi/Kovacs on HIITs. See
http://drops.da= gstuhl.de/opus/volltexte/2018/9190/pdf/LIPIcs-FSCD-2018-20.pdf
They gave= a syntax allowing both higher paths and function types.

Another next step would be seeing if we can = define this type through some clever use of quotient types, perhaps in a si= milar way to the construction of propositional truncation.
In addition, see the paper 'Quotient Inductive Inductive Types' by= Altenkrich, Capriotti, Dijkstra, Kraus and Forsberg. Not all HITs are cons= tructible as quotients, because that would require AC. This is because func= tion types are added to the syntax. Section 9.1 in Lumsdaine&Shulman= 9;s Semantics of Higher Inductive Types also gives a counter example. Again= note that they use a function type in the constructor sup.

O= n Saturday, August 18, 2018 at 11:30:53 PM UTC+2, Corlin Fardal wrote:
I've managed t= o create a 1D Mu Type, essentially just a basis for creating any recursive = higher inductive type with point and path constructors one could define. Th= e 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 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 te= rm for the function types. To be able to deal with the new terms, the const= ruction 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 f= unction, 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 po= st.

With this type we have a starting point for many nex= t steps, including exploring the semantics of this new type, including show= ing that it gives rise to a cell monad, and showing homotopy initiality. An= other next step would be seeing if we can define this type through some cle= ver use of quotient types, perhaps in a similar way to the construction of = propositional truncation.

I didn't write a pap= er about this, largely because it is just a fairly straight forward extensi= on of an existing paper, and also because I'm not a terribly good write= r, but I hope that this post suffices in sharing what little I've manag= ed to accomplish. I also hope that this post doesn't seem too out of th= e 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 r= ead a good few things on here already, and from what I can tell, this doesn= 't seem too strange.

I checked various cases o= f HITs with my Mu type, and while the various constructors and induction ru= les seem to align with my intuition for what they should be, I don't ac= tually know of anywhere where the induction rules for various kinds of indu= ctive 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 &= 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_1793_396209963.1534849921330-- ------=_Part_1792_1546997684.1534849921330--