From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-yw1-xc3e.google.com (mail-yw1-xc3e.google.com [IPv6:2607:f8b0:4864:20::c3e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 69d18ccd for ; Thu, 16 May 2019 16:15:43 +0000 (UTC) Received: by mail-yw1-xc3e.google.com with SMTP id k134sf3581123ywe.7 for ; Thu, 16 May 2019 09:15:43 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558023342; cv=pass; d=google.com; s=arc-20160816; b=gecYx8sbujw0MrvOnUuDrZlopBjsJKjCommEhuQc9RQgBoZVxdcQBtvidWjF/gRmxO hDP2tDHWqLI6+ZdTzsQtuzJvodfqiXzUpNJIXENwmgTPjgDFTXqhTDh8jyTEP7Ea+zbn 8BAhtXIw6KWBgPJa1borbdFsJEqqT/+d8oMdKmbjP7OEN1AeH3Cm6ug8hSQ+aBu9Lc9j kvU4D8RFyiuA79hUcZWCDNmw9bvfRbnAkE6jOv6u5fMAAQHpl053uwFEMSoq+/efVPu7 7qGBpewf55cEanhBOSWbgSmU8LAdyva/KoFrEqSTgfXV/CGuZgW5sJX6Y4yTbqtmU6aR NiXw== 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:sender:dkim-signature :dkim-signature; bh=ds8K12LNYoqTFC7hgGww1aS16+GX0d9DMImlfCM7HpU=; b=Hz++lwUKTpHMhppijKd+y2fpF1vizRoEjMs3rCo4SgK4u8L160vj60cvdSwKQQzYAk 84qZX4K2gWuTfuYl3N2KCr8b45qFwks1OF3iF/3AzVU55vQqqZTSsN806tpMHHiY3rDc vJachnfxsPvGykWM90+PtHYvpKOp0gsSnGEx+5Tyd07LzUEj0J2m8SvS9JzpzMWhkxff 2Ic2Af/WqBGMLBnHf9cySmhwMf4UO2cZ5ZZfIRLR2HuWXOwoDoT/3O/u41Fh3Mx6hkUu M0b434hX8wpOZpiRCzJuyfTkIyjV4f3sBwfwIzidRYP2oFOokv+YAduhEGavVwCVZQ09 n2KA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=gb5g4vDj; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::743 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=ds8K12LNYoqTFC7hgGww1aS16+GX0d9DMImlfCM7HpU=; b=q0fbRU1wa7P5Afz/UJenOUxqhufqbUCdEdN4NsepdYtSUwAkb5hr6QxfyMJzgb70Qv Dph1B8fUKfNCuuHHuQL4WSpQxwErpIf24glQumciSKD/OoV1xEbVsQ8qwAxrNYmpBsa8 3b+WslRFjro6hBGlcQE4S9+DsUREcn/FpIc5FFaUyAJEkcMSEVEjvMUiGtXtW1mGUpCy LYReCmUjuiGonAWATmzwWaxqzZRy5FSmGzvkhx1wN22NAq8VzTCM7wbUmq1MxrenxTwJ 019l5x7ZpectAahouGHdvkQBOPuYuTakb0EH1KyD/hDYA4TMRq3aVu9pDja6hsmu4kXf 9s3Q== 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=ds8K12LNYoqTFC7hgGww1aS16+GX0d9DMImlfCM7HpU=; b=SvgOq5yFZrWLMgeliH8e4t5yW9+1uXtzISx44wwkCugEQtO6rVuwrwAiKZweX8t5C3 ROflX0GAj92fnCJ25G6hKDrFEdVcnReZwxFA9rpnmxXF96Wjbw4S59a6WK+OLWj7B+2z bDosiXy9qrveKcuG9O9LFtAxNteiKSCiETCI4uKSX/NnCMGfvJO1yBpt6GZvS3SawRc8 ewX/Cu4oVdHouBvpgvMP6cbr4xVjsKECF4zlhzVEBNppICvGGqSoFU9RLEXvU7HgoifK jV+iKUhOfR9nGSVtj56r8yd/R1R8eGHTMo7+B5kotsZEiR5KtYv2OnvydtgBPvX2tpnl chXA== 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=ds8K12LNYoqTFC7hgGww1aS16+GX0d9DMImlfCM7HpU=; b=XuLVSp6ECvDw3e4w3SzMfOsbsGbMIE1maxPDLH1vFM97FRvUcz+8XJmVhw86vcBQNP VMswn5VN8xpseqq6cBFkWQUB26qbIimCM6HlPBZhobRGNSnc7ihC46GRiXKdf4kgkPyt BHCdFHTWq+JTjPwTn7VFsg33TT0obYhcLDMMrhh9jA2lpjgolfHTVyco+rDXMqcq1oHW w5iJw5faKSxdU2OLuCj8FQ4G8L7gOgNaEhjc8k/mItSkHRK/+2QCyoGZCl5BoXcgg8Xy 5zUhU4OfGU6xvOzaaHAUdmCiDUfrSPx5wD7tlnghCP2pSNwIrs6XsawXXHMAL6Yjxtxt aGlA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWXp7JEqb49qZOJycoYYEZGzriMnu0/6Z1Gjv5SOd7gTEF7l4LG vyKWt0aLE87LziZEFcT8kl4= X-Google-Smtp-Source: APXvYqyvB55ziqZ9rguywXVNkRHiS57nYUXurjEJW1dZuI0Ka0PHP7fsb97Djjo4uacOZfl2+jKqew== X-Received: by 2002:a25:393:: with SMTP id 141mr24024491ybd.374.1558023342519; Thu, 16 May 2019 09:15:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:1d91:: with SMTP id d139ls713402ywd.6.gmail; Thu, 16 May 2019 09:15:42 -0700 (PDT) X-Received: by 2002:a81:4b8e:: with SMTP id y136mr12476681ywa.253.1558023342148; Thu, 16 May 2019 09:15:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558023342; cv=none; d=google.com; s=arc-20160816; b=vx7xNfJLc+r9ilwhZNM4gIaTSz6zb47Dq9LJTZnYnjinR+3lBB7K+u9o05czufz0E1 ImAJy4P+YOgKJEY3wWmhisaeBHuLwUYVa1FrvKNOjFedIvya4skpu7QEZmpU7/F7kuQT UhI09qb5F6D6jMinG2N9N30UqTee+2PpVmNMPEvtnNXVwg8utlMufF1+KqfWNF4AiyHH +c0GSrDiBjBmkGxooEM/gWU9+9LUQ3xVV8TWRSHyUi54SAEZ94iqyUi7jDFNn0HE7bRp +M9a/UlWocyZ+/+rAd5Ykiq6cyuOzW7Dki8ojiYhJDoABG6CHmRCYfTKJ6tbRExDR8r2 60bA== 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; bh=8y7/E6UgWR557nAtHOQZKjNhOP0vwqeOKioT0PuMGN4=; b=NC+8wVes9QYK8wH+dCMfpSCd5XPIZ91aJeSXjbss6XlHxLV8+QLQ+WWaIfpw7UoyNg l7UsCaVptI2uWfizslbfksusa0a7oSGb8p2y7fgLuBzJlaFweNsU8kC0TrAHye3Y1tRU di5FqQUXRedCSghZnPULewF/FiBz+EJWFZAOoBDJyF4IITVko20XT1k2mB6LaNBx64u4 UC75Cb2B3NM/3VJz/zX6NHxXhD6Cf53MKbl0CsUa5kuL2EeFWQIyVwCzQ9a2vLe9BIU/ b6+QDEN4Ype0yQ1Z79aSmjMfiYXSmLtu7i3NV7unncYnmMnFogXl+GamBMUIkG8xQPJk QV0Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=gb5g4vDj; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::743 as permitted sender) smtp.mailfrom=puttamalac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x743.google.com (mail-qk1-x743.google.com. [2607:f8b0:4864:20::743]) by gmr-mx.google.com with ESMTPS id i63si569520ywa.2.2019.05.16.09.15.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 May 2019 09:15:42 -0700 (PDT) Received-SPF: pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::743 as permitted sender) client-ip=2607:f8b0:4864:20::743; Received: by mail-qk1-x743.google.com with SMTP id c15so2632377qkl.2 for ; Thu, 16 May 2019 09:15:42 -0700 (PDT) X-Received: by 2002:a37:480e:: with SMTP id v14mr19431991qka.344.1558023341792; Thu, 16 May 2019 09:15:41 -0700 (PDT) MIME-Version: 1.0 References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> In-Reply-To: From: =?UTF-8?B?QW5kcsOhcyBLb3bDoWNz?= Date: Thu, 16 May 2019 18:15:30 +0200 Message-ID: Subject: Re: [HoTT] Semantics of QIITs ? To: Bas Spitters Cc: Thorsten Altenkirch , homotopytypetheory , Ambrus Kaposi Content-Type: multipart/alternative; boundary="000000000000d6e1730589039384" 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=gb5g4vDj; spf=pass (google.com: domain of puttamalac@gmail.com designates 2607:f8b0:4864:20::743 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: , --000000000000d6e1730589039384 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi, In "Constructing QIITs", we only considered signatures and their semantics in the setting of extensional TT. It is currently an open problem whether construction of QIITs (in the style of our paper) can be performed without UIP, and also whether the syntax of QIIT signatures itself is constructible in such setting. Jasper Hugunin's recent work on constructing some inductive-inductive types in cubical TT could relevant here. best regards Andr=C3=A1s Bas Spitters ezt =C3=ADrta (id=C5=91pont: 2019. = m=C3=A1j. 16., Cs, 17:50): > Hi Thorsten, > > Yes, I saw your result (congratulations!) However, I may be > overlooking something, but do we know that the theory of codes is > available in any of the standard models of HoTT? > That doesn't seem to be stated in your paper. > > Best regards, > > Bas > > > On Thu, May 16, 2019 at 5:39 PM Thorsten Altenkirch > wrote: > > > > Hi Bas, > > > > Our POPL 2019 paper does address this I think, maybe not exactly in the > way you expect. We define a theory of codes (based on earlier work by > Ambrus and Andras) which is an intrinsic type theory such that a context = is > a representation of a quotient inductive-inductive type. The formation of > Pi-types is restricted so that you can only form strictly positive types, > it is indeed a special case of a directed type theory. Now the semantics > are categories with an initial object and it turns out we can construct t= he > semantics just from assuming the existence of the theory of codes. The > category assigned to a context is the category of algebras and the initia= l > object is the intended interpretation of the QIIT, equivalently we get th= e > expected elimination principle. The theory of codes can "eat itself" it i= s > an instance of a QIIT definable in itself. Hence this QIIT is in a certai= n > sense universal. > > > > One would also like to interpret QIITs that are indexed by "external" > types which are already defined and in particular include infinitary > constructors. One can extend the theory but the semantics suffered from a > coherence issue. However, I think Andras made some progress on this. > > > > My view is that this programme can be extended to HIITs by considering > higher order versions of type theory and in particular the theory of code= s. > However, this is maybe an overkill, since one can normalize the > substitutions (make them implicit) and address the coherence issues this > way. I think that is basically what Andras has done. > > > > Here is a link to the pdf: > > https://akaposi.github.io/finitaryqiit.pdf > > > > Thorsten > > > > =EF=BB=BFOn 16/05/2019, 15:58, "homotopytypetheory@googlegroups.com on = behalf > of Bas Spitters" b.a.w.spitters@gmail.com> wrote: > > > > What is the status of the semantics of quotient inductive inductive > types? > > Looking at the literature there's some progress on reducing QIITs t= o > > simpler constructions, but this does not seem to have led to a > > convenient semantic result. > > E.g. QIITs do not seem to be treated in the work by Lumdaine and > Shulman. > > > > https://ncatlab.org/nlab/show/inductive-inductive+type > > > > Do we know that the prototypical QIITs from the book (e.g. Cauchy > > reals) are supported in the usual models of HoTT? > > > > Thanks, > > > > Bas > > > > -- > > 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. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQBwyvbY_f3qNZ= OgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com > . > > For more options, visit https://groups.google.com/d/optout. > > > > > > > > > > > > This message and any attachment are intended solely for the addressee > > and may contain confidential information. If you have received this > > message in error, please contact the sender and delete the email and > > attachment. > > > > Any views or opinions expressed by the author of this email do not > > necessarily reflect the views of the University of Nottingham. Email > > communications with the University of Nottingham may be monitored > > where permitted by law. > > > > > > > > > > -- > 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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQT%2BcX7QbmKT= %2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout. --000000000000d6e1730589039384 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi,

In "Constructing QIITs", = we only considered signatures and their semantics in the setting of extensi= onal TT. It is currently an open problem whether construction of QIITs (in = the style of our paper) can be performed without UIP, and also whether the = syntax of QIIT signatures itself is constructible in such setting. Jasper H= ugunin's recent work on constructing some inductive-inductive types in = cubical TT could relevant here.

best regards
=
Andr=C3=A1s

Bas Spitters <b.a.w.spitters@gmail.com> ezt =C3=ADrta (id=C5=91pont: 2019.= m=C3=A1j. 16., Cs, 17:50):
Hi Thorsten,

Yes, I saw your result (congratulations!) However, I may be
overlooking something, but do we know that the theory of codes is
available in any of the standard models of HoTT?
That doesn't seem to be stated in your paper.

Best regards,

Bas


On Thu, May 16, 2019 at 5:39 PM Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>
> Hi Bas,
>
> Our POPL 2019 paper does address this I think, maybe not exactly in th= e way you expect. We define a theory of codes (based on earlier work by Amb= rus and Andras) which is an intrinsic type theory such that a context is a = representation of a quotient inductive-inductive type. The formation of Pi-= types is restricted so that you can only form strictly positive types, it i= s indeed a special case of a directed type theory. Now the semantics are ca= tegories with an initial object and it turns out we can construct the seman= tics just from assuming the existence of the theory of codes. The category = assigned to a context is the category of algebras and the initial object is= the intended interpretation of the QIIT, equivalently we get the expected = elimination principle. The theory of codes can "eat itself" it is= an instance of a QIIT definable in itself. Hence this QIIT is in a certain= sense universal.
>
> One would also like to interpret QIITs that are indexed by "exter= nal" types which are already defined and in particular include infinit= ary constructors. One can extend the theory but the semantics suffered from= a coherence issue. However, I think Andras made some progress on this.
>
> My view is that this programme can be extended to HIITs by considering= higher order versions of type theory and in particular the theory of codes= . However, this is maybe an overkill, since one can normalize the substitut= ions (make them implicit) and address the coherence issues this way. I thin= k that is basically what Andras has done.
>
> Here is a link to the pdf:
> https://akaposi.github.io/finitaryqiit.pdf
>
> Thorsten
>
> =EF=BB=BFOn 16/05/2019, 15:58, "homotopytypetheory@googlegroups.com= on behalf of Bas Spitters" <homotopytypetheory@googlegroups.com<= /a> on behalf of b.a.w.spitters@gmail.com> wrote:
>
>=C2=A0 =C2=A0 =C2=A0What is the status of the semantics of quotient ind= uctive inductive types?
>=C2=A0 =C2=A0 =C2=A0Looking at the literature there's some progress= on reducing QIITs to
>=C2=A0 =C2=A0 =C2=A0simpler constructions, but this does not seem to ha= ve led to a
>=C2=A0 =C2=A0 =C2=A0convenient semantic result.
>=C2=A0 =C2=A0 =C2=A0E.g. QIITs do not seem to be treated in the work by= Lumdaine and Shulman.
>
>=C2=A0 =C2=A0 =C2=A0https://ncatlab.org/nl= ab/show/inductive-inductive+type
>
>=C2=A0 =C2=A0 =C2=A0Do we know that the prototypical QIITs from the boo= k (e.g. Cauchy
>=C2=A0 =C2=A0 =C2=A0reals) are supported in the usual models of HoTT? >
>=C2=A0 =C2=A0 =C2=A0Thanks,
>
>=C2=A0 =C2=A0 =C2=A0Bas
>
>=C2=A0 =C2=A0 =C2=A0--
>=C2=A0 =C2=A0 =C2=A0You received this message because you are subscribe= d to the Google Groups "Homotopy Type Theory" group.
>=C2=A0 =C2=A0 =C2=A0To unsubscribe from this group and stop receiving e= mails from it, send an email to HomotopyTypeTheory+unsubscribe@= googlegroups.com.
>=C2=A0 =C2=A0 =C2=A0To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQBw= yvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com.
>=C2=A0 =C2=A0 =C2=A0For more options, visit https://groups.goo= gle.com/d/optout.
>
>
>
>
>
> This message and any attachment are intended solely for the addressee<= br> > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>

--
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. To view this discussion on the web visit https:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%= 2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.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.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTO= SW2PfX1EreKnOe2ozQ%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000d6e1730589039384--