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.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yb1-xb3c.google.com (mail-yb1-xb3c.google.com [IPv6:2607:f8b0:4864:20::b3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3f5bd81c for ; Thu, 16 May 2019 14:57:37 +0000 (UTC) Received: by mail-yb1-xb3c.google.com with SMTP id d10sf2999836ybn.23 for ; Thu, 16 May 2019 07:57:37 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558018655; cv=pass; d=google.com; s=arc-20160816; b=PReA6Id3V56rkDXrIH11il9035jV0IUIXnF7MWcOI71SVPz/i8LctKT9VzVCz0U7h1 LuQxZNNgsVQvUCDVm9266C9PBokt1t+Ji4x4sGF33vXFBkgfQHDba7i4VOCewDgExedM 6bXwd2ksPn0ZmVnxm6R+9nn1ai2aAk2Em6/FXs0Vd44F7xrgsgaRcz/G1Y/Nd9RV8YuR 4InAI7wSUnT78vIaAa/cmHD8hXwLL+1wqo18LmWr5LYGnRZZUJVNQOcTOqhSOvidNW+B vK2UuEO6bW5M7ssj8gzfKf+2kZ7Q1CAcw9mEMqytyP/i4elqQ2hzfElqndiWyVChEkqm uMhA== 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 :mime-version:sender:dkim-signature:dkim-signature; bh=8prE/1Gb9Pv8bBRBdtGjzzPDfVlbUxt62x1PhRhVpvk=; b=M+NafChMurBV4MOiBdNCXR0U4ga/IUv3LOVeFUhgRL4FnvE3DT9uELR3wpWEQOMz3x 4jtgqY/fu2HIB6tcPto/C/jh/TffviUq9d+bA08niprDgccdpHgo2ZxHOvxBZMi3UTEW 3cV0pWeEYDh0+nr4ykoU9rqkp+OrZjCYn1pbzLSEEPUdBf+ZBMXtrmLXupd8q0c02nzK R5JX5rY4lqql8yeNMZJRqTBvTELca6dN+uBFaVVdsiGUPLavrR1BAXfnCCkgfwX34RsK ejGlmbDqfbNw8O3XU3R+Bgr9qiOeKxfV5tmeMIlNlWufGvetQvWAWZB5Ym7Gafor24vz WMRw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="R1Alrk/s"; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=b.a.w.spitters@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: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=8prE/1Gb9Pv8bBRBdtGjzzPDfVlbUxt62x1PhRhVpvk=; b=JPnpE7VttTnx4HRZzIEVzfsQY0IygFNL+27qAHCIEH7RvWy9tRuBoA9gnGO16Q2zxZ Cpc4cZ2wlZyOPj3Ch9Z72MDQ99dLLqRqyjLXtza7sZk6Hf34+/Zdj/E1Lvieapoc8dz+ vi5O999xZd2lSmjVrQPyoNJ7cEsPluUr4Sv/T287axTI6/QJIkAaZW2qNNQssdE5mV3z DGdLi1rGjrBq81lmsQpF3C1J40qMfFLBYQDVWLWjPTZ3DDA+eyjD6VUjx9Z4nTpZC1/W orWR11ocLz4C334ShQ2YLPkASkSaevCLnr5mD9dNrrxuaMdHD+CBWXy0eYxfnoJ+b3Zg d3bQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version: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=8prE/1Gb9Pv8bBRBdtGjzzPDfVlbUxt62x1PhRhVpvk=; b=XSOyOnz6iQKnjDWgOeyiKk8GTtc5NafTK2IhM4FGHnLJETocw2uFF/kSZV4g3qS1xB 6krFRwoS8BuBwZKC8vC5bZPfQM2WyoxhnkiwAJjcVtBNdw3tqXgB4DrVUNTw7mVzTFME nzCBqmijN8JLEOjsglEikg0oAiE0zYi1a6EkW56LQjl9YOmr/sOKOn+DJpC8hWQc79RF iaTN9eOKR3ACOQJ6tF6tAm0d8w8bKoTv9MBCZdfgqAzHVs7pZAgGeGWrcrzQF4ww+KRa wftatedmm+ppsCb0GrrOGqiy2ObpfjL5bDip3SPR9zPUrEQOOBIuK41vILFTJpywC19F R+Cg== 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: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=8prE/1Gb9Pv8bBRBdtGjzzPDfVlbUxt62x1PhRhVpvk=; b=Rmfk3Cr4oyLlXYsdhdsBr37wRnfSnvT0RwO4AqOiFH24wwhYbAoIGj4U4fqbMqWx51 5Eund7Mfa75FPlPJcnTagXF8L7HdTLbRlw+CLDSJFUdjAMu1RR3/VyN428mFtPuqtE5y ru6QfGY4gbAcVGytn6hb7WiWleyS+/wvboqQi9d/tfLR6n1hWC6QhgZSAMmTuVv2+pvB tPTTWD9ZulxgNsmBt71sCzuqMlWSHp0yjQxMX+mJVH6b2qZIYslsJjfDVK1p0C2QDn+B gk2I9XgUiiH+G8rWuiAu3PCfEgU9U0V/BDYrLyiKOxzDnpsDAIAp2RWFjDQ4pae5EJmP EFXQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWDJI7wiDr6uibPd98591pjPBDC8MxDJnd5NNiktf1jICZYEROQ eTBHDjNwIgAHJUEY5POX1x4= X-Google-Smtp-Source: APXvYqxuatNXTl8pl3/hnGmr65xmX+UYPz34e2WyTK/auB7mHrPWZuXog+uE/gThSfxZxkb4ni+Xew== X-Received: by 2002:a25:cbca:: with SMTP id b193mr1742731ybg.27.1558018655724; Thu, 16 May 2019 07:57:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:330e:: with SMTP id z14ls683620ywz.11.gmail; Thu, 16 May 2019 07:57:35 -0700 (PDT) X-Received: by 2002:a0d:ddce:: with SMTP id g197mr19571885ywe.335.1558018655277; Thu, 16 May 2019 07:57:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558018655; cv=none; d=google.com; s=arc-20160816; b=kufc284JFehBdso1VRODwtFOGacehZzSt+i12sCLvqpnjguopEGVM9XRvhRCpYp5WS Uxdm7C5WjfQ3y9r714wE/txOIQcbEcd5AFW1dqVNJWJn06WF+A6bfTqK8DThcmTYLM7+ zHnSTu9uXx24iZ+C57LrJK8jnRBi+HG8b8jOqroDkpVQ8odCVSbULrDlbuTNlOTCmuPk FTzbk6Knh8NH6i5VefF1rWSipJFQNYhB/bqvUWn8pU9dxO9K/OjHyd//tekyQf3d7sN+ IvDuJu/UA99gXYpCqX2XYiLRdOOrT2wgQnY63lMscNB+CsU5NVT/Il6OJDnTu6Qa1Spc ikDg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=1CP3c1Qr4oNu+FpAtmekpzTOKOlTcAn85U1+R6Irc54=; b=0x2b+gN1TRZtxjZTZegtrs7EOaNiPg+zVbHKXJRFDjsDqKjXGTHwfhRGJ4pbtNOTZL ur48ncrZEG0t1EpUNyJHGkxRDyKeXmjBeW3KQPOyDluR2FyfdM0Q1SjYbKMf1Y0PcdnZ 6ic/rdGSq/Tc4+0386wbAZSs9B5F3FrdTXmUZOMnSSVgKdAyiDEw6YZcYlbrOHz6tWKp ntO4hObg4KuzN5TyCXBgVNmYc9gMP0lNvOn5zVdC4FR39RhjbI+lShKDmTKfXp0qodEr XbvU4XqVTIoEtGBXrIsY4e7ZhKCdIRfYw11Bbw7LG0TWbOjCooTgQ4V/CQcqAYaqYqR7 TB/w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="R1Alrk/s"; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb2a.google.com (mail-yb1-xb2a.google.com. [2607:f8b0:4864:20::b2a]) by gmr-mx.google.com with ESMTPS id a193si586902ywh.3.2019.05.16.07.57.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 May 2019 07:57:35 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) client-ip=2607:f8b0:4864:20::b2a; Received: by mail-yb1-xb2a.google.com with SMTP id k202so1374737ybk.2 for ; Thu, 16 May 2019 07:57:35 -0700 (PDT) X-Received: by 2002:a25:b43:: with SMTP id 64mr4337424ybl.175.1558018654724; Thu, 16 May 2019 07:57:34 -0700 (PDT) MIME-Version: 1.0 From: Bas Spitters Date: Thu, 16 May 2019 16:57:23 +0200 Message-ID: Subject: [HoTT] Semantics of QIITs ? To: homotopytypetheory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="R1Alrk/s"; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=b.a.w.spitters@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: , What is the status of the semantics of quotient inductive inductive types? 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 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_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.