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-wm1-x337.google.com (mail-wm1-x337.google.com [IPv6:2a00:1450:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e33004c8 for ; Sun, 17 Feb 2019 09:15:24 +0000 (UTC) Received: by mail-wm1-x337.google.com with SMTP id o5sf3952644wmf.9 for ; Sun, 17 Feb 2019 01:15:24 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550394924; cv=pass; d=google.com; s=arc-20160816; b=D9sxRUThZ40AS/XFfiJjxI3YkJmki8uGLFCNRBB9ByZkF3EnvF3x70tnoOxoY6091T VVL36Igug/Xu7AD42ZsSajgG2SIsCs1uy1k66folhcldCUsr8rYdoHJ+s/8yzMXJcVWE vNPCUaRcOXIcSeBd8MXFz0a4i1eZA+sx7dDYisothwYdgaZqr79+oqgXXQcIW1SP5ayw MzZswWyQ5fcJ4xES9of9qX4yX54iSqpSbfuAodZ2nofIpXiQtjBmM/CsyZihVPv/ZwaL iFCGTrXiHqRmc1HzabR51IGDroanvwKWH55bsf3nAIY2lfehVSlquwW6nBpanBw53YKf t01w== 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; bh=MAESEfdQEd3kA5yU1LZvj3o5UNpzI4LZgYnwmWU9FGk=; b=mvAt4y7fqh+sc9luaZ/DUqXh6e8RrLiLAYbUWJNz9r6LtE5sG7i7mcR7Bso8wZvhwZ Vg65rBQa2+Dyprsw+MeolQeLPWyWEp1VjY03KadUAPTRg8iyWX/tB/cMasTo9o2JI5U8 7T4ttHdRx2TER8W4asRTIMSFp8vudrjRPO1RVA3OwgRKtZn4HeQslC0/rC2Q2R+F9Y8A 4UfbexUI4u7dJX6grllpupXzTaDUs+Qv/RR2dA0znQiK1ktwUKQV2cB3erWETvO+gZnZ zF1UYlq3kEog0tFUzdXQuEoAXdjLwsPQDNd2bCPjhA+WAW0KlhxCvuLf0nLdWVmPSmP3 kErw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de 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=MAESEfdQEd3kA5yU1LZvj3o5UNpzI4LZgYnwmWU9FGk=; b=C1LeI90kHIffS0rhoAQ2J5kagZKrEZQIB1tv9HTLsJMR6KHcD+qybAi7qqoVGV7YDX 2scvta0QewndurgV05Yd06Up/bwQR3B6TWZS6+glQnhQinuSjQM1F2ggV1S+iOn0lqSF VaalgWZTMysvfw2DosiQpya6Vyws5bPtT1yq7COlU/1xn/1Qy3Rt3+fym4mccQf+7G8L 5mE51WQFd1TU8Z5JmFjTbhFpM0vRwetFWnEzXiew/Sw4nVk+UYE6Ph2rBOY5OR/u+0aO xVzfloTmfbZFesdJSjIJwZ1yH+fnTDRSwwwWRcH7OCBXDvtnnvHtZ1NGaxVfIoHBKwww 9b2g== 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=MAESEfdQEd3kA5yU1LZvj3o5UNpzI4LZgYnwmWU9FGk=; b=cf/m+RMWIDCX5YuKfv/sLVek3JVboBon/8/CMDg75WRvThHb5blvDwHpB39LuXWC8Q 1XCEDs6I5vHFmjhWqawl/d2bY72hoCgP4Nfk59/ncJ15D9xq4Ys7jjVdXRuej0Gm9aIW oT7iwSpBOIFAfwvGqS5MtoMt2dkDYwBkDV92w6MajeojqYRzdMWsGHLkB8ODjDIqog98 XIrCgN7HqIYFNvrFpzZqdQnqY/HREnQ2OX66zvqvL641XRDrQLH3OAKta1IBbzzOosI0 +PDG+8kdfa+yI0+DovFVnKnrznt2UbFU03DdeBRA36SweCbeLOTuvfCK3P1C9anc+NmK 3Z+w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubGO1jMau85wfaI9nfqX52B+DqqfSsZ5kVJyXePC3+NI/VVYnXi oPorAjOu/H56RsAv1oo8hso= X-Google-Smtp-Source: AHgI3IYcT3JAR1gQP6z/brhpaTEyk7IL+pRBp2KDBk0Qc/P5T3VkpLagiHF8CarELDdplZEqufWo3A== X-Received: by 2002:a1c:5f45:: with SMTP id t66mr115246wmb.0.1550394923905; Sun, 17 Feb 2019 01:15:23 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:3d6:: with SMTP id 205ls553798wmd.1.gmail; Sun, 17 Feb 2019 01:15:23 -0800 (PST) X-Received: by 2002:a1c:7910:: with SMTP id l16mr601710wme.8.1550394923481; Sun, 17 Feb 2019 01:15:23 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550394923; cv=none; d=google.com; s=arc-20160816; b=Me05GlKt81C4LDE44KpV52T3bGrKAv6efOpGTdkjUOC19KGn2yYhUu9mb2ydZr3N/b aFYltvI8dSLqpkMBX9QHhkYdQqhN7mUEjrXHljfqsglvJLFTF/nAEdldn6wfmFzaT+7m UUgYACELCYPS25gwRSeS8l/aJxM7+Uviia8lbbO/rE5eAgICp508hoDbUWt+YE1JyCX6 3gr1ec1vaKNq9MQKiBS0TtEXNIh54jN2wCBwfFZUqK5lwlNn1kXVUYt2tH8Zi8zK2fYQ QRz5DAvXa+mP/TUppDCdedwYcwu5QQfjVxoPH4Kj/qecuTNqJaHH/nNXHp4My0FMH3S5 SkrA== 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; bh=1q+MhbVggAICAudahhW+KkNnCxSvES0RS1rK+FsDYWU=; b=VRUIT6VtIkM2HZZfPGfTSqi7/vw2JthQcqsEHxM5xTvBcDtvsn9L4cMQAiBrx03UUs 8q6GI/f5x7Slsha6LYQKqNLcOW30WKttarmkYtS9kARMHlhTefg/6ZiXOGbaD5tjSVFf YDco52DeWDyIQEzaoieh2GDQgHf7sDLHmlFMCzqDc1jjRkqwbPucwdDxoGCsg3xli195 S1HDjM401tcnLXjQRqvVD49L1j533hQbtmmLSWY//y7PSzvLGK08Tt5ZoKTFeQrbS2yt abWGrcUeLoHkG3MhFbYBJduUfQzHmqhbMf4lTaMXE9QPPwbOL7C93yYxzkG1no/0J7+s ctfQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from mail-relay231.hrz.tu-darmstadt.de (mail-relay231.hrz.tu-darmstadt.de. [130.83.156.231]) by gmr-mx.google.com with ESMTPS id j12si595119wmh.2.2019.02.17.01.15.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 01:15:23 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) client-ip=130.83.156.231; Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mail-relay231.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 442Ltz1Sq9z43ps; Sun, 17 Feb 2019 10:15:23 +0100 (CET) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x1H9HDWw022675; Sun, 17 Feb 2019 10:17:13 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id E6479C5D3E; Sun, 17 Feb 2019 10:15:22 +0100 (CET) Date: Sun, 17 Feb 2019 10:15:22 +0100 From: Thomas Streicher To: Richard Williamson Cc: Steve Awodey , Michael Shulman , =?iso-8859-1?B?IkFuZGVycyBNw7ZydGJlcmci?= , Homotopy Type Theory Subject: Re: [HoTT] A unifying cartesian cubical type theory Message-ID: <20190217091522.GA3415@mathematik.tu-darmstadt.de> References: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> <4d63c003926b2c19e530c107c5b141cd.squirrel@webmail.mathematik.tu-darmstadt.de> <20190216215813.GA1514@richard.richard> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: <20190216215813.GA1514@richard.richard> User-Agent: Mutt/1.5.23 (2014-03-12) X-Original-Sender: streicher@mathematik.tu-darmstadt.de X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de 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: , > 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. but in simplicial sets the minimal and the test model structure do coincide (since filling open boxes is tantamount to filling horns as shown at the beginning of Goerss and Jardine) Thomas -- 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.