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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x540.google.com (mail-ed1-x540.google.com [IPv6:2a00:1450:4864:20::540]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4d4fa5ab for ; Sat, 16 Feb 2019 21:58:17 +0000 (UTC) Received: by mail-ed1-x540.google.com with SMTP id x47sf5349159eda.8 for ; Sat, 16 Feb 2019 13:58:17 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550354297; cv=pass; d=google.com; s=arc-20160816; b=kmKFXDkO8L5qcM0pPAsMuidh4S9gngHzqPjJyhR+WX3EhU/2uLQpbfL/lei8utgghU tXs5aUYUVGG98BAFvqwY3QXloEvgaY+Qso4WcWtJ0RGlwtyRrnMssJ3kNuPq/oLPguRB nBYkVXjvm7Z1+aJt/gT/4n5NnL9Q3auTbvb3yVTaTEwETZ0g9rcHaurYbH13mWGtfDC6 SmtSwIGgZKbTFW0T53hWqZRg5pLQxCcuU+MOhHWJro0HGx9J/Hxx5L25JsUj7eXZNzAJ bMZxsPd33bcuY/jqU+ndGyQOwr07QrBjAtF1BtYTwbk3kypru1FzW4KtLYYGCt2tA0Gv fXUg== 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:user-agent:in-reply-to:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:sender :dkim-signature:dkim-signature; bh=Pl3eD/TT6Fg2D7vmSNJEKWsxM2l8lYaoalu/cLx/6VQ=; b=KlNNoZD+t/SnS5pZumk+Zx9xN5vzGMUE5vEGOsyhBB/7N4ytIknRV0/ExKO3dZGMBJ M9ud/dstJk7eXjYX4iwck2KskScD7vBEgQFrIoRJqJiy80tyXkG1EDLLwnHZbso8BkJi ZK6gFVL1PwYc0gADJJ84zM4defOGLOtz1DreC1rR3MefcECQTbZVCw4oeNBLBpNef5HP xxTlQEht7YCus1ssntToqjpxlwmPzOxz4idyX1gWR7Fx7EQISywJti4F5s5xPY8zh0Tz YTNRBuzQKgjlcKtzOdbVtr++Pkzq0Vy4hLohrO2SRuL2REjztIkxBY9lsNq5Z34t54qL kGWw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=X4Y+DpCA; spf=pass (google.com: domain of rwilliamson62@gmail.com designates 2a00:1450:4864:20::136 as permitted sender) smtp.mailfrom=rwilliamson62@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:date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Pl3eD/TT6Fg2D7vmSNJEKWsxM2l8lYaoalu/cLx/6VQ=; b=WeME17g+MmwRNOrx4PZiqIaZHI0ZRSmrMEgijs4D3+2uMfi9spL8PtNxthwo/vJWUU G9UGbEi7gVfTCzR7doZL0YrKVQgPjxw8AVI9YgcR1GoaEgupdak0pOZE/6uHLISGwH7K 2Bi/yKzpDiRhPqeKlvv+4BvO0adMfs4BiDiJKwlB6rI6gQ8sichLdIs4mdF2zPZ1t281 +VD9kdazpvkz4daijJCXpJBTrQ1BPpTJ3hL4bn3sLQl2WvLEnmd6XjI0paYi5r9jkF5E FTs0g5OBXFWRz4R6qL8VGipBGtvBXZn398pq6OwDeiahlkcbvYC2DiqFHE7IUjBVT7Ct Hkvg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Pl3eD/TT6Fg2D7vmSNJEKWsxM2l8lYaoalu/cLx/6VQ=; b=G3qtg/zcSpfZnbk8nj8GjlZQVzdyrcYSJ+I5/NNBIyuQciUOL7YKGQtrJRkbuCGqUJ 8WhkE4zx0AN3L8Lk90QqG8/BGXDnRSrQOOTtYbalATEjJZjFmNmIbkWIkaQku37C9KPb y+pc5VT+pnwdj0RwuFmQg6C3FFhTyG1Iw8uGikVVuJ/cGfpHfQ5P17k3WKFONfoTFIhb C+NuJ/x9bb5bTiXyVza0MMUHMlqv7ssHuRzJroaIz1/FkM/tnb09ar1B7Y9MBZhIfSEr dzj02zcnO+KcpY4dGNMC2qDe+z89wDprriAn2SGKZi0AeMP8HqtWJI8KLq6w/ttYAVqt n1mA== 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:cc:subject:message-id :references:mime-version:content-disposition:in-reply-to:user-agent :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=Pl3eD/TT6Fg2D7vmSNJEKWsxM2l8lYaoalu/cLx/6VQ=; b=nQqCHc5gct3zwBM84w/v9z7YHgr77at+GHx5o01bOlMpCTcM+e3ZAhE7mp+qJ513WW ruBpUQOySNJnrUcKjgSP+aTK89yqXA5uFWQgO/h1NrhqrVhgnf00ELOWYRRPCd7IeyyM TpRxjne+TQa8Mlyrxo070csY3wwOXzzvS6nQ1NmUyRauTKWz5GcIiwwRmISUDfm+l9yb yZa528QKXsBBbD7CDcVdaZzmNu0I57u5pf5yJR9OaMaCXdblg2MfQYr7yoD1gLVW0+Mm a+jofa5CNRM9Eb1NfBFK2SNtWeyPoiHbapTvg3voo9VXJPdNgNKpVXxlfcuPJt/8BFXA h90w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYAoTVoZklnoqqyv2a57RrMHegHPujSOhjTl6/b87Tm8cy7b6IA D2AeuNipDZg1TkyA4YXUkZk= X-Google-Smtp-Source: AHgI3Ib9mqNdNr0STuEui4opAElfMyoTDl2qPQ7BqOWALM357zwvoRT7gQPS/uHU1Pkn5xSAp+EQJw== X-Received: by 2002:a50:b130:: with SMTP id k45mr51672edd.5.1550354296905; Sat, 16 Feb 2019 13:58:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:8863:: with SMTP id c32ls1462222edc.2.gmail; Sat, 16 Feb 2019 13:58:16 -0800 (PST) X-Received: by 2002:a50:b781:: with SMTP id h1mr1940326ede.3.1550354296517; Sat, 16 Feb 2019 13:58:16 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550354296; cv=none; d=google.com; s=arc-20160816; b=H0HX7g68alxBalEes2rEwXnqsvTEn1UBpKTcYSo7iuNKzg0SKKv0z0c1CRxDzwy48G Cw9u0Qr/KGbA3xGYI7ZvDQvQRlWoCQ9r4IrtTKCjvvArFDfZMl0NJhmxbaU4jueq+Yst oZZZYWH/i0QzDQLnQu3P/7cXCLVoECs2ITRMBA8SdBcwsV+xP0Z3vSx3yBmmOyXMym79 uYZtkru1JEuN23/HHt+oWVbGnJYpYJ0i6SjaGpRQgmJCwpfN49EaAMJOogrmpN8kkPu+ kcLjuAopbdwAVOpztf2StmyFUgjvWX0/yPYP54nJJpFu521aby4w78KTWbwOF3d//H04 /HmA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:dkim-signature; bh=lfnJrlM5dIGKzGYEGODbpzrfJqeAYRTMFzMpRAlD6Fk=; b=EbuLbwlYx8A1h9Pv2IiAhK44EIsC7JBrYynaU2GBEif9diCX569z08D7UN5TACwCoT JRAmTJXspzmhYltSzPh6E1VY7RDUZozi0/HsGyrHLHJlOg9k41a9dvR2poelII7GKnoD QM8E7IBM347RJLS7du4q71ygoDhpfZy0/D2UIk4xWChl3wIlFVkAzQn5SNTncHLF1mIR vfpRhlAD2uZZ7UyCdoOq2wrKgSi2u2DCumrSHOItTQsasMUfJPzNmf1dsjBIEXbZ2F0G B5xy3j2wKg4d3jlW6AemNp6UXMC/UNhBz0L2EnRz/aUTQgl5Yy9+rOInednGL2riWv7d YTGA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=X4Y+DpCA; spf=pass (google.com: domain of rwilliamson62@gmail.com designates 2a00:1450:4864:20::136 as permitted sender) smtp.mailfrom=rwilliamson62@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x136.google.com (mail-lf1-x136.google.com. [2a00:1450:4864:20::136]) by gmr-mx.google.com with ESMTPS id c7si140043ejx.1.2019.02.16.13.58.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 16 Feb 2019 13:58:16 -0800 (PST) Received-SPF: pass (google.com: domain of rwilliamson62@gmail.com designates 2a00:1450:4864:20::136 as permitted sender) client-ip=2a00:1450:4864:20::136; Received: by mail-lf1-x136.google.com with SMTP id v7so9693699lfd.2 for ; Sat, 16 Feb 2019 13:58:16 -0800 (PST) X-Received: by 2002:a19:c942:: with SMTP id z63mr9301935lff.162.1550354295903; Sat, 16 Feb 2019 13:58:15 -0800 (PST) Received: from localhost (109.247.202.84.customer.cdi.no. [84.202.247.109]) by smtp.gmail.com with ESMTPSA id g194sm2562333lfg.55.2019.02.16.13.58.14 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sat, 16 Feb 2019 13:58:14 -0800 (PST) Date: Sat, 16 Feb 2019 22:58:13 +0100 From: Richard Williamson To: streicher@mathematik.tu-darmstadt.de Cc: Steve Awodey , Michael Shulman , =?iso-8859-1?B?IkFuZGVycyBNw7ZydGJlcmci?= , Homotopy Type Theory Subject: Re: [HoTT] A unifying cartesian cubical type theory Message-ID: <20190216215813.GA1514@richard.richard> References: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> <4d63c003926b2c19e530c107c5b141cd.squirrel@webmail.mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: <4d63c003926b2c19e530c107c5b141cd.squirrel@webmail.mathematik.tu-darmstadt.de> User-Agent: Mutt/1.11.2 (2019-01-07) X-Original-Sender: rwilliamson62@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=X4Y+DpCA; spf=pass (google.com: domain of rwilliamson62@gmail.com designates 2a00:1450:4864:20::136 as permitted sender) smtp.mailfrom=rwilliamson62@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: , > Unfortunately, we don't know when minimal and test model structure concide. Maybe one can expect them never to coincide, by the following loose reasoning: in between the minimal model structure and the test model structure should lie something like an (infinity,1)-model structure, i.e. something like a cubical version (in the chosen flavour) of a quasi-categorical model structure, and one does not of course expect the (infinity,1)-model structure to coincide with the test one. For simplicial sets it is known of course that one has the quasi-categorical model structure strictly lying in between the minimal one and the test one. Best wishes, Richard -- 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.