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=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,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-ua1-x93f.google.com (mail-ua1-x93f.google.com [IPv6:2607:f8b0:4864:20::93f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2225c1b2 for ; Tue, 21 May 2019 02:45:26 +0000 (UTC) Received: by mail-ua1-x93f.google.com with SMTP id p9sf2555865uad.23 for ; Mon, 20 May 2019 19:45:26 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558406725; cv=pass; d=google.com; s=arc-20160816; b=NX54Y1tcKwNQLZ8tDKybWQY08lwIHKabZIRtmCdUeo2B0Gjetd7twt7WZee2ciNjLJ 9Zj7vpjmeIqfNezFmskfgj1PxPWcb639EiZKMQ0ZeDawvMAZiUhYA7hD5uBEbBH6igZo Nxcp7mMb35Si77EmE/cYj0gbVBZmxaV/SBsglTG+zB/ydL8ntB0ADWFo0t6Nh0HWLzlz oMgaWRTP6D4V43QJtn+xtYXwXgsxFq90BgoVRWDmzFV7Wcg4nFTaNp9YWi4ToNe6OUs9 CuPjlklquXwbndTkQIgBqU+Ue2uoO/NWbSF+6A/GbnufRbFAVyBGlzjOgpBhzcZUjlKa h5oQ== 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:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature; bh=TTHU5uP5sxCjFmuLcrhvTmWPbQ2ZJe9NOmr9LdVKZp4=; b=eXbbBd8/UPGb2XDFQrlh4SLalc83icODMZcB5UOiQKtCPNzQEv5OczqNn4ajXOmuXv TnPmpTEBw3V/Z9weStNlXpDCRlLebr8n+e3jcdrlD3l0TBSbZcyJ7F7d7b5clB5+Oz6V c769JRDAnNgQLeROT3AW6ElqSPBTZcGZiyq1Y7pmYVEiu23/GoGZhmHgTN9nDZNq9v1p g+Z19HzDmz03xOwGCIOzYlQximka/XEtR68Aio+4OOZsmxyTkOOqCOo4zVcqD7AorZvd gjdy1pt5ffUsZ6ccOpadhY+XBZoh2EJlNrbYHQa8/mqTCTs+BCiXTIMpZExcvTmpIvkg BZXQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=Sh6zM1Wu; spf=neutral (google.com: 2607:f8b0:4864:20::32c is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=TTHU5uP5sxCjFmuLcrhvTmWPbQ2ZJe9NOmr9LdVKZp4=; b=GPrFriLf3GxGYyaeqjV+IRyy8Cr94F91kfTd6ipWYLB727eWWi4i3TuhZaS3fSUM4U xsouGhoIPJnSTYfKX+qTdxCklJLw1m5AgDbbDkdQObsBXPM8YMIli3aD7RATLdb8yLLe Qj5V9M4w9i5jPI2CkibcfrzuP0Izq3bAjiHZoU37oFbJhfbk/8XKNthZQ8voOed0M1W9 5ywe7gFjRS0Sm/B6x9bJRPs7486oxCMJhaU2tSpyrvFoesH3dvTvUUjAU9zTb4zR5+1U JUZkT45ciBQ3KLOdTWh5tE/vbakAre3gX+yz3tAu1SfCYZhE1X6Lwy77ChU3iaG60Osc XXGQ== 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: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=TTHU5uP5sxCjFmuLcrhvTmWPbQ2ZJe9NOmr9LdVKZp4=; b=kMeD24SMBLRH0ImjueVZtAI06R+yHciyujXvZkfpm0yVXrnDBYNcrYmOTvE757tPHK av9rGuKTxY4MR8V9tnCQFatSn1HLfs5hB0wNRmt5+suMTY+AzOObHeZkTLuEGymDnEvy aXtiN/DW7ArVNnMaa72QMWbCDwkjhnx663XwExlhnjkufp/ufvBqwGOsx+75BGsRC21+ ztp2Ra7g3/036VbYE1lPsPkcrvQjzVQqQ9kOSXBrIKCL7n+ccLGYENbajdez9bBtAkQh +lTOJ4tXfaAo8B5ori8H5WPEwq4qlpfBlHatewrouPEO7EwWXDO/wYYueBd3uAsE+nAt rSEA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV7XvvVfAFF8y+fOAq6aXTmhbO+7H7tMJUCZGoW1FSzsZGr6mTI TlQu2aeVRpoovUFDFWlj9A8= X-Google-Smtp-Source: APXvYqzJ0nR6eCNjBjj9NCv4ByHGSngKhmcNdn+rPgHKKHZt4Sh8kdrMqTMOpD+HgsKhkMCkSGfqfA== X-Received: by 2002:a67:8c47:: with SMTP id o68mr39046348vsd.170.1558406725395; Mon, 20 May 2019 19:45:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:42b:: with SMTP id 40ls281785uav.5.gmail; Mon, 20 May 2019 19:45:24 -0700 (PDT) X-Received: by 2002:ab0:484c:: with SMTP id c12mr13213908uad.57.1558406724928; Mon, 20 May 2019 19:45:24 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558406724; cv=none; d=google.com; s=arc-20160816; b=W3/bK1cDWDxLx54HAlSMxIHP514QLh7Zk9VSOqjgWYDO+GK1xo45+jTFXD1sxh9tTh DjtOPnUBySRy3QFCEfQSkfq7gBpGXSh1kO05kvxM5caAfrm3wv/eGodfgJempfTla4k6 fWduO6DciR5wZOAok3CcHZfVcyM7Nt1aAfodinPTq7+fICcjIMkU5Bdthy9hXS9eWEQ2 VzddGgF9w+0GKFpIrg8IsN3dGB3bA2yEwqavuXKDDtNbtTkuxk/UYWPlTiLdOlEky97K PmWieDECTk3H4JeOTxga32pvIlftJaScdTVRU+QAlf3i5sIJwpjgQxxYERuHAoMCJEFT b2MQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=NTpvsiRvEGJRWbvTNURtdfXUv8xDyLMBvEtTe34AC9M=; b=zL9IYdHazmaEQPliWZmMK4C/gTDm87KW2LX8SC3dSnDj64S4SM3jvRjBqKB0sa2Sml ncLGSDbI7CQd9/TeueklZQtSnsHR9XdORUooTSX+kJuNhDJG7ahuuSuVK67Fgj9Eitkl Wu+Cf4m6v+ne28YtBLvSDroreBEfIEZou49w83dyVTgN+RMK+USNQn3fZj201EKh7wZU TV+wqqMVyITOI/70z4frFbiS6emdj9Ez4PjLM5rZyHLPbv11cyd39cqcTW85HKsZffWs hst1PVF9S8naKQcqou60A9iFTjuSDp68G2yEMrNm1GlhO29Akq1zNg1E8pzDHIkI5Wu2 3b1A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=Sh6zM1Wu; spf=neutral (google.com: 2607:f8b0:4864:20::32c is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu Received: from mail-ot1-x32c.google.com (mail-ot1-x32c.google.com. [2607:f8b0:4864:20::32c]) by gmr-mx.google.com with ESMTPS id 19si1808902vkv.4.2019.05.20.19.45.24 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 19:45:24 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::32c is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) client-ip=2607:f8b0:4864:20::32c; Received: by mail-ot1-x32c.google.com with SMTP id j49so14895657otc.13 for ; Mon, 20 May 2019 19:45:24 -0700 (PDT) X-Received: by 2002:a9d:538b:: with SMTP id w11mr1826568otg.154.1558406724283; Mon, 20 May 2019 19:45:24 -0700 (PDT) MIME-Version: 1.0 References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk> <4CAE313E-7B00-41D3-A13A-3AAC0A496AB0@exmail.nottingham.ac.uk> <96fea5d2-535c-43fc-9832-48ce96e916ca@www.fastmail.com> <64897263-717c-4596-9397-76f03b4e1c38@googlegroups.com> In-Reply-To: <64897263-717c-4596-9397-76f03b4e1c38@googlegroups.com> From: Jasper Hugunin Date: Mon, 20 May 2019 19:45:13 -0700 Message-ID: Subject: Re: [HoTT] Semantics of QIITs ? To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000003784cd05895cd759" X-Original-Sender: jasperh@cs.washington.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=Sh6zM1Wu; spf=neutral (google.com: 2607:f8b0:4864:20::32c is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu 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: , --0000000000003784cd05895cd759 Content-Type: text/plain; charset="UTF-8" Hello all, To confirm what others have said about my construction: As Andras and Jon noted, it remains open whether the construction can be extended to reduce higher inductive-inductive types to higher inductive types, but I am hopeful that it can, at least in a situation such as CTT where the eliminator computes on path constructors. As Matt noted, the general recursive-recursive eliminator is both essential (for proving initiality, for example) and missing. This is the same restriction as on the construction in extensional type theory (or using UIP) given by Nordvall Forsberg. The main obstacle I see to getting the general recursive-recursive eliminator is that the simple eliminator is not strict, but only computes up to a path. I think I see a way to turn a strict simple eliminator into a general eliminator, but this is still conjectural. To summarize my understanding of the original question, QIITs are an obvious subset of HIITs, and we know how to handle many HITs primitively in cubical type theory, but the extension to primitive HIITs in cubical type theory has not been done, nor does my construction immediately allow reducing HIITs to HITs (and even if extended lacks strictness and generality of the eliminator). Best regards, - Jasper Hugunin On Mon, May 20, 2019 at 5:28 PM Matt Oliveri wrote: > I'm not completely satisfied with Hugunin's technique, because it > justifies only the "simple" elimination principle, rather than the general, > "recursive-recursive" elimination principle implemented in Agda. As far as > I can tell, realistic use cases for inductive-inductive families also need > the recursive-recursive elimination principle, where the types of the maps > out of later families depend on the maps out of earlier families. (I'm not > sure how much of the other research on IIFs stops short of handling > recursion-recursion, but I think it should be taken seriously.) > > On Monday, May 20, 2019 at 7:26:12 PM UTC-4, Jon Sterling wrote: >> >> Echoing Andras, I recall that a new encoding due to Jasper Hugunin enable >> us to interpret IITs without using UIP, and it is an open question to >> determine whether Jasper's ideas can be extended to QIITs. I hope they can, >> and someone should find out :) >> >> Best, >> Jon >> > -- > 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/64897263-717c-4596-9397-76f03b4e1c38%40googlegroups.com > > . > For more options, visit https://groups.google.com/d/optout. > -- 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/CAGTS-a9F-8ph2U4MoPFaoTHam0SCTg3YZWAEJAjyLrrbBd71sw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --0000000000003784cd05895cd759 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello all,

To confirm = what others have said about my construction:
As Andras and Jon no= ted, it remains open whether the construction can be extended to reduce hig= her inductive-inductive types to higher inductive types, but I am hopeful t= hat it can, at least in a situation such as CTT where the eliminator comput= es on path constructors.
As Matt noted, the general recursive-rec= ursive eliminator is both essential (for proving initiality, for example) a= nd missing. This is the same restriction as on the construction in extensio= nal type theory (or using UIP) given by Nordvall Forsberg. The main obstacl= e I see to getting the general recursive-recursive eliminator is that the s= imple eliminator is not strict, but only computes up to a path. I think I s= ee a way to turn a strict simple eliminator into a general eliminator, but = this is still conjectural.

To summarize my underst= anding of the original question, QIITs are an obvious subset of HIITs, and = we know how to handle many HITs primitively in cubical type theory, but the= extension to primitive HIITs in cubical type theory has not been done, nor= does my construction immediately allow reducing HIITs to HITs (and even if= extended lacks strictness and generality of the eliminator).

Best regards,
- Jasper Hugunin
=
On Mon= , May 20, 2019 at 5:28 PM Matt Oliveri <atmacen@gmail.com> wrote:
I'm not completely satisfied wit= h Hugunin's technique, because it justifies only the "simple"= elimination principle, rather than the general, "recursive-recursive&= quot; elimination principle implemented in Agda. As far as I can tell, real= istic use cases for inductive-inductive families also need the recursive-re= cursive elimination principle, where the types of the maps out of later fam= ilies depend on the maps out of earlier families. (I'm not sure how muc= h of the other research on IIFs stops short of handling recursion-recursion= , but I think it should be taken seriously.)

On Monday, May 20, 2019= at 7:26:12 PM UTC-4, Jon Sterling wrote:
Echoing Andras, I recall that a new encoding due to Jasper = Hugunin enable us to interpret IITs without using UIP, and it is an open qu= estion to determine whether Jasper's ideas can be extended to QIITs. I = hope they can, and someone should find out :)

Best,
Jon

--
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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/64897263-717c-4596-9397-= 76f03b4e1c38%40googlegroups.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/CAGTS-a9F-8ph2U4MoPFaoTHam0SCTg3Y= ZWAEJAjyLrrbBd71sw%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000003784cd05895cd759--