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.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lf1-x13a.google.com (mail-lf1-x13a.google.com [IPv6:2a00:1450:4864:20::13a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1e47241d for ; Thu, 16 May 2019 15:39:33 +0000 (UTC) Received: by mail-lf1-x13a.google.com with SMTP id c18sf758767lfi.22 for ; Thu, 16 May 2019 08:39:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558021172; cv=pass; d=google.com; s=arc-20160816; b=LYxuHjWorsyDHszn8MaRP3QNiKDNThCq68Y1SZZm2LVA3rE/breSxR38Nl/wSjej7w RoOSQIE6ZfV16jT9T3nvrxkxI40ie7jIOo3xCOiI+jRZAoIdtjnGOobj+lfyp/YFKDJr tPPFiP7nDmxy3ZtZBIMq9zp3RlLsKZHokOEudlnfZ4QauHLrH9g8KRQmfzrDgo/yMidH CXvbA7InxcsH6zyRTrh+hwom+nZorbT3jvZ46Z0hDddARb57p8Ex2pz5hhc99DF6TWN1 logJOEUgTvN9zdeAn7mnrS35AxSm6UQxMLMs2I5iuiIG2w9ep4OSMLhvKz9G0vcIsRwN uKFg== 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:mime-version:content-transfer-encoding :content-id:user-agent:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from:sender:dkim-signature; bh=6i8Nm+vljkhpxYmVknavwnEwM9OAOQjiyFmqzdr8L8E=; b=gsbWZKmUZzKydXBDuhkbkglLZN/pjVltqGuz4J68dVUcji3jGRCejCLlh6agelreED 1kBp0p0X5asCPSyOB6IGnv8wwuKiEsVgQApz3ylqpwygOE3g1U2mAY/tsqTPUr125p1l vblq2Xilplpx56onkjMXf/C2xbsrTCPDH2ENKO3U1GFhDVPP4bdJqG7WfVtXG4x3oR6j P0/Do3iOf5kx7BZ9a/JNxNJ3UvoMSEZMeVu8l3aP/mf/Y37DNzZX5BDbxLLPoVrzkc2/ Mu2xITl396HDTNxoRcnj9rTFZdUgZyt8Kj74YiXvHWCsjT2Xi7TaSiaDHi3xaPrsS20V EfaQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :content-id:content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=6i8Nm+vljkhpxYmVknavwnEwM9OAOQjiyFmqzdr8L8E=; b=cGRO2wXIP4tD4X9eMZ+due1mXmr3hyGW7Dcv92OlEtquR0irsTGei4PSOYQjtn8jE7 DXpcgElaXuceLeIIc93qQNZhsg7vV/SN3CkhUzNpUDpc0l0DYtrAJHbNP62EbeasL+4K h5cF5uyGCqPYVvOKo03xQDJGLtj4O7s++cGirz/hi0xYsBSgq2DLRtayeo/pYTgsNKbz iNYMkAe3A5jJvwHdRJkKNUH5zKujWZ5VjYgCqBzc+O2L580DtuBkWNI3RL7UWp600mJC Jnvt88A3QBzhPeZmcOKP0/AP78UeWuJjTpbuW76+Uh1DUyUuvPN4XKf1wuANqXm96NZ3 dluw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:user-agent:content-id:content-transfer-encoding :mime-version: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=6i8Nm+vljkhpxYmVknavwnEwM9OAOQjiyFmqzdr8L8E=; b=RtOCsz1/qUOL+f347/k7jGsC0eUG01aVO3+kJ62DAChb35dbd0LjWKGdWB/W468sh2 ghXsVyoe5mIJGX9ruV3t5YSeh8XA65j+3fwZ3zd+XdSDRDUUKqX/HJ/cuyABVPv5pRvt EIuUASML1J4NXU2+udsp7+IOn7AYBYAG3zlzl+wn251z/vIGpXJz8FAoqNjxKIzH+9rW Qqlqf6zBshj7wBcr0AYM6BP/OOhIdusyS1/lgXj7VBv6D4eMUSHU2b/xCaQSPIgMcT2A izBQjmHD97JkaMmmX+p0YO7KcAs/7Pw4tPMFCA7LP1+5yO4/LCDLV3PnKqwyTwQu3cIq LuhQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXN9tgQHs0UZD7cDM62mbf5Cqe4nPO69WnZZXVOElmQceFG+Uq4 7u7xYUyHUhEftRTjaG6woMw= X-Google-Smtp-Source: APXvYqzaJ+AmjYJwBHoByAGdHLWTQnzK/sqwX2ZqdiNbVS9RfVvUYuinX9foPzRwDc2wu0zipbltew== X-Received: by 2002:ac2:4357:: with SMTP id o23mr26078892lfl.146.1558021172840; Thu, 16 May 2019 08:39:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:5d1b:: with SMTP id r27ls727347ljb.10.gmail; Thu, 16 May 2019 08:39:32 -0700 (PDT) X-Received: by 2002:a2e:6545:: with SMTP id z66mr1704536ljb.146.1558021172186; Thu, 16 May 2019 08:39:32 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558021172; cv=none; d=google.com; s=arc-20160816; b=aAbE4Ho8LnFDc0wv1zOUNG6NY3PaddcMdit5vDcRJsuXMYHpWa8PmllF9qjVPWYn9A CuoZL446FdIlHqeLX18zah+TqTGeBtk/uW5LnG7LzSJfQoL9L8h/QDdia5tnkGvv2r+T /pZ0NEbfEM7X/llTrt5n6R8l52ZmqKEfSIjF3lFRniUeS0l9tnPKh6xCWtungmUnf2yK LEE0/nfIdjDxavYE0vqsnW7j5MYdGDhgGqZo15aeImLrQW18z/1SLCNOfesHdqyQLH91 Vx85Gfk/3nbyRnK52JE1sXYfiQ0A9FiV5VGmXy6jbCwne84kno81OIGiYIkDZupxiyFr YVPw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from; bh=f+n8+BkzOndulj1lQCd14ZkDifhGN+IKZaHEjNCrbws=; b=ouxmU4sofQlDkmn35eG1P8hT3gzHNPWTUaWkJSbZ000y0ngpv1uTgSh3vnVKCCyu3A X4/Ux9tfcB1kXL8tIhzQ9V99KbiCQvypCzbfKGtU/No7cwJFKeZ193n7CsnpwmZjux9u adCV6C24LGKOy35hpz5KWclZZdhJ2yF0W9tBOWibXQRzv3XZIFo48a0ueIN0ZL/wGuqP FD51x6ZrSx14wi+22wI4J4U/mNa0hcELLO0cmN7J6udPoalLcIOrzf2xFmHEvdPJGeUB SfTm9v/7qv6Z0FHBUqr14zSKpswaMKExfvv12ADKAZB2GztFOFe/Pg+Mj6F48ioA49yt q4MA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTPS id h3si696630lfm.3.2019.05.16.08.39.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 May 2019 08:39:31 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 2A14C2B7E3F_CDD8433B; Thu, 16 May 2019 15:39:31 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id E741C2DC99E_CDD8432F; Thu, 16 May 2019 15:39:30 +0000 (GMT) Received: from uiwexedg01.ad.nottingham.ac.uk ([10.159.172.13]) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1hRITi-0007Ui-Ik; Thu, 16 May 2019 16:39:30 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Thu, 16 May 2019 16:39:30 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Thu, 16 May 2019 16:39:30 +0100 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Thu, 16 May 2019 16:39:30 +0100 Received: from EUR01-VE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Thu, 16 May 2019 16:39:30 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4607.eurprd06.prod.outlook.com (20.178.10.89) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1878.24; Thu, 16 May 2019 15:39:28 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5%5]) with mapi id 15.20.1900.010; Thu, 16 May 2019 15:39:28 +0000 From: Thorsten Altenkirch To: Bas Spitters , homotopytypetheory CC: Ambrus Kaposi , =?utf-8?B?S292w6FjcyBBbmRyw6Fz?= Subject: Re: [HoTT] Semantics of QIITs ? Thread-Topic: [HoTT] Semantics of QIITs ? Thread-Index: AQHVC/fCTTpdQv6taUilYMlObALJqKZt8+sA Date: Thu, 16 May 2019 15:39:28 +0000 Message-ID: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> References: In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.18.0.190414 x-originating-ip: [86.28.226.182] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 11d32570-f07f-4f67-d4a4-08d6da14aeac x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(5600141)(711020)(4605104)(2017052603328)(7167020)(7193020);SRVR:VI1PR06MB4607; x-ms-traffictypediagnostic: VI1PR06MB4607: x-ms-exchange-purlcount: 4 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:6790; x-forefront-prvs: 0039C6E5C5 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(136003)(39860400002)(396003)(366004)(376002)(346002)(199004)(189003)(51444003)(86362001)(486006)(786003)(14454004)(446003)(110136005)(68736007)(26005)(53936002)(74482002)(6436002)(186003)(6512007)(82746002)(9686003)(316002)(6306002)(54906003)(91956017)(476003)(229853002)(11346002)(6246003)(58126008)(478600001)(966005)(7736002)(81166006)(6486002)(3846002)(2906002)(55236004)(6506007)(305945005)(76116006)(8936002)(256004)(14444005)(81156014)(66476007)(99286004)(83716004)(8676002)(102836004)(71190400001)(71200400001)(4326008)(66446008)(64756008)(66946007)(5660300002)(73956011)(66556008)(33656002)(76176011)(36756003)(6116002)(25786009)(66066001)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4607;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: celB3Rw3K1gOjZGnL2163RaSQrQUld65lROq2h/SBwdVT/2hOZ+l6A0NPQqQ31Vv0xw6esyqX8D2w+Q3NI51dWXoNzHQ0gFENZ8QiFh8pVdDGa69wYv0mSQDCuABdH10V2EnzQoUtU4EJvxVTwA0m5i9DA1iAlaEwtuEyvjWCFRebXO6Zsd9tGQQYuq89I51AlHVRtqE7t3wCznueyZh+P6J8PFy+cveYKGMaEfehC1+/JAuK5Hu0PpfZ4Hc5hAa3tqs70XtjnyNqKn5Yl6fYkFtjmeH1aWotmQ88t7Ig5hdTDeYMV2iCDs2FiTHgkZG2vtpF3yJNdtCagCwm7x9UggRGXUSYtJ96Kq5InuXLTWcpTGdbAr1Aoowjcu3giFhc2krNqxwBUSuUiNU9J/6Q5R0BhQbUygJUDSl+tJDoQg= Content-Type: text/plain; charset="UTF-8" Content-ID: <59C737EB8E8EB9468662B5B58755C4DB@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 11d32570-f07f-4f67-d4a4-08d6da14aeac X-MS-Exchange-CrossTenant-originalarrivaltime: 16 May 2019 15:39:28.2418 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB4607 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk 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: , 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 a= nd Andras) which is an intrinsic type theory such that a context is a repre= sentation of a quotient inductive-inductive type. The formation of Pi-types= is restricted so that you can only form strictly positive types, it is ind= eed a special case of a directed type theory. Now the semantics are categor= ies with an initial object and it turns out we can construct the semantics = just from assuming the existence of the theory of codes. The category assig= ned to a context is the category of algebras and the initial object is the = intended interpretation of the QIIT, equivalently we get the expected elimi= nation 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 universa= l.=20 One would also like to interpret QIITs that are indexed by "external" types= which are already defined and in particular include infinitary constructor= s. One can extend the theory but the semantics suffered from a coherence is= sue. However, I think Andras made some progress on this.=20 My view is that this programme can be extended to HIITs by considering high= er order versions of type theory and in particular the theory of codes. How= ever, this is maybe an overkill, since one can normalize the substitutions = (make them implicit) and address the coherence issues this way. I think tha= t 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 beha= lf of Bas Spitters" wrote: What is the status of the semantics of quotient inductive inductive typ= es? Looking at the literature there's some progress on reducing QIITs to 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 Shulma= n. =20 https://ncatlab.org/nlab/show/inductive-inductive+type =20 Do we know that the prototypical QIITs from the book (e.g. Cauchy reals) are supported in the usual models of HoTT? =20 Thanks, =20 Bas =20 --=20 You received this message because you are subscribed to the Google Grou= ps "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/ms= gid/HomotopyTypeTheory/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%= 40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. =20 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.=20 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=20 where permitted by law. --=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/99645C4A-A893-459A-B027-5607E89A37EF%40nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout.