From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC62R4PNV4PBBQF76XNQKGQELA3NBYI@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.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM,FROM_EXCESS_BASE64, 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-pl0-x23d.google.com (mail-pl0-x23d.google.com [IPv6:2607:f8b0:400e:c01::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e32e8401 for ; Wed, 22 Aug 2018 13:06:11 +0000 (UTC) Received: by mail-pl0-x23d.google.com with SMTP id t4-v6sf984549plo.0 for ; Wed, 22 Aug 2018 06:06:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1534943169; cv=pass; d=google.com; s=arc-20160816; b=EHCJLjElFKyohX7HII6p8n4PnfN0Gits1OV+XkFKRFovjAO5FWM6936DwLx25pZ9Lb R75jmtunYtfpF5HIxSTu5z62+4e02SuFLsw0qcrTdXKKHnggFG4A5HeuqGlpMGVunJTP 4Lhqg8POTh1ZyBJNxFFOlh+6VsX3kQaicdHtxNedjP4hNJOD8+7KmpqkSoFSSkp6Rk+D nPLy1E/Xcl35cExdy5B3mbJ/KH2ZF/fXZsEyPs7LeN/jWDpIOkLF/8xvtY6ZsT5fkMBa aR+s5O6UAtQUXvI6o1MMAtjofMwUS2hokM4zjVYYNVIM5wZNrlP58UHJbNrc898kP+BH dbLA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature:dkim-signature :arc-authentication-results; bh=SSXEGRZBWadTh9uZJKpCK3V6YRH9vAIbN+j+mkdPomQ=; b=W8HbLJuGibM0fYdNuMaaJqHXzLeKRpBxDGJ2rYxuYy6es3vQw8w0BRzYXnAgCNfOUx ZZn2jDL4gUYGCclbT9m06Vs8PJEdtS1ScjmDnXM5En0Fl7QmgoIk1nSe3OwnZkKNRHDw 2XpOOflf7eMyRBHg5YaiGTzJmQqXEErm7VPiPo/2c84NTJcT9E3zCMDG3gRbiI6BLZsR bORVkGWAKx04GGJJzd0w8A6Pdu1wnwazdV3cpo10g7EY997koaYgFf7SdNlDSUWQa8aT i9NBkT2QuJ++jvk/n9tHRhCXnYQsR3NxxWk1pPzyqZehsSkwg6y+e89ux6Oxgm5Gavzh O9aA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=q5kAUYuR; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:400d:c0d::236 as permitted sender) smtp.mailfrom=puttamalac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=SSXEGRZBWadTh9uZJKpCK3V6YRH9vAIbN+j+mkdPomQ=; b=Mukiq9/vUiy5W0ZiP9iGuD8bVi/fNMwcp8y7t2GzmCmR/PL12IGayK7FjW6viclh2B 0nGDgM6q37tR8HiLv/IM57txXeMLAVfTETV0R7XhK/HvK2jzmmqECNC7IlKTgJjb5oH/ Qzfl5k+jKwFneGywYuRYC6PcdfipKMriD6GHB93Bmfn3uARg+vEiByJJjx961qtqaoG9 qq7ZdYxyHvBNY5F3MOQ5ImGAv7qoLUIdSCQkhnxNdDSpFElizaj+OPsKqzs5XJGhLiVK Raq/UIntBhlLKm9Z4y9xWVfXfvLtaMeXp6aqPdgLtglQtuy+hrQmDU/32lMQmF6mxCvp 9jag== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=SSXEGRZBWadTh9uZJKpCK3V6YRH9vAIbN+j+mkdPomQ=; b=geB1d9ypvmzbc3gcA47maor5UUgRYTm/t5v9tW62yFNgLbrYjnIhTMe62/XznHmgaK D6nA3IupHSoFB27yOJ9RvKQ3cYJvKpIGLUDMi6PVz5Sv1kHk610CblB81mhUQsRL0gQQ eQ3CLTRgt3bTgr7TbHikNu6aRsWKtGwNRS3iD2nsg/fKjMnZH8KWy1cVI5B4EEYZUgBo wrTjiqot0cCIpYyJelwIjURA5qDOWHmGuY4oY6BZlZ6ubC8nSZ6+W+wjSNmKQGJ3INMj ieY7pHaupJ3aioyjGQTTKPVqHNFr9+Ga8TVl/YLkyMgN7ow2jTXOetXstGPevpuOK7aD bWIQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=SSXEGRZBWadTh9uZJKpCK3V6YRH9vAIbN+j+mkdPomQ=; b=D22exStYIhxZMiQHQDDxgZKXrHuADadtj2S712TUwEzB5SFxdjkQYpiUJcZhj3rRsp KkoMt8csctg49m9jyhn7OoJCNsPXGLqn4NaaEiY0LMR8jSro/LI2ul7sGbn4bXrRUnJL hjXoHoJF0VqiXm7SOKWjkog/ASb1+OfPordf5cx6kJsI4EiG3sgm34mLQyT1T5S1hgjJ 7p9/k0V4XZYaAAHGfMNkxepLpSmVxlXBIziFzkE9UvjdqwSBaTwfjQ8z2csHdXiNKlYJ mtlkbneP+pgR4McHH55e93DvCOBrV4EhCZ5tA7/SLn0qDcuSUncgw6LGH7bOjGA5tTFj 085Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlHgd5RKxkFB84zPd4dvAFH8h8RzHQ46ZwkO/ImPCTsEHBoM1X8U g5FEweEUYytnNoKHOW3Xczw= X-Google-Smtp-Source: AA+uWPwRVCBgYcZv3GyvWCLUpV9933EU7t8sRxTR3B0OyusZsCusuxWXrxH1UaFEkHUEuARnxWALQw== X-Received: by 2002:a17:902:a718:: with SMTP id w24-v6mr241975plq.2.1534943168360; Wed, 22 Aug 2018 06:06:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:63ce:: with SMTP id n14-v6ls319999pgv.33.gmail; Wed, 22 Aug 2018 06:06:08 -0700 (PDT) X-Received: by 2002:a62:a658:: with SMTP id t85-v6mr12904635pfe.38.1534943168008; Wed, 22 Aug 2018 06:06:08 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1534943167; cv=none; d=google.com; s=arc-20160816; b=hbTx+3Hb64SWCgbfFvdEyCgRpfg99NHmg5+GKB3VJ+2JvCOcfGuyazv2ECRQyOYBHv vLLHZndlUt81dii7NgnnIZsABDI/W4VLXAVtRIUtvl23F1dpBChf/nA0KaecZlttuFMQ ZN8SLVCJgLrj8T+aAg86wcycIWjXLK2RmE9Afjc/euIkbxNT6aQNpyrQE8Nm2rrCAwFn H+ltq9ujLeeaRTfFnWa3dQtrQG+y7sk3/WnCIIcXa94Z0z6iiAgSbhU6AewNeL6dxGp/ pnmg8nEPktYQUSfovFug+rzrGQcV+4D7Rmh9HdGCTFElxYbuol9Yzi26LQSh73iZsptc //Ug== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=PwUkKCeCJfetXcZ3BQ09OpJBBwtbMceUPaLQud4pVrw=; b=UBwXf9j/jj3BbvTELe4dONECwnlFBcvqZSlItS/KQUtnqIji0dd7TSSahcMBfDnNkm R1E3ImXMdx3hm8ywg1+K5MA7GGmi5DP0p34NMMmOujdZIUHSf6yrsY+CZOHVZwqqRzNJ S141fVGHKG9Lyk299TBjy8z14ENlBWTgt0a/60MaqZl5FjE+kPTeyDvQlIETNoxnW9N7 4XlccY7zPPW381hfUwEzeVALEd7gJwqysBH7tmSevKJMFZlXOxFF0pTiCFdLpb4HWEOV wpZie87/RqcbvjQ+qx6A1weMV0ZVhPxsZvpXj5uyOHkAuirDxqXmWds1nq+JjhsGZMOa JSGA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=q5kAUYuR; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:400d:c0d::236 as permitted sender) smtp.mailfrom=puttamalac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qt0-x236.google.com (mail-qt0-x236.google.com. [2607:f8b0:400d:c0d::236]) by gmr-mx.google.com with ESMTPS id e9-v6si49935pfn.3.2018.08.22.06.06.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 22 Aug 2018 06:06:07 -0700 (PDT) Received-SPF: pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:400d:c0d::236 as permitted sender) client-ip=2607:f8b0:400d:c0d::236; Received: by mail-qt0-x236.google.com with SMTP id f19-v6so459111qtf.2 for ; Wed, 22 Aug 2018 06:06:07 -0700 (PDT) X-Received: by 2002:ac8:705a:: with SMTP id y26-v6mr55392968qtm.118.1534943167635; Wed, 22 Aug 2018 06:06:07 -0700 (PDT) MIME-Version: 1.0 References: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com> In-Reply-To: From: =?UTF-8?B?QW5kcsOhcyBLb3bDoWNz?= Date: Wed, 22 Aug 2018 15:05:55 +0200 Message-ID: Subject: Re: [HoTT] Re: 1D Mu Type To: Corlin Fardal Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000041e448057405ce45" X-Original-Sender: puttamalac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=q5kAUYuR; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:400d:c0d::236 as permitted sender) smtp.mailfrom=puttamalac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --00000000000041e448057405ce45 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > my name's Fardal not Fardar Sorry, fixed it. First of all, is the Empty constructor necessary? Fair point, it isn't necessary, I removed it now. what the path algebra in the definition of Section is actually doing, is > there a simple explanation? Also, though this doesn't really matter, why = is > the path > algebra on the left side of the equation, instead of the right? The last component of Section is just the weak (propositional) beta rule for path constructors. If every point computation rule held definitionally, then the path beta would be simply (apd (F=CB=A2 Id X=CB=A2) (paths gx) =E2=89=A1 paths=E1=B4=B0 gx (F=CB=A2 g= X=CB=A2 gx))), which has the form we usually see when people use HITs (with definitional point beta). Since path beta rules are generally only well-typed up to point beta rules, we need to refer to Tm=CB=A2 t and Tm=CB=A2 u to make it well-typed, so the le= ft side is wrapped in an extra composition. It's an arbitrary choice whether to compose with point beta rules on the left side of the equation or the right side, since the two versions are equivalent. The names > of the sections sound algebraic, but I'm actually not quite sure what the= y > mean It follows the terminology we use in the followup draft to the HIIT stuff. In the HIIT paper we used "constructors", "motives/methods" and "eliminators", but the new terminology is much better. I think Mike Shulman previously used the terms "algebra", "dependent algebra", and "dependent algebra section". We use "displayed" instead of "dependent" because displayed algebras generalize Ahrens and Lumsdaine's displayed categories, in a rather precise way. In general, semantics for a inductive types should include constructing a category of algebras for each syntactic declaration, where algebra homomorphisms are the morphisms. However, if we only have a category, we can only talk about initiality (unique recursion), but not about induction, because that needs a notion of dependent object/family/fibration. So we need to have a category with a notion of dependent objects. In the draft paper we use CwF (category with families) where displayed algebras and sections form the "F" part, but there are probably other workable choices as well. Corlin Fardal ezt =C3=ADrta (id=C5=91pont: 2018. a= ug. 22., Sze, 3:49): > 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 do very simply. I=E2=80=99= d 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 further know about the > construction by Lumsdaine and Shulman, but I wasn't entirely certain if > that applied to my construction, it's been a while 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, and 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 replace it with > Const empty, and replace exfalso with a lifted function. Additionally I'm > kind of > struggling to understand what the path algebra in the definition of > Section is actually doing, is there a simple explanation? Also, though th= is > doesn't really matter, why is the path > algebra on the left side of the equation, instead of the right? It feels > like if they'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 to go from the simple application of induction to the > path, down to a more complex expression. Additionally, as one last little > nitpick, my name's Fardal not Fardar, as > comment at the top of the file says, though that really doesn't matter > much. However, despite all of my nitpicks/confusions, I really like your > version of it. The reformulation of the > lambda term feels obvious but clever, and I'm kind of mad at myself for > not coming up with it, seeing as one of the problems I was having was > defining a quotient type in my version. I > also like the connection made between the all function and the coerce > function, I didn't realize the connection there, as, at the very least, > the two functions needed to finish the > computation rules. In general I like the method of building from the > algebras to the displayed algebras to the sections, it gives the Mu type > at the end a very nice definition. The names > of the sections sound algebraic, but I'm actually not quite sure what the= y > mean. I mean, I know what an algebra is, I'm relatively well versed in th= e > categorical semantics of at least > simple inductive types, but what are displayed algebras, or displayed > algebra sections? Displayed algebras seem to have at least some connectio= n > to the fibred algebras 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 don't know abou= t? > > Now, if you'll excuse me, I'm going to go mess 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 > in general. > > -- > 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. > --=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. --00000000000041e448057405ce45 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
my name's Fardal no= t Fardar
=C2=A0
Sorry, fixed it.

First of all, is the = Empty constructor necessary?

= Fair point, it isn't necessary, I removed it now.

<= div>
=C2=A0what the path algebra in the definition of Section is actua= lly doing, is there a simple explanation? Also, though this doesn't rea= lly matter, why is the path=C2=A0
algebra on=C2=A0the left side of the equation, instead of the right?

The last component of Section = is just the weak (propositional) beta rule for path constructors. If every = point computation rule held definitionally, then the path beta would be sim= ply
(apd (F=CB=A2 Id X=CB=A2) (paths gx) =E2=89=A1 paths=E1=B4=B0= gx (F=CB=A2 g X=CB=A2 gx))), which has the form we usually see when people= use HITs (with definitional point beta). Since path beta rules are general= ly only well-typed up to point beta rules, we need to refer to=C2=A0Tm=CB=A2 t and Tm=CB=A2 u to make it well-typed,= so the left side is wrapped in an extra composition. It's an arbitrary= choice whether to compose with point beta rules on the left side of the eq= uation or the right side, since the two versions are equivalent.

=
The names
of the sections sound algebraic, but I'm actual= ly not quite sure what they mean

<= div>It follows the terminology we use in the=C2=A0followup draft=C2=A0to the HIIT stuff. In the= HIIT paper we used "constructors", "motives/methods" a= nd "eliminators", but the new terminology is much better.=C2=A0 I= think Mike Shulman previously used the terms "algebra", "de= pendent algebra", and "dependent algebra section". We use &q= uot;displayed" instead of "dependent" because displayed alge= bras generalize Ahrens and Lumsdaine's displayed categories, in a rathe= r precise way.=C2=A0

In general, semantics for a i= nductive types should include constructing a category of algebras for each = syntactic declaration, where algebra homomorphisms are the morphisms. Howev= er, if we only have a category, we can only talk about initiality (unique r= ecursion), but not about induction, because that needs a notion of dependen= t object/family/fibration. So we need to have a category with a notion of d= ependent objects. In the draft paper we use CwF (category with families) wh= ere displayed algebras and sections form the "F" part, but there = are probably other workable choices as well.

Corlin Fardal <fardalcorlin@gmail.com> ezt =C3=ADrta (id=C5=91p= ont: 2018. aug. 22., Sze, 3:49):
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 do very= simply. I=E2=80=99d also read the QIITs paper, but, like I did with the II= Ts paper, gotten lost in the category-theoretical brushes, and ended up mis= sing 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 further = know about the construction by Lumsdaine and Shulman, but I wasn't enti= rely certain if that applied to my construction, it's been a while sinc= e 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 i= t would be impossible to construct any HIT from quotients, I thought that t= he subset I had created a Mu type for might still be constructible, and 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 replace it with = Const empty, and replace exfalso with a lifted function. Additionally I'= ;m kind of=C2=A0
struggling to understand what the path algebra in the definition= of Section is actually doing, is there a simple explanation? Also, though = this doesn't really matter, why is the path=C2=A0
algebra on=C2=A0the left side of the equati= on, instead of the right? It feels like if they're meant to be computat= ion rules, it should compute from the left down to the right, and because o= f that it
feels like it ought=C2=A0to go from the simple application of induction to the path, do= wn to a more complex expression. Additionally, as one last little nitpick, = my name's Fardal not Fardar, as
comment at the top of the file says, t= hough that really=C2=A0= doesn't=C2= =A0matter much. = However, despite all of my nitpicks/confusions, I really like your version = of it. The reformulation of 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 defining a quotient type in my version.=C2=A0I=C2=A0
also like the connection ma= de between the all function and the coerce function, I=C2=A0didn't realize the connecti= on there, as, at the very least, the two functions needed to finish the=C2= =A0
co= mputation 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 nic= e definition. The names
of the sections sound algebraic, but I'm actually not= quite sure what they mean. I mean, I know what an algebra is, I'm rela= tively well versed in the categorical semantics of at least
simple inductive type= s, but what are displayed algebras, or displayed algebra sections? Displaye= d algebras seem to have at least some connection to the fibred algebras of = the Higher
Inductive Types as Homotopy-Initial Algebras paper, and I have some id= ea of 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 HII= T paper's system and Kov=C3=A1c's version of my system to see if I can't und= erstand both of them more, 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 https://groups.google.com/d/optout.

--
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.
--00000000000041e448057405ce45--