From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDTLDGMZRMJBBOUC6PNQKGQEUADJACY@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 9ef82a12 for ; Wed, 22 Aug 2018 01:49:48 +0000 (UTC) Received: by mail-oi0-x240.google.com with SMTP id l14-v6sf469262oii.9 for ; Tue, 21 Aug 2018 18:49:48 -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=gD99CG7qvMOTsG4z7cc3PdBM7lU3jxQyvUFnRqsTRcs=; b=CBnwiU2viX5Y/8UkCpRpv3ldWYJe33w9Z8Q+dBvzp+6XdAoVeGKjc82iNZRY0XenCr XPSjOZ9RpUcpFFeaxB6QMhIM9ECBV/AJZCQBEDgUhvnb68Q/ChpJjDVA1cCJtWOz8AzY 1N3tSLEzoaBhISD/3PTUlbWp9VSucX0WK2IslMVPCUN8luepzXFE5Oed6XAQo+TQwldF a0hBxkortvGSPqkRIAGJ8o41M5OKytkihTewk+/GJFAuhlNtINc/iVIIzZCumdDz59kP OoWux7B1Np6Td8BNlDkMBEc0Tzdw3djNjkb4xFuqc6S1LIMV/f+4givLiRmcdvh6C7g6 Bcsw== 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=gD99CG7qvMOTsG4z7cc3PdBM7lU3jxQyvUFnRqsTRcs=; b=gcQ1o/yKqx83RX4Y91Bq4GTu+y77tHg6IoUBXDnF3ZHhrlEjv0B6pHeGzmR2kqTBRV HDRG+cJEGTElFxi3K4zCivB3zG/OzzWDKni7XJ0L35b1HSP0yx9UC+2HL5QN8C63d7Jg mYA/HhjDEaReppQa7Yty814v1O6mzyru+e0aQRYhxS90zdwt6s71T79Ax5NLbO3e43iM P1WsnvFLCzjHETBo6TPI5k64XxC09ctGwfTgFakd1cwSUiscRg9St3RmKm8mT4COnAp/ EgXvwEDnQG0CgShRI2JgF9sDyg4JwCKgU0WoENbDrQ5LgiqLdCaZ4PQ106Ld4KhxOOiM IkHA== 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=gD99CG7qvMOTsG4z7cc3PdBM7lU3jxQyvUFnRqsTRcs=; b=gneTb9FlGOsdR7Hc81DXjLJxTzfN40RurxubKi68eq2Rkb7+dpX8LkQbk52M4+aZoy 8xkJqNiRsd0ey0sdRbflxHr2ggtUjPJKVE1O+T5os4owvCixe10lSk77h3ssUENRhLZY ksvmaBjgbj9ECqoQOvvORjTkuRuL07kaS7MF13uuDn94h5NO5VKOLY3M4arTYj2pZ0gT 1pyVj0BqNhll97xSGiMVxmPUAFcrOCGW4jJlFck2ND0+75R1DuoYcbZ1D7EnUqkHVL2p tQj+nm5q4GkkR2R6w6WlhKVV48O76v07Y9gMMHCGw4AwujZE6V2khNoY0BSOvOivCFwf BK+A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlHG/jTYm2FIxuJz5knSxDPqZuPCRCj+mUtdZjEwic8sXbKfaxsO Z1aOt8xnPkUPt1rjW43Or9I= X-Google-Smtp-Source: AA+uWPwcbIqpYeJIhRvdoLIUsuN5F06N5YgCG9QeUSKcTG8L7JhgskJQShGYobu8hzfBWRWAYps1RQ== X-Received: by 2002:aca:f495:: with SMTP id s143-v6mr1166781oih.7.1534902586855; Tue, 21 Aug 2018 18:49:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1702:: with SMTP id j2-v6ls5670289oii.8.gmail; Tue, 21 Aug 2018 18:49:46 -0700 (PDT) X-Received: by 2002:aca:c68d:: with SMTP id w135-v6mr15419oif.4.1534902586301; Tue, 21 Aug 2018 18:49:46 -0700 (PDT) Date: Tue, 21 Aug 2018 18:49:45 -0700 (PDT) From: Corlin Fardal 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_2126_387763111.1534902585670" 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_2126_387763111.1534902585670 Content-Type: multipart/alternative; boundary="----=_Part_2127_698525319.1534902585670" ------=_Part_2127_698525319.1534902585670 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I=E2=80=99m pretty sure I had actually read the HIITs paper before, but I= =E2=80=99d=20 completely forgotten about it. Reading back through it it=E2=80=99s kind of= amazing=20 that I had, considering how much it manages to do very simply. I=E2=80=99d = also=20 read the QIITs paper, but, like I did with the IITs paper, gotten lost in= =20 the category-theoretical brushes, and ended up missing the fact that a=20 quotient construction would require AC, though I'm not entirely surprised= =20 by that, I kind of figured it might. I did further know about the=20 construction by Lumsdaine and Shulman, but I wasn't entirely certain if=20 that applied to my construction, it's been a while since I've read that=20 section of the paper, but as far as I can recall they didn't provide the=20 actual definition of the HIT, so while I knew that it would be impossible= =20 to construct any HIT from quotients, I thought that the subset I had=20 created a Mu type for might still be constructible, and not contain their= =20 HIT. I have a few questions/comments about Kov=C3=A1cs' version. First of all, i= s the=20 Empty constructor necessary? It seems like we could replace it with Const= =20 empty, and replace exfalso with a lifted function. Additionally I'm kind of= =20 struggling to understand what the path algebra in the definition of Section= =20 is actually doing, is there a simple explanation? Also, though this doesn't= =20 really matter, why is the path=20 algebra on the left side of the equation, instead of the right? It feels=20 like if they're meant to be computation rules, it should compute from the= =20 left down to the right, and because of that it feels like it ought to go from the simple application of induction to the= =20 path, down to a more complex expression. Additionally, as one last little= =20 nitpick, my name's Fardal not Fardar, as comment at the top of the file says, though that really doesn't matter=20 much. However, despite all of my nitpicks/confusions, I really like your=20 version of it. The reformulation of the=20 lambda term feels obvious but clever, and I'm kind of mad at myself for not= coming=20 up with it, seeing as one of the problems I was having was defining a=20 quotient type in my version. I=20 also like the connection made between the all function and the coerce=20 function, I didn't realize the connection there, as, at the very least, the= =20 two functions needed to finish the=20 computation rules. In general I like the method of building from the=20 algebras to the displayed algebras to the sections, it gives the Mu type at= =20 the end a very nice definition. The names of the sections sound algebraic, but I'm actually not quite sure what they= =20 mean. I mean, I know what an algebra is, I'm relatively well versed in the= =20 categorical semantics of at least simple inductive types, but what are displayed algebras, or displayed=20 algebra sections? Displayed algebras seem to have at least some connection= =20 to the fibred algebras of the Higher Inductive Types as Homotopy-Initial Algebras paper, and I have some idea of= =20 what sections are, but is there anything deeper that I don't know about? Now, if you'll excuse me, I'm going to go mess around with the HIIT paper's= =20 system and Kov=C3=A1c's version of my system to see if I can't understand b= oth=20 of them more, along with HITs in general. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2127_698525319.1534902585670 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I=E2=80=99m pretty sure I had actually read the HIITs paper before,= but I=E2=80=99d completely forgotten about it. Reading back through it it= =E2=80=99s kind of amazing that I had, considering how much it manages to d= o very simply. I=E2=80=99d also read the QIITs paper, but, like I did with = the IITs paper, gotten lost in the category-theoretical brushes, and ended = up missing the fact that a quotient construction would require AC, though I= 'm not entirely surprised by that, I kind of figured it might. I did fu= rther know about the construction by Lumsdaine and Shulman, but I wasn'= t entirely certain if that applied to my construction, it's been a whil= e since I've read that section of the paper, but as far as I can recall= they didn't provide the actual definition of the HIT, so while I knew = that it would be impossible to construct any HIT from quotients, I thought = that the subset I had created a Mu type for might still be constructible, a= nd not contain their HIT.

I have a few questions/comments about Kov=C3=A1cs' version.= First of all, is the Empty constructor necessary? It seems like we could r= eplace it with Const empty, and replace exfalso with a lifted function. Add= itionally I'm kind of=C2=A0
struggling to understand what the path algebr= a in the definition of Section is actually doing, is there a simple explana= tion? Also, though this doesn't really matter, why is the path=C2=A0
alge= bra on=C2=A0= the left side of the equation, instead of the right? It feels like if they&= #39;re meant to be computation rules, it should compute from the left down = to the right, and because of that it
feels like it ought=C2=A0to go from the simple appli= cation of induction to the path, down to a more complex expression. Additio= nally, as one last little nitpick, my name's Fardal not Fardar, as
commen= t at the top of the file says, though that really=C2=A0doesn't=C2=A0matter much. However, despite all of my= nitpicks/confusions, I really like your version of it. The reformulation o= f the=C2=A0
lambda term feels obvious but clever, and I'm kind of mad at = myself for not=C2=A0coming up with it, seeing as one of the problems I was having was d= efining a quotient type in my version.=C2=A0I=C2=A0
also like the connection made between= the all function and the coerce function, I=C2=A0didn't realize the connection the= re, as, at the very least, the two functions needed to finish the=C2=A0
compu= tation rules. In general I like the method of building from the algebras to= the displayed=C2=A0algebras to the sections, it gives the Mu type at the end a very ni= ce definition. The names
of the sections sound algebraic, but I'm actuall= y not quite sure what they mean. I mean, I know what an algebra is, I'm= relatively well versed in the categorical semantics of at least
simple induc= tive types, but what are displayed algebras, or displayed algebra sections?= Displayed algebras seem to have at least some connection to the fibred alg= ebras of the Higher
Inductive Types as Homotopy-Initial Algebras paper, and I= have some idea of what sections are, but is there anything deeper that I d= on't know about?

Now, if you'll excuse me, I'm going to go mes= s around with the HIIT paper's system and Kov=C3=A1c's version of my system = to see if I can't understand both of them more, along with HITs<= /div>
in gen= eral.

--
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_2127_698525319.1534902585670-- ------=_Part_2126_387763111.1534902585670--