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-qt1-x83f.google.com (mail-qt1-x83f.google.com [IPv6:2607:f8b0:4864:20::83f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6a7085f8 for ; Thu, 16 May 2019 18:50:27 +0000 (UTC) Received: by mail-qt1-x83f.google.com with SMTP id o32sf4144295qtf.1 for ; Thu, 16 May 2019 11:50:27 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558032626; cv=pass; d=google.com; s=arc-20160816; b=rM+BiaQ2a9c1wn5gBzIAf8Mrho+8yFMAVAHN/c3BqWhyb3RW/85wjlkcbqqO74ZaA/ O2VoZBlKdy2fllpWlwvqelq0hjukarEFmXmX/4uO8Yl1bPSc8R/pvnD2/ITtpbMspeKj hBXzRGhhrHZB0+LcdDW599oP7i5D10hN+1LF+Pxkq6gyxOMGcZSvu4ZumtzOOycMiSQa alxMBmNTDhh6hjIYNFFbPF0lkNZkK4sexsfplu7wnkQsiFmHooSacEuOJ6UrP2SX6eXs hqwn6qgQogDdJ9lHJStDjKqxm3leRXE6xOrZ7gjizmOi9KAd9o+PQsodEfV52LXPOtxU Kg/A== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=04G/DMdBr2f775NphCLYLSgTMxWynbHDg2VpvMSXqlE=; b=RSeum0uUBjE2uk3JXTuBUhRoztB2+fi5ppwhJclw2MeUzEnB9Q1o5ceP6VAC2LAs3E grbww3k7E9Qlq3/UkXHxbuoEoDLvRzZWKzVT5ZJv9BywPLA+Rf+wsBhRx2qKzYRfR0Ei PKMdK6uPDWXXbxbNrWkiFh/kIfcdYNCB5P2sWkazTJLyBmLuIgmW1IvPb+Go0cWebIMR pfyoVduoFHvoENFFNP6d3KrwD3pl7DCBROrXsm2m4cU27xEpYB1Rdzjhk/THPDOXMaNM pZCfawHsdA8gCtqsoJLyVsYtAuawU4X/mpdPApZR740K2u8B2P+5zBPqSiwjyMk83FwW l/Ag== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=TcFKhJOj; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 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:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=04G/DMdBr2f775NphCLYLSgTMxWynbHDg2VpvMSXqlE=; b=rdXvbT1g6zdkh3lYzy7FK14pUGoZRUF/D6MkhqH5WAvG6bEtrDsMzp9mi8tbNqj23E lO09PNg6wp0JE4mD1za+HAiV+kpGYMd2v6dAMn6aPyy1+0wz/qHGD0LvbxCge/iL1HbN Sooi6UZZw4hQpGZn2YyasjnX/rZE9SNivZmHRN398Wt45CYyXxcrlNQZbrIZ1D74kqGy n4MP10kpe0Jn3V0wGzd/Mg7xYsFlSJMuib2NbEJtR7UnjH1VoS7xf5R91ETkudkxSMWS L1I2T7dbsrBB5kC9/zdTcOELs01K70Ny4IRq3yyxcUiJbPv5cBFCzkaH5ZjAJ/Nc9xbJ IeGw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=04G/DMdBr2f775NphCLYLSgTMxWynbHDg2VpvMSXqlE=; b=VfFT670ZPdSDPzdCT1ELCL8B1+/GSlG1cj6RgPWFEMlQm8FuRhkNBXjNC0gxsTZZ3M A0WK3rp9+gbxIX1u7uwfIKFSrCQt/XpP/9qYdUUrjAFI7WrZsKP0zH8ccP217//34h9s gG6nSOvbrYrpMeOgsrYARZ+TMd00XvAsFu6j3dt9G/2ezJqYwIa9o2gkDau5H8uGtq0W XFo9Z4mOvSv7GqJ1t3T4qFwrDIRJ2RqvKDtVMYO+DWyCSI18kRRS0E9u5ZWZc0RTMZyA VYk6YO+9+K3zm1I+vbrdrJuGGhMXEvYq1MMR7ebwPobb8tBdYr9EJqvEY5l83JDPCZRR pYOA== 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:cc: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=04G/DMdBr2f775NphCLYLSgTMxWynbHDg2VpvMSXqlE=; b=P4EfB6gvhnxrlhxCJSeEjztOZpZ94RqGPQx5pNTyGsAvC1PIPYa2kcPC4CPpSZbyQw V1eKFNTH93dLSmjj4IgKuB+y5/XIJxK3SNeIUolag+EkjTSF1fLAvEue1V9SfoQGXpFD JQVHrsNg94hY5GHT5UqpCWd2V+kBIDxbgIJ0XHC4GdEVL4cQAQvm4+O7kqxIEOix1wE+ 4eoUR8qxUbHxRV9Ip4Ky4/b2TOeFCqcYpa0ZE82T1EKc/XbJAkNQA8ztekcT532AK/iH XwHVqB0tXKhMgdakLlX3p9I+IpUIX7KZ7TltG3BiVJy/MsxpY/z4C9XI7pMV3qJS6qYR y46w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUuiiGOcMORm+YFRNzXA1HQPHYQUvuakxpZNnAOynVMHr+zOrlS q3T5XCnb/IX/4cjYG43IInk= X-Google-Smtp-Source: APXvYqxSodMZqyrlQAUgS2W8Shcx8P5oV9QEAsezU7VCSw6748jcLf2YQPw0wjTp4Wz8ooCmHUfOMg== X-Received: by 2002:a05:620a:1206:: with SMTP id u6mr18584131qkj.88.1558032626335; Thu, 16 May 2019 11:50:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aed:3685:: with SMTP id f5ls661140qtb.1.gmail; Thu, 16 May 2019 11:50:26 -0700 (PDT) X-Received: by 2002:aed:2665:: with SMTP id z92mr10092497qtc.368.1558032626134; Thu, 16 May 2019 11:50:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558032626; cv=none; d=google.com; s=arc-20160816; b=g69vhlEsmYcn+r0dR7oBXgVkPlyCpjDbwXaZERZ6U5wcHD1MPKeNJu4+PJSeYcwplS k3k5wwXzrq/jOUvHgmfs3LgD4zxavA2FIMBMDZ50Xs+EzmPFOQMCrJjKZAeHv5tRRjjR WG/OdNr+Bwguur3mOHCURWALdpa1Nzes59lfUtgatwlQcxK5ZS+pIQAxBUaCjvMKsY7t V7VGE/DB8lh82N1D09ELdvMF0DY1S2EMYeDo5RaR/BIch74nM+/7v1ci27DxrFBxNIoq ALcI1S/CqWuEwLUR0kl9cEmIBVR6iK2u6dZMCEmt8sKiihglvd12pnV0kd2fZaUwkDat /o/Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=9dBGH5WIpkf1AfrVtzB/yFmeg9Y3CdjPUA4Bm099LrQ=; b=F4xJnZeLo4pfB1xg4DaHKPPB26FSYo9ATYjxa0Cvs7H6jSIjBrHMZ1vWwZSXhvxThk 8AeNWlWN6uTAmf76K+nC8aE6V7x3XnUd7S0MqNedwTjR2lOOreLbdEF3zjlU78BXhu8R jHnS/bGwFf7M7W/3RZuAVIPMpUsguQIGv1J9Kz9w4YplmMkwg/Fpl/pbSgYeq06qrg/F I79ZpWvhqfb5uAUaR3nFTdaLS7wH1prPubPH9FVPPeUzhOCDnbpnfWAZOG/2y4G9ofbW hZVQgSQziSP6UBa0BxzEP7/WQuX8Rq3+9mLwsHGINMJmBxboNDXjDIJJNiskMYmEXKS+ QLVw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=TcFKhJOj; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 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-xb29.google.com (mail-yb1-xb29.google.com. [2607:f8b0:4864:20::b29]) by gmr-mx.google.com with ESMTPS id m20si494568qtq.0.2019.05.16.11.50.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 May 2019 11:50:26 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 as permitted sender) client-ip=2607:f8b0:4864:20::b29; Received: by mail-yb1-xb29.google.com with SMTP id t7so1639335ybq.10 for ; Thu, 16 May 2019 11:50:26 -0700 (PDT) X-Received: by 2002:a25:5508:: with SMTP id j8mr23572467ybb.448.1558032625715; Thu, 16 May 2019 11:50:25 -0700 (PDT) MIME-Version: 1.0 References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> In-Reply-To: From: Bas Spitters Date: Thu, 16 May 2019 20:50:13 +0200 Message-ID: Subject: Re: [HoTT] Semantics of QIITs ? To: =?UTF-8?B?QW5kcsOhcyBLb3bDoWNz?= Cc: Thorsten Altenkirch , homotopytypetheory , Ambrus Kaposi 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=TcFKhJOj; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 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: , Thanks for confirming that this is still open in homotopical models. -- 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/CAOoPQuRVR1A84pFE67GndjCHcUUV_vRCQ8UWdndai%2BzoiqqjZw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.