From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDTLDGMZRMJBBCMU6PNQKGQEBD2ZZOY@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-x23f.google.com (mail-oi0-x23f.google.com [IPv6:2607:f8b0:4003:c06::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1f166788 for ; Wed, 22 Aug 2018 02:27:23 +0000 (UTC) Received: by mail-oi0-x23f.google.com with SMTP id b8-v6sf540841oib.4 for ; Tue, 21 Aug 2018 19:27:22 -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=cFm2zc+y3p5ntISYl4fiiWJSupr8OTj1qwZEpgf0LCA=; b=WVrxxF6rf8EApcwR7+7aqSQDOJAvNP6rnFpHxisyE4gegNzEfTT09CEA2Pm7BvAlIN JByawFBtJU4WZ6ugcsxZ+Z3AVHXMc3DpG6/dVEYVIYUgqUNr3WBT8A95vsbQapChRVJX AZUhtpiA5paMIatQyUQMLWs9tDLx16hx4LE8c+mFfajuRMX5J3iHRoze3rJY71Wg/6SC twv/Bbxp016EQbnBfDKSdLuBpa5u6TaFFcvi+4npIgrXvjL7XC1uQ3/Zd+3NWtXhCoBL 5Am1NdYjx2p62mK9RLi7EZVknupIs9NndUo0104opjcLyhaLZGI0QlWuNTcDuRrhrLr5 7qdw== 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=cFm2zc+y3p5ntISYl4fiiWJSupr8OTj1qwZEpgf0LCA=; b=pGMo0a/UXn1k9KJoPvB5D4P8HYFcWoj4CG3WMQfM3h6J1bYxneXpQACO2eLFWvRpBv JB5Fm7GCRQ/+27KVoIU124k90f9qWXI0kQV/1UTtyQCY4fji8PKoixnCW5oidd6PHC+/ yTRU4d8ls825RVAxjcirmdNNm2wuWUhYZMyqhA61M/za9xQhegIR9bVRp7cC4n5FKsJV bGF9yGPbg2Xn8oDbkKQQ0ksKpniKG+/AvT+QIhy2TsbzO/a3oQv66hoUGe1yGCurOjWO UHUVJjxx4iPo/pHi8Xy00su/2PRmX5H8TO3gMstHfp1yRi1nh+hGUWS8kQMQ6MPi9Pau YgrQ== 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=cFm2zc+y3p5ntISYl4fiiWJSupr8OTj1qwZEpgf0LCA=; b=e15nxhA/52sKHvCrMxvrM1avk40GbxAijREYCVOM8jhEnmJSvVn3TRKq7qZ9J/GdOg sbORUOtBIVqZ/Q16CHDodSrz3wdmp/iactlmmn/DEq20PtKljC5NPT1ZMUC/aHbD1zSQ HisgjDLagWUytIZT02jNP2P1PGteXGw+Kx0lzu2JE+sNvQdS30Cp44v/o4QA0PVxTCf4 uZhTyuxmH4YAUtV4XAvLtOO45BvxviUt8M6S0TqYnujDEJ8RQhtJFPnUHyLMcUWpkwaa 9qIriFYfengLFp/TnAplGIRgekaaLtozy9kl+bGxpG5CkdSXLuZb2YDscRCvr7sG4WLp X3jw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlEK0Pf7YgwA08qyweO70rSmt2T4EqPxvcTlA3TJILxv95ichQz0 zzw2ZybX8Z11LMG3a2D87N4= X-Google-Smtp-Source: AA+uWPx0pVC7NKAqc3XZH9zxu6GHx3/DIniYJAyHcSRyVzrbYHRi4VTHAhSD+IjMCOnqseZlvsTm7g== X-Received: by 2002:aca:2b06:: with SMTP id i6-v6mr1189619oik.0.1534904841988; Tue, 21 Aug 2018 19:27:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:8d0:: with SMTP id 199-v6ls13705oii.9.gmail; Tue, 21 Aug 2018 19:27:21 -0700 (PDT) X-Received: by 2002:aca:2b06:: with SMTP id i6-v6mr1189618oik.0.1534904841511; Tue, 21 Aug 2018 19:27:21 -0700 (PDT) Date: Tue, 21 Aug 2018 19:27:20 -0700 (PDT) From: Corlin Fardal To: Homotopy Type Theory Message-Id: <62705675-c00d-4b36-a06b-09f066a0a42a@googlegroups.com> 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_2113_453833017.1534904840984" 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_2113_453833017.1534904840984 Content-Type: multipart/alternative; boundary="----=_Part_2114_2124866204.1534904840984" ------=_Part_2114_2124866204.1534904840984 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 the computation rules essentially define induction, so it feels like= =20 the left side should say "this is the application of the function," and the right should say "this is the value of that=20 application". Additionally, as one last little nitpick, my name's Fardal=20 not Fardar, as thecomment at the top of the file=20 says, though that really doesn't matter much. However, despite all of my=20 nitpicks/confusions, I really like your version of it. The reformulation of= =20 the lambda term feels obvious but=20 clever, and I'm kind of mad at myself for not coming up with it, seeing as= =20 one of the problems I was having was defining a quotient type in my=20 version. I also like the connection made=20 between the all function and the coerce function, I didn't realize the=20 connection there, as, at the very least, the two functions needed to finish= =20 the computation rules. In general I like the method of building from the algebras to the displayed algebras to the=20 sections, it gives the Mu type at the end a very nice definition. The names= of=20 the sections sound algebraic, but I'm actually not quite sure what they mean. I mean, I know what an algebra is,= =20 I'm relatively well versed in the categorical semantics of at least simple= =20 inductive types, but what are=20 displayed algebras, or displayed algebra sections? Displayed algebras seem= =20 to have at least some connection to the fibred algebras of the Higher Induc= tive=20 Types as Homotopy-Initial=20 Algebras paper, and I have some idea of what sections are, but is there=20 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_2114_2124866204.1534904840984 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 the comp= utation rules essentially define induction, so it feels like the left side = should say "this is the application
of the function," and the right= should say "this is the value of that application".=C2=A0Additionally, as on= e last little nitpick, my name's Fardal not Fardar, as thecomment at the top of the= file=C2=A0
says, though that really=C2=A0doesn't=C2=A0matter much. However, despite all of my nitpicks/confu= sions, I really like your version of it. The reformulation of the=C2=A0lambda term feel= s obvious but=C2=A0
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 defining a quotient typ= e in my version.=C2=A0I=C2=A0also like the connection made=C2=A0
between the all function and the coe= rce function, I=C2=A0didn't realize the connection there, as, at the very least, th= e two functions needed to finish the=C2=A0computation 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 nice definition. The names=C2=A0of the sections sound al= gebraic, but I'm
actually not quite sure what they mean. I mean, I know w= hat an algebra is, I'm relatively well versed in the categorical semant= ics of at least=C2=A0simple inductive types, but what are=C2=A0
displayed algebras, or di= splayed algebra sections? Displayed algebras seem to have at least some con= nection to the fibred algebras of the Higher=C2=A0Inductive Types as Homotopy-Initial= =C2=A0
Algebras paper, and I have some idea of what sections are, but is ther= e anything deeper that I don't know about?

Now, if you'll excuse m= e, I'm going to go mess around with the HIIT paper's system and Kov= =C3=A1c&#= 39;s version of my system to see if I can't understand both of them mor= e, along with HITs
in general.

--
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_2114_2124866204.1534904840984-- ------=_Part_2113_453833017.1534904840984--