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-x43e.google.com (mail-wr1-x43e.google.com [IPv6:2a00:1450:4864:20::43e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8a642422 for ; Mon, 18 Feb 2019 10:25:44 +0000 (UTC) Received: by mail-wr1-x43e.google.com with SMTP id f4sf7648077wrg.9 for ; Mon, 18 Feb 2019 02:25:44 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550485543; cv=pass; d=google.com; s=arc-20160816; b=NnlzblwHmJCMbz9b/+tI7a4esn785Yfwwk0IfrsnOMI9JpYvvin+GkoiVz6yPjvl/P opTl7HSH79zyr9OhP0qnTKmfzG9WFNSeFNuyuQs/S6USSy1BTObPbkGY6W3ZAanLLGqs 4xKxh5nvGs1N8B9Tuv836B2MYA9AKap4MG1HaFIs+kdoIUbG4UoVVvdBGBO+8FEizpnE hc4zbITBWBAa9iQRiRJre9mpwieXWQsNmgV6mNotv+WIB4NcFMx5VYML+0Re+y384I2j a4X2rC+AufHBDVwqlKSJXzCRDh8MDDSSH9aMbJ14t6YzPIZJV9jTP9RtM4v7XbUtYFm9 C+Gw== 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:content-disposition:mime-version :message-id:subject:to:from:date:sender:dkim-signature; bh=ujJHB+R3tl3hEO8m6WDMVqyqS/rNLN66Y4FdD9GbVNA=; b=n8jVVUkGXNDLg+xRkkcEc3Ber4W4wiiqNAcrM/GlHy683Uvz/qUM9VBjHeShOc0nsu NxWZR14R6Ms7gZsvcIviT/JxHE10FyNIOnWk0l7Dii9o5zPShc2B1Y7nUQJp6VvhdwgQ OpjWCx9vG1ZXVUco6HRDfW4XENbF7qDLBVgG/LGoLjKbgtlm22HZEqRquFQi4cdi5DJQ +hnw4+ijEm2vp2CgxFs0hZ2r+tcMWeQYaUOkh5S68aB8ErC1tDn/vc+NtMM1+MIcrXvK hBFNOifnwSZ/eHvSh+VXiD9c7wg3ugutLh42AGSDSn0gEMmrEqlXZjL+f2t5R8A70VN/ syww== 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:subject:message-id:mime-version :content-disposition:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=ujJHB+R3tl3hEO8m6WDMVqyqS/rNLN66Y4FdD9GbVNA=; b=eC2Pl7lgWLCUSZt8qC8m9azafIZJZ2gWiBD84yyJbW3AR9LnRHOYa9whhyUUtVaQuP +sBpSyFnqNW9CJM76N3gcVChweiO9nBpTmb3oH66EoyGkdg8Sk1dZaOy9P0hdREHR4Tl yG3wXK4ngGW7jN6ILurrUsn2GzWD2MpToqxa8FWlNl9Wca4LLcysEUhTy7wJY5mHaV0a uaNfUmJy/d5kObfZVkPPefYg817WoDNMBsuTL4UwAdHt31ThGGPbJvq+DNYXV6bQnvrJ /V1nfXuQZw0HuezdTyF3ehIK65x1Ewp+RCsrsT4TmcL06hOdq513xuptZtZmmotOtj4k XsaQ== 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:subject:message-id :mime-version:content-disposition: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=ujJHB+R3tl3hEO8m6WDMVqyqS/rNLN66Y4FdD9GbVNA=; b=FSxFbtUo4EbxHUPTFwxcoyI/bzL9/VCLf6ij154tz3jhkM9DgvJKNm5s6X5eo209aP O0bJ9r72EVlfuce9CTHCU5TXRHxghaBmQbVBUDU9An+vzz/j36De6ZT7AuVJsPH08iyL jcuyZlNheR2twvSNr3cyvH35+epIKn2c+UMMZiqrzTVATmxumHZvgg4FQeF7XkiNbBfv I7oQ+gA0ZZvIFax5c7ftd+2I5BZxGQFo9yr6Uf137TF4qBgP8xDXIelbuZNRGLuIVejH qXnR4dm4D8UjvZII28rmlJc0mleKZYN4lj0XlhXiAGvc5bQQ3ePkJQlz75ZEZ2Y8Ur4J tCMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuY0KgliLyEg7Awe+scnlO2ZUG1NDJrJOKVGyb7B/dZJ8zw8Gsu/ FjwL7jrNREgOdBdrt87d4QY= X-Google-Smtp-Source: AHgI3IZ8u6jM7x5k8QX9XQdUotigDwG96IDT2E900NPF9AHVweLcwFY+wMCtLR9cw+7kN4z0lC2W3g== X-Received: by 2002:a1c:9652:: with SMTP id y79mr147876wmd.3.1550485543578; Mon, 18 Feb 2019 02:25:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:3581:: with SMTP id c123ls1667011wma.9.gmail; Mon, 18 Feb 2019 02:25:43 -0800 (PST) X-Received: by 2002:a1c:a741:: with SMTP id q62mr304689wme.7.1550485543140; Mon, 18 Feb 2019 02:25:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550485543; cv=none; d=google.com; s=arc-20160816; b=CAgZxaOw8ZWLZ7o2BfqU6cQcHbZgrj65K1QZ2nCpqkkVKO81PpDiRKMgEY88MOUq7L BefA8FayO2icNg0RwCILWosrQnRHjSYyMumqq5ftX0hLd7b891J3BnPTjkUNOvPyQMFR LtX/ST6hOHpYSkdZHQ6hRwPuYCoS0+3GlxQ5m2pggEZCpX1uyk+W7ybj8PomcVnrknpF RW966w/JJQNF6zMCNGJrH07Ge5LKVgJg3tsA9Ul+HYbBwZQypY98090ViY310/3Znbe1 NHjYy3RdHzY5V+CM1ZhTHQC1JUoRZNwx1bY/Nl+ySl/06ta3h0vXKPRfqIXbq9rJ1+ek AwIg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:content-disposition:mime-version:message-id:subject:to :from:date; bh=K28MK9rCBE6V4Pwrx4/81EHPGzUzK7ygL7c5j37H94Q=; b=adtwXk2Zqwtk28EOzxhl3dYJjj7Ytje5eP6ccdcIslBj2XfH8ypfgcocs+dpjKCiy8 4vvKESY8nwVVajn9Az7QCCT3G8RqFRWRXDzjApTwpHtQqMO6pfejLu+k1Yj5jsBxRfFR /mCKuzcd4LRmpiNCX2LSdF/yeFJkP3wMUpkwl+NDoJJnPwYQFjEQQLFxfqzCY9lmvWZy 9aWrO/doFnXsdewQ6wpgHDDmiCWaY8U4g3DGZSgt/cPhZljODg+bDLQNf5ihUvmVcqDc 6hRnBzkTkFvuxp4VdH1vgIzVyLlFBgPe99YgE3UrA1qRLnJgHCr8rdfDjiTZ9r4BvuvD WCWg== 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 s124si435470wmf.0.2019.02.18.02.25.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 02:25:43 -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 4430Pf5sRlz4499 for ; Mon, 18 Feb 2019 11:25:42 +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 x1IARXDp012934 for ; Mon, 18 Feb 2019 11:27:34 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 8D499C5D18; Mon, 18 Feb 2019 11:25:42 +0100 (CET) Date: Mon, 18 Feb 2019 11:25:42 +0100 From: Thomas Streicher To: homotopytypetheory@googlegroups.com Subject: [HoTT] "type-theoretic model structures" Message-ID: <20190218102542.GC28450@mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline 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 was a bit imprecise in my mail about "type-theoretic model structures". I think there are (at least) 2 different uses of the word. The first is as certain model structures whose fibrations give rise to a model of type theory. In the old days these were called "categories with display maps" which have got rebaptized by Joyal as "tribes" which is a nice name since it's about families which interact in a certain way. Another use seems to be for particular model structures on categories (of presheaves) whose fibrations provide a model of type theory. Sometimes, e.g. for simplicial and cubical sets these are minimal Cisinski model structures where "minimal" means "fewest anodyne cofibrations", typically generated by open box inclusions. But not every (minimal) Cisinski model structure provides a model of type theory and, thus, it is not at all a good idea to call them "type-theoretic model structues". 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.