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-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4711b23a for ; Tue, 21 May 2019 00:28:37 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id e17sf8841683otq.0 for ; Mon, 20 May 2019 17:28:37 -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=3R9v4m2/3TcFlGyQQdP9xjWoFOApG15Q4LsUxX/qMmA=; b=Bjn7pWtvZzf3h0OlpZ+o78PFH9OrwhKYLtxPVhENWKn0xLeSGwuVHeIgXDGNDNtUW5 oRtuvaMBJOQDWQhqg66UMSF2Yy/SK286Grrf78vxfDGLCKMMwT2+Rbmptt4TE/1LpE2T ea07hR/+WhgvD4jz0oBviih3t/TXk9Sq87dsVQmq+raHAeEbkPUt4NIzjcOoW9zFXNFp IZym3W+MlCMIDp9jp1gV95gh4lw8k4n9SKv+eOM5LPgCCnHkJ6yvENmF8uVA6/l/uBwA 2weD9Z3s5Yjl9HE3MpUN6vCJCCTce9xY14UZ8g4nOzxSGy6LfM9oeuq+z63YW0+mCPip ctFg== 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=3R9v4m2/3TcFlGyQQdP9xjWoFOApG15Q4LsUxX/qMmA=; b=N9ULSvhebb5pp0kcmkAPQjWQqP6xEuJ/NSpFBRofnwqT7ecsqcqEkM97VGY+gYoJD0 PRdronuQorxgK3l1yx2hmLAPqQBAnmoZtFMf39xdsR1zIubelk8u3qj/GhhFhIGQd54J qexO6HAfvg/72xfvQnGKn/MGGRbfb08WSxNhOoUu6XCLEPyucHg4XZ5g85Rk+cMah0Y3 w3d3FcYtEtYjPtOwQYw7glRlFo9OJ5mYLbNUihC/8Kn+EiopRJy2ikLoDqMuCS8B9VfE MSx8lyNPr+GEpOeRV199kr/T5mYbZ+hvkxY56vgHodSCm3WO5d45KElcep8EGY9rdEDZ f0eg== 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=3R9v4m2/3TcFlGyQQdP9xjWoFOApG15Q4LsUxX/qMmA=; b=Pe5zchKLaap9g+kZkJGuKsSaivSY1xZ9uNPHXWPOAZ/vw4OAC82MkieZ2vxIl1n4xW UNJQ7AXpHhc0JKqlS038i8LihUN7EYpQV5MH3pyXj2HLGo/cpd3joHnlJr+G678o+IHd Flh+5Q3LJJ9U5Ou+npifQ9n8GzWr2Lf6+hZktaEGzfgklG7RKcr2vLQrSLU+e05wMYmR hRoUgBFq+Bq5BZ+y1gbdquKasAugiU0T6xS3hvn/AWCnSVc8TrxtIdeBwahgw9bNPUvg 0cxy5V/qSU2BZS1VjEjpuUa2ePv8VkDnx0xuMADuJCqWChB9UM4T8rfezmqiumIQzJQu Lieg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV86ofNdtzxdDxXJhneGC2NOkarohulLTpm2VWXN4jdgISKnvP3 EuznioeGgeij4mZBssc9J+s= X-Google-Smtp-Source: APXvYqwM44PQJq9fBbkAMiC5CiyPhZJ+H7R0ViX7kGantsiDGxuCYQVSm7LieNzYvJ3Hvf4cJeLTTg== X-Received: by 2002:aca:54c7:: with SMTP id i190mr1529232oib.108.1558398516207; Mon, 20 May 2019 17:28:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:302:: with SMTP id 2ls737616oid.4.gmail; Mon, 20 May 2019 17:28:35 -0700 (PDT) X-Received: by 2002:a05:6808:28f:: with SMTP id z15mr1489349oic.32.1558398515833; Mon, 20 May 2019 17:28:35 -0700 (PDT) Date: Mon, 20 May 2019 17:28:34 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <64897263-717c-4596-9397-76f03b4e1c38@googlegroups.com> In-Reply-To: <96fea5d2-535c-43fc-9832-48ce96e916ca@www.fastmail.com> 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> Subject: Re: [HoTT] Semantics of QIITs ? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2070_2096195560.1558398514993" 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_2070_2096195560.1558398514993 Content-Type: multipart/alternative; boundary="----=_Part_2071_614698360.1558398514993" ------=_Part_2071_614698360.1558398514993 Content-Type: text/plain; charset="UTF-8" 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. ------=_Part_2071_614698360.1558398514993 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I'm not completely satisfied with Hugunin's techni= que, because it justifies only the "simple" elimination principle= , rather than the general, "recursive-recursive" elimination prin= ciple implemented in Agda. As far as I can tell, realistic use cases for in= ductive-inductive families also need the recursive-recursive elimination pr= inciple, where the types of the maps out of later families depend on the ma= ps out of earlier families. (I'm not sure how much of the other researc= h on IIFs stops short of handling recursion-recursion, but I think it shoul= d be taken seriously.)

On Monday, May 20, 2019 at 7:26:12 PM UTC-4, = Jon Sterling wrote:
Echoing And= ras, I recall that a new encoding due to Jasper Hugunin enable us to interp= ret 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 &= 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/64897263-717c-4596-9397-76f03b4e1c38%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_2071_614698360.1558398514993-- ------=_Part_2070_2096195560.1558398514993--