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.1 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-it1-x137.google.com (mail-it1-x137.google.com [IPv6:2607:f8b0:4864:20::137]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3bc4ce9a for ; Sat, 16 Feb 2019 22:27:09 +0000 (UTC) Received: by mail-it1-x137.google.com with SMTP id q184sf16460056itd.6 for ; Sat, 16 Feb 2019 14:27:09 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550356028; cv=pass; d=google.com; s=arc-20160816; b=sJUsK2aK5RrL4/+eBBJwnBd9jQqEv3zx6CIAQbzt2mZdgv6x/gCaiBMn3fSNO7rm+n rikQ+enNmCoYHwsgBfmDm0nvpQOQ758YIgRWKsOkvzghM1RsgxqqTbvv5OIyGUi3ykXx c+PhpIQKDp9F+V96z4JFpcGOX30+OhhSYllFCT0fNwXeGYCMKkZAE7+BEJW9pDrXyRiT ++4ZvTl+xJoDyqtlS+vPEjVuxy3zgnm9/Ynf8wery7afUSIddW5BVuVs56p83TWlkoLO mWsNzXEyTjMtTT9S2tC/kQWiAikMuHBDxA8ngBhwYRJOtoSirTmR+GjWAgTJ7GzPmp52 CqpQ== 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:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:sender:dkim-signature; bh=sax9QnULPHR1ric/qIX8ZdwcHHswYGUV7m1bxHX7mSI=; b=H/4A2WQ2b3BaFuhx1lUiy/clUOE7JF6JrVXHyNZARYQUMQMpJXDPEKiyRXGTmbnoHV scsAaOnuYu+TclBjUqJFy3MJ0XU+QOqepVd6TBRaV29CvayX2p+PCTqmXw6UCIDCgqcC w7u0kYeBNOofMixTn9W5oafDGsU2GF97rFUQuz5i8nX10tb96Y6eEad7v63mL6cwbRxl +m2tD0A7TXlHRVfLD3M8G/kAwCCt26rkZa26STE2U/iTxgRnKTJhg0nZ1WbIfVph9NTB 4kPmUJXiN9L6KqmHpXaknMwO3gAVEy5dnl86Tg1+6j92YoE7J8edd/aBT+zelgmS3Gvb Wj5w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=K5PPLERt; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::835 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=sax9QnULPHR1ric/qIX8ZdwcHHswYGUV7m1bxHX7mSI=; b=MZzwbE0APRQ+Dg4cHdN6bYOMvEf4bfZClysiUsy5FTqN5/qo2lleGdciqRsz5nSMuk YEAadfk7LsOxgQ8XFVVdL5bjLyftHdVkoJQXJmjlnHX3PWPpjYWKh2k2Nf6V3mLGecKN +wZGo/xj/ZRSQVLkZglLRDma6GAfyY+hDUlFU0/FDwkRn7cG7i6NomtkwBLXJL7waPcK alIm6V7Z37Gla3zknHH6LEtK4Gdh4qV2+bdqZaJPqlueKG+sZuOOtHujGMCTDsxGOYKJ 55FRC6mdWVmBvW7k0EP5MoeugIPsEdWDMij0ExefohE/kCKWDXMcSZN0/gjT6dIwj2vN b24w== 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:subject:from:in-reply-to :date:cc:content-transfer-encoding:message-id:references: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=sax9QnULPHR1ric/qIX8ZdwcHHswYGUV7m1bxHX7mSI=; b=A70wyrb9iscszNDFHR0x/M2HXvpyI2JBUqMylBbVPmG4ov3RLMQbnbHtxIcf3UIuTR Q5wKAWxBHZBpc+c+y+YvqsYpvKBxopdQGaNM2zOjlf/N0RYFQH3FtCfFYzxbck8VmunC 23xf8cvgvZlbnj7CBiEtwsG+riBsRgzF/UgMyfpE+CqO5DXZRbL/WgNrbUny9wsgneAq twIwMRaxBBIF6KUjoCUrf4hyR5rhfOOP0Q4jUTNMO6HIuqDJGj/YmVfLZAH0NAU+N02l 0ldzPFeFqs3LekHaRCGE92S7TWGGqMz0iAg0qxmdC6m8HSWvb1M8EBdb1cc2aH/YJpHs Nntg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuY7sY7ITbZ9/2snwLTg+JWShpJVK6Z2+uGZZptafAg4CPnu7y2J Eidf0n1xa7lD17b6Op7/vDI= X-Google-Smtp-Source: AHgI3IZUGNOaUYY0Wl6rS91FRw13Uv+PPiTy7UY/gqVAHYm96/ewecyla5BeONr6ok22foYiI/Zg2w== X-Received: by 2002:a02:1601:: with SMTP id a1mr79057jaa.0.1550356027829; Sat, 16 Feb 2019 14:27:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:6c09:: with SMTP id w9ls2641731itb.2.gmail; Sat, 16 Feb 2019 14:27:07 -0800 (PST) X-Received: by 2002:a24:7381:: with SMTP id y123mr9132506itb.32.1550356027288; Sat, 16 Feb 2019 14:27:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550356027; cv=none; d=google.com; s=arc-20160816; b=p0uTefrb/Lz3+POlgYuUPsZGNu8zOHPqnw/BjECLirf9Ze/VauaZOrwxjoNVk/D+wW gu7eC5JJmyRyQF2cJ7tlK/mi59bkveskzkw2QAN5oLe0CMaWcXDJ80yoCtbBJH/LfrFC Eys5l/RL68Fkmpe9SEjVNAmjoKPmqs+sJmWjkhEsksQEiygqabZR67v3buDqR/flU0AN dGmDvcMT92amC328uiHCHR4ReXfRz8HXcHqrQEIgCmeAhI2kSWtECE0PaiE59HK2tK5j BJ4uXT0fdxr9e2kxWAwlM7ik1jyNhSHgWsjYPK909X6dKX2DZvTdNcTuU4oV3rV8eT8Y aZdg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=WjpcmY+HpiiVbxMMHY8MTcsZFHVXr8jXsKQgSEvouxA=; b=l2q8G166CExRbA9VRlYFa6pgpmQtPWS/0t62qVVfDP/Qn/9uGhe9bmjD2t3fHJdSga oMjAPWjOM1HY6KDzfgvdS+3kVpZYwgDzWk6qja7ZTcG1Ny1u1xJO3+7kvKxxGb0w3N0u q0V34TM2rkFin6pORzgeMFjaRMzHLd7g3ziSaFMpyohIVLGBFpvB3p0aIlHEUmdQMed8 Gy+JwCircFQzMDK//X4UsqiFjIwER/owYfR1rbZDiy/iGWIRVYJnTaC8vRoZSZFYmFek 6BXtgAsOg7Ry5HFvZdQGGFbIWXXD4UZuMZDYOSqAqmbY+U5q+hcsODD5WWQ12S6aHxsY jd1g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=K5PPLERt; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::835 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-qt1-x835.google.com (mail-qt1-x835.google.com. [2607:f8b0:4864:20::835]) by gmr-mx.google.com with ESMTPS id y7si482785iof.5.2019.02.16.14.27.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 16 Feb 2019 14:27:07 -0800 (PST) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::835 as permitted sender) client-ip=2607:f8b0:4864:20::835; Received: by mail-qt1-x835.google.com with SMTP id p25so14948638qtb.3 for ; Sat, 16 Feb 2019 14:27:07 -0800 (PST) X-Received: by 2002:a0c:d947:: with SMTP id t7mr12501758qvj.49.1550356027065; Sat, 16 Feb 2019 14:27:07 -0800 (PST) Received: from [192.168.1.110] (pppoe-209-99-217-10.greenmountainaccess.net. [209.99.217.10]) by smtp.gmail.com with ESMTPSA id x17sm6086742qtm.43.2019.02.16.14.27.05 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 16 Feb 2019 14:27:06 -0800 (PST) Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Subject: Re: [HoTT] A unifying cartesian cubical type theory From: Steve Awodey In-Reply-To: <20190216195136.GA11255@mathematik.tu-darmstadt.de> Date: Sat, 16 Feb 2019 17:27:04 -0500 Cc: Michael Shulman , =?utf-8?B?QW5kZXJzIE3Dg8K2cnRiZXJn?= , Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: References: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> <4d63c003926b2c19e530c107c5b141cd.squirrel@webmail.mathematik.tu-darmstadt.de> <20190216195136.GA11255@mathematik.tu-darmstadt.de> To: Thomas Streicher X-Mailer: Apple Mail (2.3445.9.1) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=K5PPLERt; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::835 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu 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: , > On Feb 16, 2019, at 2:51 PM, Thomas Streicher wrote: >=20 >>> I think the idea is that the model structure is constructed / proved us= ing >>> ideas from type theory (like univalence), rather than that it is a mode= l >>> of type theory. But I agree that the terminology is confusing. >>> The methodology is, I think, due to Christian Sattler ??? so maybe Satt= ler >>> model structure is more appropriate? >>=20 >> When the interval is fixed one might speak of minimal Cisinski model >> structure since it is the one with the fewest weak equivalences. >> Of course, Sattler studied them a lot so it's good name either. >=20 > Well, Coquand-Sattler might be better because it was first used in the > [CCHM] paper. From the many anodyne monos of the test model structure > one took just those which were syntactically convenient. I don=E2=80=99t want to minimize the importance of the work on cubical type= theory=20 =E2=80=94 which I believe is very great =E2=80=94 but it has focussed on bu= ilding models of type theory=20 directly, often within other type theories, rather than on building Quillen= model categories.=20 To be sure, many ideas, and some terminology, from model category theory ar= e used,=20 but without showing or even claiming that there is a Quillen model structur= e. > But, as far as I know the test model structure also gives rise to a > model of cubical TT because its more restrictive class off fibrations > suffices for interpreting sytax. has it been shown that the test model structure interprets Pi types, univer= ses, and univalence?=20 Steve >=20 >> Unfortunately, we don't know when minimal and test model structure conci= de. >=20 > Thomas >=20 > --=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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. --=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. For more options, visit https://groups.google.com/d/optout.