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-wr1-x43d.google.com (mail-wr1-x43d.google.com [IPv6:2a00:1450:4864:20::43d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8c52daa8 for ; Sat, 16 Feb 2019 12:30:42 +0000 (UTC) Received: by mail-wr1-x43d.google.com with SMTP id o6sf4699782wrm.2 for ; Sat, 16 Feb 2019 04:30:42 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550320242; cv=pass; d=google.com; s=arc-20160816; b=P7Ilcr98wOFzRuoW7a4TorgF3ROywpRfHTjar7KTTWg05Wyf6iYAEimayx5pCfI3Ea s/9f3a7WZ1SjfbIkkBG3HaZmZIsI7uRhEjpLcq/uy9sG8GXqyvzlrBUx9+A/zz5hBIz4 DwsZVcOvg0VHQkLZXifIC1dZHAF0zlOQFRzSp46TFqPcZVuYtUF2yTMjNRC7DnMzQtU8 gBw+AGUC63WG3JRuaL+xwBz78CtPnIG/8zfsv6IbYhZOhz0dPUVfCSbWd65NunDGxFSL dC3CYdC6DCmSWc6AJhMThgtsnFG+YNqPnMhXwhcF9bMb1FeA2eehcz3X0lGxDVTA1Qsc ZRkQ== 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:importance:content-transfer-encoding :mime-version:user-agent:cc:to:from:subject:date:references :in-reply-to:message-id:sender:dkim-signature; bh=I+vq+VATQQIzTj3IGlKYICRi3OX/JCsxKhTCqjHRFyo=; b=yOQqy4Cy0hvQShQCgUraEdbNhRWf4gQnvZLmyrnGhmVngkLNSu0Gn4VR3KgxCoGj92 ALqS6icWCBPVWc+hsvwHAzqcmGfel6HJ4r4Mzrs1yChb0jCO/j0BDtlHzy7laIPv16HQ RSefJhnTt5Yd2qP3qH2h9wlN4zEqFu0r+sYd/NbuOIyXvJ/IkzkktzkFVeGGNbjxYmL3 F2J3eMk/xCNI+eGw47iKofUuuLxvIYpH59ufpaXCTI7uNZ0J6TS08pMkMXWu49sye62n BzZT4+w1SO2aVIheD78dGF6n6DXzDwSE6p6bsuU1CFaQBE175lUZXjZ7cg5/R5FlCUqv R7wg== 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:message-id:in-reply-to:references:date:subject:from:to:cc :user-agent:mime-version:content-transfer-encoding:importance :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=I+vq+VATQQIzTj3IGlKYICRi3OX/JCsxKhTCqjHRFyo=; b=ShVslx4GnK4+fVJb/awuMJt5yUG50Cs+3+GXi3WearvAQ0QbGf/r2oY4jBrkXCTwgx 0AQbsSg+crBK63FF8BboBq8RQGjyMcVmXxuulM3VQdSE9uekYwvOnJW3Y3XkooX5Jj4j iABQEGcuiMXQh/mIOTSxCK2Gm6SM9smgiiskh5leiyefqFTNin/W7Cu2ZrnNBjEHH/GH oNK9QmqEH6rUDCQtmM3ccZdfqaGSKlfseSETRI3uU67Oh7TAvw6QzwjC+PKVLEMV/tvM JM4c9Evbv4+vCpsfRx8oh9NmNO2fIVQ8KElrTrNBglpCU7lXbC2/luF5fJ3rwNV0IUVA WNlw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:message-id:in-reply-to:references:date :subject:from:to:cc:user-agent:mime-version :content-transfer-encoding:importance: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=I+vq+VATQQIzTj3IGlKYICRi3OX/JCsxKhTCqjHRFyo=; b=OhLmE3uRsiZqJ5hdQtphgeJpHuM1oab6GD6PCKjeJTE6PynDZb4w6wRcN4KVrym+mU IyHDIEReVWcusYMfSIUP6Yb+4FmvUZK77XsWl+ikdeSx2Zwua3smpqBzlWMyrRvjU0hr ANHsPecwNo0Wr+ZNJnQ/z/dWkrKovCvvrJnE1VkmVyt1XIpLBn6K2KTgiknG4ej4rlUy w8R+LqtMSg5VDRHN0lXgnCE7IBTpYKMHtITdiH1UEGgYFYGUvaRosChDKG2ilol4iWA5 uUHaroR0mMbktb8sByaHZAU215pg+yVST47fUfyuWZxF1JiB6rtKiET07fUDHyyqFS5Q nrhQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuY0Kg7ijfpa9Jzwb5XADaVrZ5cDegjMx1CmVuxenGHHpgXAO8RG eVzbSa3tkNFzbt7Kc2njQM8= X-Google-Smtp-Source: AHgI3IYdOPb6Agg7z/h7/4M7M4zDcnQjGY1mvqxIebRUmiVUD4sLKev9bNHjTEW4El/S8EF8Yf5WAA== X-Received: by 2002:a05:600c:2157:: with SMTP id v23mr45874wml.2.1550320241831; Sat, 16 Feb 2019 04:30:41 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:3581:: with SMTP id c123ls1118439wma.9.gmail; Sat, 16 Feb 2019 04:30:41 -0800 (PST) X-Received: by 2002:a1c:c3c5:: with SMTP id t188mr876832wmf.15.1550320241383; Sat, 16 Feb 2019 04:30:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550320241; cv=none; d=google.com; s=arc-20160816; b=t12SO1OsOd9puV+vCZE83Zse21GUXcSJ3nLTcXr107PR1GrK68rfq/2Dp94Dhoqbmw rf7Loi9tfr5pxacNd+vo5mSLKUHwAW+6SYRhwg1+SfTrErfBm5IlQdF+604OIjOm6ztQ BL0lY6fWOMbmN7Ug2LbUnKVo2u9XOH6e3oM/NP41zBuMzygfn0sisj8gdFISP+d3zOp0 dIjw3IIa+JNaoqk4EklZYVzTUjuaygwZZg1+zyoEZ7A4GCJQqUKzNxjMjbj89S7KRrYk bbb3srRjEVpQrcwbbmBBVfZdq0rAbiIAlDuklqmXGKPjktk30WfH3y9/fkq+PyVcKfor JJRg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=importance:content-transfer-encoding:mime-version:user-agent:cc:to :from:subject:date:references:in-reply-to:message-id; bh=HNjfrsHmvffactecQu3Hd5SMmK8j8iQkxUmj4sQrhX0=; b=kzP+whL8Iexz3EmBv2fkk5nYBs6e25dj7pLWFcOBb15eCK9H9IEeHOdNcn8uqVfiN4 OoBx+Byspgmm1MOZIK9zYtQ1SYlwiyd9wpLQb7LVAR2XVEVlf+79RAFnOUkdxTGJuqVE Gy+BLCH/8eHiUmfoEIy3BZRtqybq3gqKhKm7vRxY3Kr23IBVcDnWGjfC7+uo6D6AmOID DDq0+B6OqOKYBI3G9PrkNQtYhPSzpTs9/txNlGbYFlSYtBrlXnR/Jr/A0ljdpm4E/qfy bk1G31w2ZZVgKdvafO0Ywk3B2fOZ+eQCFlFCRgoYASRi9QiDUOw82qcD8POtoYf+J1JY e3+A== 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 n4si652874wmh.3.2019.02.16.04.30.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 16 Feb 2019 04:30:41 -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 mailout.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de [IPv6:2001:41b8:83f:1611::150]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mailout.hrz.tu-darmstadt.de", Issuer "TUD CA G01" (verified OK)) by mail-relay231.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 441qGn0k66z43sM; Sat, 16 Feb 2019 13:30:41 +0100 (CET) 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 mailout.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 441qGn0KHBz43WB; Sat, 16 Feb 2019 13:30:41 +0100 (CET) Received: from webmail.mathematik.tu-darmstadt.de (fb04277.mathematik.tu-darmstadt.de [130.83.2.17]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x1GCWTDG014584; Sat, 16 Feb 2019 13:32:29 +0100 Received: from 79.208.250.203 (SquirrelMail authenticated user streicher) by webmail.mathematik.tu-darmstadt.de with HTTP; Sat, 16 Feb 2019 13:30:40 +0100 Message-ID: <4d63c003926b2c19e530c107c5b141cd.squirrel@webmail.mathematik.tu-darmstadt.de> In-Reply-To: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> References: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> Date: Sat, 16 Feb 2019 13:30:40 +0100 Subject: Re: [HoTT] A unifying cartesian cubical type theory From: streicher@mathematik.tu-darmstadt.de To: "Steve Awodey" Cc: "Michael Shulman" , =?iso-8859-1?Q?=22Anders_M=C3=B6rtberg=22?= , "Homotopy Type Theory" User-Agent: SquirrelMail/1.4.21 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Priority: 3 (Normal) Importance: Normal 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 usin= g > 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 =E2=80=94 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. Unfortunately, we don't know when minimal and test model structure concide. Thomas --=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.