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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-ot1-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 11fc862e for ; Tue, 21 May 2019 19:56:59 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id q12sf35777oth.15 for ; Tue, 21 May 2019 12:56:59 -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=O7Ac4OvSvkRJU77VaYk9jyGySbPIR+UOSZ9J+jDpFTE=; b=Y0D4jMAtoxrgZK0YT/8M9GNE5JT72qfdPWaFrWOWGLcDSLJtIEXupzFQtf1kJi/zMa XCfTfnP44IN4pLlpvXwmbUQXfXW0DlOvT/og2H5HMViR9AmCMwcEGJRIMZgzo+Nx9TwD XAGFwXp03OjBJ6ElFfjMDx2PZqxatNE5bDl6OfB/5jVtlito3S0OFAhEVD17mV3xn8gd wgSsflnkghR3SesHyxEsMMP6JDASDuGK2KtaV7sjbSH+B6PhNZdUHwpA0BsVSvVu3nvm hMv9OnGGV0U9bu6XaOYWQYiI++/57cyU8cFM8hlvqr1Dj35vrTkmr/2dPX6PeF5R3CD6 ZlDQ== 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=O7Ac4OvSvkRJU77VaYk9jyGySbPIR+UOSZ9J+jDpFTE=; b=pUNYa9/Eb+dgPFq/Jv/XMKjCUv3cpBL96xBBnV9cMGBlWF3yyQ61wzpXeV768CjlWc WTnrRN2liNB11NKqp2pyir1cXCEPtI37LKVqo5+mPkR3jcaO9gZnDLzQHva9ob1dhzNB EcE3rP176evSDPaOobEsrwC2aTx03xdp1c3yr46mzO5TluROgZDMH4sty+HoLgtV8ele cfjUwfQGFMk986k3uK2hLG+ANqMlV9OQ2rOVYkvGgEqeOEftnRSI1P7sxACXJIypgDAa qA9m5Hh17fjZ/J0VIPIvQltfQC/fIXuCoSw5ljuIAj8fBTZQbJYvBUcM4RzV6uI/c/Oa aVLA== 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=O7Ac4OvSvkRJU77VaYk9jyGySbPIR+UOSZ9J+jDpFTE=; b=svizu3tn5hqqZL115ub2NqWlOM1uswouhrEzfK8YWCP050gxMvgyymO85HAeTsHyF4 EIGaEwgkkeSxc/Cc5Jjuu2J/8i8/xpm3qtwk17uf59+e1IVFjlcH6CEe+JGzT/FW+xPs sOGl/1J/optRC1Nv9RRRlkzaqm9/PfFOMrkjBz3cGKbZpIaYa0whIqTKnFZO5TQ+XYQ9 OsLL5xEg0eOQgG7O47pt5eYnbanQDxSuSifq1SQdo8iMT6sqA+NJZb4WkKhy3GLhowax CM1RFE8/Wc8YEYPx+uuPkMLVazPAOZG2/QEdkUx917zeg6f0u1kljY44RYe+CsfHWe1Y Ujkg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUKVig25M4eLKYwMdfmqxBZMkIWB0NT7sJIxVnAH4wH8HxKe+am 7yvXyMgVd/1UHvQXO5M/0Lc= X-Google-Smtp-Source: APXvYqy+M38yvVLxTrfiEc9HEKQcVJvURBbKIjulG3b2zQHDFV1vgXNLEueoVl48NNEXuYodTy+kbA== X-Received: by 2002:aca:b403:: with SMTP id d3mr3357341oif.179.1558468618558; Tue, 21 May 2019 12:56:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6345:: with SMTP id y5ls15272otk.3.gmail; Tue, 21 May 2019 12:56:58 -0700 (PDT) X-Received: by 2002:a9d:77d9:: with SMTP id w25mr15582967otl.366.1558468618164; Tue, 21 May 2019 12:56:58 -0700 (PDT) Date: Tue, 21 May 2019 12:56:57 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <22a97b80-cab0-49f6-b3fb-b1b44fd41e9c@googlegroups.com> In-Reply-To: <3DC3F379-F057-49AF-9232-CDC925E9646B@nottingham.ac.uk> 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> <3DC3F379-F057-49AF-9232-CDC925E9646B@nottingham.ac.uk> Subject: Re: [HoTT] Semantics of QIITs ? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2207_185106662.1558468617273" X-Original-Sender: atmacen@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_2207_185106662.1558468617273 Content-Type: multipart/alternative; boundary="----=_Part_2208_931716536.1558468617274" ------=_Part_2208_931716536.1558468617274 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks. This sounds a lot like the interpreter I did=20 (https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/) that= =20 required UIP, and like Streicher's method for proving initiality of the=20 syntax of dependent type theory. Combining it with Hugunin's technique=20 sounds promising! On Tuesday, May 21, 2019 at 4:33:10 AM UTC-4, Thorsten Altenkirch wrote: > > This problem has been solved =E2=80=93 see our TYPES 2018 abstract (attac= hed).=20 > > =20 > > Basically the idea is to define a relation between =E2=80=9Cpre-terms=E2= =80=9D and the=20 > semantics and then show that this is contractible for =E2=80=9Cwell-typed= objects=E2=80=9D,=20 > this way you avoid the mutual dependency. This was an idea by Andras=20 > Kovacs. In this year=E2=80=99s TYPES there are two abstracts that show ho= w this can=20 > be used to give a universal reduction from Inductive-Inductive types to= =20 > indexed inductive types and hence W-types.=20 > > =20 > > I have discussed this with Jesper when he was in Nottingham and I think= =20 > our tentative conclusion was that this could be combined with his approac= h=20 > to provide a reduction for IITs. However, this needs to be checked. > > =20 > > Thorsten > > =20 > > *From: *> on behalf of Matt= =20 > Oliveri > > *Date: *Tuesday, 21 May 2019 at 01:28 > *To: *Homotopy Type Theory > > *Subject: *Re: [HoTT] Semantics of QIITs ? > > =20 > > I'm not completely satisfied with Hugunin's technique, because it=20 > justifies only the "simple" elimination principle, rather than the genera= l,=20 > "recursive-recursive" elimination principle implemented in Agda. As far a= s=20 > I can tell, realistic use cases for inductive-inductive families also nee= d=20 > the recursive-recursive elimination principle, where the types of the map= s=20 > out of later families depend on the maps out of earlier families. (I'm no= t=20 > sure how much of the other research on IIFs stops short of handling=20 > 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:=20 > > Echoing Andras, I recall that a new encoding due to Jasper Hugunin enable= =20 > us to interpret IITs without using UIP, and it is an open question to=20 > determine whether Jasper's ideas can be extended to QIITs. I hope they ca= n,=20 > and someone should find out :)=20 > > Best,=20 > Jon > > > --=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/22a97b80-cab0-49f6-b3fb-b1b44fd41e9c%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2208_931716536.1558468617274 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks. This sounds a lot like the interpreter I did (http= s://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/) that requi= red UIP, and like Streicher's method for proving initiality of the synt= ax of dependent type theory. Combining it with Hugunin's technique soun= ds promising!

On Tuesday, May 21, 2019 at 4:33:10 AM UTC-4, Thorsten= Altenkirch wrote:

This problem has been solved =E2=80=93 see our TYPES= 2018 abstract (attached).

=C2=A0

Basically the idea is to define a relation between = =E2=80=9Cpre-terms=E2=80=9D and the semantics and then show that this is co= ntractible for =E2=80=9Cwell-typed objects=E2=80=9D, this way you avoid the= mutual dependency. This was an idea by Andras Kovacs. In this year=E2=80= =99s TYPES there are two abstracts that show how this can be used to give a uni= versal reduction from Inductive-Inductive types to indexed inductive types = and hence W-types.

=C2=A0

I have discussed this with Jesper when he was in Not= tingham and I think our tentative conclusion was that this could be combine= d with his approach to provide a reduction for IITs. However, this needs to= be checked.

=C2=A0

Thorsten

=C2=A0

From: <homotopyt...@go= oglegroups.com> on behalf of Matt Oliveri <atm...@gmail.com> Date: Tuesday, 21 May 2019 at 01:28
To: Homotopy Type Theory <homotopyt...@googlegroups.com> Subject: Re: [HoTT] Semantics of QIITs ?

=C2=A0

I'm not completely = satisfied with Hugunin's technique, because it justifies only the "= ;simple" elimination principle, rather than the general, "recursi= ve-recursive" elimination principle implemented in Agda. As far as I can tell, realistic use cases for inductive-inductive families al= so need the recursive-recursive elimination principle, where the types of t= he 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 recal= l that a new encoding due to Jasper Hugunin enable us to interpret IITs wit= hout 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 &= 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.co= m/d/msgid/HomotopyTypeTheory/22a97b80-cab0-49f6-b3fb-b1b44fd41e9c%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_2208_931716536.1558468617274-- ------=_Part_2207_185106662.1558468617273--