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-lf1-x13c.google.com (mail-lf1-x13c.google.com [IPv6:2a00:1450:4864:20::13c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id be07a2f1 for ; Sat, 16 Feb 2019 19:51:38 +0000 (UTC) Received: by mail-lf1-x13c.google.com with SMTP id z8sf46612lff.21 for ; Sat, 16 Feb 2019 11:51:38 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550346698; cv=pass; d=google.com; s=arc-20160816; b=bUoG/JPhrbAlPodaSTE3xsqZchYWmCWS9CvrHA3VEeeTSZWsL8oae85vJg1P2C9c/7 BXsX3mHzZPgoDa7lspSmbjWhvk8PnYQ1PhGWsswl5trxdiHtlIMndJUaiHaH0Pr+5gg3 2XqG9fcb9rJtXF40xvfNgHqmmU5YVqc089doVy1o5hpcTtQm6ItqRzvGMVVtcxY4pPwI lOG4rcCj8zgqNNB/i6DG6ttZ8sKMLMRTp/i3jpcFgIHH+KJfwxrzJRDl3YV8jGWd1eM3 xEB+B6lGEn2UxWOFBfeb5yrtnUgj4raPiPhVNsuEqCkhP/PyYs+HivwL74/Z/djvssyN 4f5g== 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=xve0Nd7SsVg/0F9DUq1ieizq2/cubBRHbtuiOHr+W4U=; b=GDf6LMN+FjGaOY1UYgtUg8pgOBPaECh9S7ldeYhju6gBYechlqrcsaer1loJwTTkJG FlkjQFtKjWvA7pQ7JuVHdVgvf/8rpn+m+zM1xjXWnLzJAaHekNepc4qiD+n2uaXlIi41 gc7jMz1yL+CiBJ58rgKvCiIK7xJQTf7trGw/a/GLE2gOfu3BjkoBYh0ydFkBtQp3jBMB cCjxjdV+UOd1pK6xKTJdxN59VQ5QcxI4NB1EcT8WpOqUwDulPEWs8aeHAGHQG/FnBaUa 5FNhV4oiJyHVV3Ln6AW+q5HHxqWyu2UTPAYa062Q2/8O1CwLboFX9RAuj+eBmlaTvCmi /JHA== 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=xve0Nd7SsVg/0F9DUq1ieizq2/cubBRHbtuiOHr+W4U=; b=QCJIWYLnGIaUiSPmW8BKLPzZTYgwmiZb/PHDoU9729/dUw08IRoxl/wBNE//Es6nbd zT5TNI/1Y9/Zd3UACK8/oyF6n1eLYQ9FWvZak0dPwbt8h4YVOZ7jh9CfUDLyQyMHBNjo 0wqDXeFKHFJdUM9lkQJz01rxACIpNrs2q7h2i4XfjILNHHVJtwu1Te3K2MnwVSGkN0yd 2HqCZvEwH6vtkaawm790epJYlVKuhbqsaXAwkiPNT3JvRm3lW7bGkPhwXUP2EgzC2F/p dYH7+dtLLxwizkyMVYnifKdhMsKqkEF4bjocitumIBoQ+0jXm5Xus7cK65a3ZF93P2H1 rjgw== 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=xve0Nd7SsVg/0F9DUq1ieizq2/cubBRHbtuiOHr+W4U=; b=fWD8uYYdhQI0XsZ5MWHm9dKzqrVNmuRdStiYuzaPSlo8ledSeUAxK956zIUbsoLiDb AecR0qmA2oG2dIJIHwPKMHL2DzDpBURPKshYYEAC5rRU+XOvX4D8mm7AF/wo4cm41gNA A/Rxp/js9Q3pGAzHYCCN0CVMNNeIP4N1eziIuYaEtvh/dtLaoC3p83aKrhBya8Yq2k7b PRBH+FTQlJTmfWwhd5N2HVtIQkSwH05aEZImMeu1JVDJ6BpdiiE0lENqj+pPzQSZeIwO B1Gv0NAJ1e6XhflgXFENfNPk+2JlQNGdfp6R1rByXDwKaXL/m7LTMu1BuGlau2muXCY0 5V1g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYFoWh1M1rOLk96FU7sBNT8huPqJm7vYYU9EwEIY1RCq/iVyUAA xQms6mG0/e03whwMFwFxH24= X-Google-Smtp-Source: AHgI3IY3mosB9RNsqoQir5KmbSaGJ0s+hzsIpwcXa81rcusAupBviyLfPjOSaJSIDoR7URPInJtpWw== X-Received: by 2002:a19:6552:: with SMTP id c18mr66706lfj.0.1550346697927; Sat, 16 Feb 2019 11:51:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:3e16:: with SMTP id l22ls474165lja.2.gmail; Sat, 16 Feb 2019 11:51:37 -0800 (PST) X-Received: by 2002:a2e:2c1a:: with SMTP id s26mr962649ljs.12.1550346697333; Sat, 16 Feb 2019 11:51:37 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550346697; cv=none; d=google.com; s=arc-20160816; b=xgB9m3kta/5J7EcXI5UC76ySAZyfZngTAgAze00yI1aKYhJw6aZjjZyDEmGDP1MjNd 4m5HTJQYalyUr49AYQlQIuUoLtVG57YNxnOGT1zxDxiX4oc50VdDpT/9FVPvBIfGnUdX LwbJt6PDQBcDK6hwRBlKMi7e4TpMOfIYvyPskV56yqTDOYYT41W0oIegzTgs+Hzp7hVC fZMNU//U6tSpyqATn4nqBcwsNqFJjlrrhx9CQp0EP5xZohmdJ/ueB3rO83SvDyUXUnib 7lOb9joW78cUKBqiEOBZ9KzccZzW15VDPHAypWMJl7VURcvZ4WUVrEFnsyPoFm0Eqt3l gviw== 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=hrrM4f91xxQzDFKCVaUBWg+OkvWT+Ocpy6YEZm48qBk=; b=G5bMXadcQkjGHzIp7aDb2upr/jfRTqd6GFAeFRTjLm9SuvRwwBfPOEGBW3L1f8lx0D YEpLpp+sGCAvPL6c0GHf0iqPiBGl7Li3LPGQKtMY4OkZHp2domOg+GSegA59SNtt1mZl oetIuDLHIl6LwFl9QAqzHTPO3bbQhWh6fqLtLrQuEs5gIDaqEbXLMKlKvZe0++yw0DjX xQ2lSGGJnEUR79TCpo8gLz2wdqn0ZS1h2Ysqr6nrBQQXZq93BJnuS3/tMs5SqxiSvcwS VslhqW6OgR1Q+QnvojXcZ7VdPeWq1jw4dzp7741ueSarVhaQfomoKO6ZdeL1dolgO1Jb PPkA== 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 t16-v6si219375ljc.1.2019.02.16.11.51.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 16 Feb 2019 11:51:37 -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 44213X4Qyhz43pn; Sat, 16 Feb 2019 20:51:36 +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 x1GJrP5m018108; Sat, 16 Feb 2019 20:53:25 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 4F849C5D3E; Sat, 16 Feb 2019 20:51:36 +0100 (CET) Date: Sat, 16 Feb 2019 20:51:36 +0100 From: Thomas Streicher To: Steve Awodey Cc: Michael Shulman , =?iso-8859-1?B?IkFuZGVycyBNw7ZydGJlcmci?= , Homotopy Type Theory Subject: Re: [HoTT] A unifying cartesian cubical type theory Message-ID: <20190216195136.GA11255@mathematik.tu-darmstadt.de> 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.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: , > > I think the idea is that the model structure is constructed / proved using > > ideas from type theory (like univalence), rather than that it is a model > > of type theory. But I agree that the terminology is confusing. > > The methodology is, I think, due to Christian Sattler ??? so maybe Sattler > > model structure is more appropriate? > > 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. 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. 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. > Unfortunately, we don't know when minimal and test model structure concide. 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.