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-pl1-x639.google.com (mail-pl1-x639.google.com [IPv6:2607:f8b0:4864:20::639]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 81eccbaa for ; Mon, 18 Feb 2019 14:33:12 +0000 (UTC) Received: by mail-pl1-x639.google.com with SMTP id w20sf12665306ply.16 for ; Mon, 18 Feb 2019 06:33:12 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550500391; cv=pass; d=google.com; s=arc-20160816; b=P9fYyRoz8sYYImo3eiV+EmzGD0OFBDQ/b/k3BuUSWw3fB5D/S/Ej1krnCNbc8pLqUp URdf32NpGZE2PuPoB895yGAUi2PcWbXA2z0KVpnw1yNwEE/ZlD8jpHufnfGfgy2yN9bg oK+H70pG4Z5XdiQxKkKfA2RgP4YjeFFh/YN/MuMsDJ/5cy2NHsjb7xgArM9s071gnmpo ymkh34CShIWzEdrQjh/yy3RzDJidkiBNJr3Re67DhgwxZv/wbDBBOuDGxteS/CIWcL3u re/PJpJgceYfsow6yiO8oGjgTW4VC05O7DHCVvSu/yNssvLtiyj5UdygIJlHy65LsyoZ uJgw== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=TsG9roBXZQafZhUtF3nXO84SryPsoWT+8l5OVZ/5R3k=; b=ZTq66ncPbooY0wxpU3QDdKIvLXQdp3vxdhuNRDDNf9++Fhrumnjw9jWP17DwlLoNYU j9jc17NHG0QmyZmfDiHei4P94eD/1YIC3ZYzM9IUetoF7MSg7zKdqjAwJo9E3gGQ0MJB c23/eocYwBr5frTnZ/3+kOom1LJX/J4xVExbB/OR4wYKThJV44C7dk5g9WapK/UAMfB/ WEHF3AWEhPG1dWvWdSENkSdTSugBgtG7gcwpW71naNAqr14717v/ssLtJiBKy9pXZCrQ HADGAqU5tZnuUSJ7Lf288WQ+jhzZk8ypxZfKOyfr+9RtL4LAOGsFRNHHbXvlsaXYJbi0 /PXA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ObfWlHWI; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=TsG9roBXZQafZhUtF3nXO84SryPsoWT+8l5OVZ/5R3k=; b=TWHS69U9+9OoDS4w4BuwwBsIF/L4H6thaf2AWA2oca/Ci8J74urZxNrDf1xhzp5a2z LP2G+aZeuE4rUSF59y9L8LBkejA7Duc52aRIzR+EkE2lwCoxSa8YEv+CbiPmJuPtNLGa zg/HoFyawhC58W6HodqpXrEGhUwA7xUcvCRmJbUE/QvrikVWM0bsAdOe3+jLPxy2Vtch 7Cofm60oXF0mTUWmEM0htYWt+UciK0asq0tS7tx9o9oSFwa1DHd+PPmiPy7noVVF8mFM W+iI/3KHdjQmxK88dZkwsWTIf7L8UYRwPQbx9ANqV2jzl9VygC1RSOloMJU6+C43FwQ1 Rb8w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=TsG9roBXZQafZhUtF3nXO84SryPsoWT+8l5OVZ/5R3k=; b=jKcyHFeGAI/yMPHuKaEHLKXGc9Rivpi8WkmdLz3VcZpCDk96W5+XgZQTzJUb4/2pOm N/t4Vb618Fm31yVvCZ08SQllhLiFdxyF5lVcwqfTc3dJgaltqYHp2JtbPM2B7KRLow6C Pp8oPVOeUdkxj6d0ullyz2LYQjkdsPq2xECEjY1Cdi4QQkVidPFai8fkiVw0oag42Typ iW4hyvnIdvhPapczyoUgO6Sq3a4x21TkdG857JuZLJ5fR97R6Wvf71yvwBGSTCk9YXSY 9rmMdQTIOdIxuElV3M1zOBfVQ6Mw1NIQkh4CbqZ/OsK+MP8+cZ2Q+J9t8fgkAIIdaCrb OOJw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubEN8OPpAEy6Q0+Hf6wXgRLKDPvpYL6oy8el1FZyWDV9DEXMnnF 67MSY8S03RjLtCwea5EMsOc= X-Google-Smtp-Source: AHgI3IZIsAO+WP9OIbCv9n5UShXpHgqERyhD0iJbb/YJPz2lMLxWi2qDi5aBqRogeQdmVwLxYGd3yA== X-Received: by 2002:a63:6a88:: with SMTP id f130mr83159pgc.4.1550500391368; Mon, 18 Feb 2019 06:33:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:8a8c:: with SMTP id p12ls7321726plo.4.gmail; Mon, 18 Feb 2019 06:33:11 -0800 (PST) X-Received: by 2002:a17:902:a711:: with SMTP id w17mr90938plq.112.1550500390984; Mon, 18 Feb 2019 06:33:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550500390; cv=none; d=google.com; s=arc-20160816; b=ZAnfeOye/rfI8OVuVomjlQAwV+H60dYwr7ZfhPq9SdRsofcavWR4D9Hg/hM9KBbB23 uCHa5mJOI0xFOJcRGXAo+QZHJWTUDuT/MCrtihIY+BnouX9iocZU9okDhlyvY90dqDmZ Iu64XRvMlPzAQJgzXUQZawxkKyLprWx2XAHPtkfEiPuGH/1QezqajwyA1NIY1rKMW8J6 hVGZ+7yRmtk7OB2Em8k47juTmQeSeq6K8cyrvu32W6InOVGvMH7j8btYe8tbLugo8EhD SXkRPY2BHIfSJNjAjItX+RoOoDG81TrJzQ0hsD6T1fjgcg2qTepkRuoryLuTFxDqKVZO i/9A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=KXQFLidAvGTDJpCUwD7X1U6ZEOSOK7PyRNxiiiF4jCE=; b=A4WaiQYRfOFzs/c5LK9xl+pMPPgmQAAcQFgEbJ5ajphKviy1VuPtmWpKJnCtg35jbx wwCu2YeZCHvHxOz5K2S0ulHDBAGtZudFY8MHU9V+WKcFT8FRtLCro+GYsAPJfd9E84R1 VXnt8W/7H17cIRAW1q8pIG33kJkSLBJtgzYx3X9JXtoIFU0vCAcwdSrYU9z2MPO+QE7y MOREwJnlU3GetrKC3VsDaVcGWEa81wHfrU0wnBwFP1LSnkiKOv6u2jWvWY/9UPEqWbfS m8MBHsb9PSH6oDNNGznVez19GBXJxRNgVQxUhDw+VwKstzcXNKCfeSA6ACYp2Jef5UDh W4SQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ObfWlHWI; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb36.google.com (mail-yb1-xb36.google.com. [2607:f8b0:4864:20::b36]) by gmr-mx.google.com with ESMTPS id 23si615392pgc.4.2019.02.18.06.33.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 06:33:10 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) client-ip=2607:f8b0:4864:20::b36; Received: by mail-yb1-xb36.google.com with SMTP id 18so5204813ybf.8 for ; Mon, 18 Feb 2019 06:33:10 -0800 (PST) X-Received: by 2002:a25:1b07:: with SMTP id b7mr18799029ybb.198.1550500390461; Mon, 18 Feb 2019 06:33:10 -0800 (PST) Received: from mail-yw1-f45.google.com (mail-yw1-f45.google.com. [209.85.161.45]) by smtp.gmail.com with ESMTPSA id p11sm4431804ywm.60.2019.02.18.06.33.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 06:33:09 -0800 (PST) Received: by mail-yw1-f45.google.com with SMTP id k188so6501081ywa.6 for ; Mon, 18 Feb 2019 06:33:09 -0800 (PST) X-Received: by 2002:a0d:c182:: with SMTP id c124mr18854123ywd.190.1550500389421; Mon, 18 Feb 2019 06:33:09 -0800 (PST) MIME-Version: 1.0 References: <20190218102542.GC28450@mathematik.tu-darmstadt.de> In-Reply-To: <20190218102542.GC28450@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Mon, 18 Feb 2019 06:32:57 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] "type-theoretic model structures" To: Thomas Streicher Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ObfWlHWI; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Regarding the first sense, there is an important distinction between the model category on the one hand and the underlying tribe of fibrant objects on the other. In particular, a tribe is defined by *finitary* structure and operations, and can be small (e.g. the syntactic category of type theory is a tribe), whereas a model category is necessarily large, with infinitary colimits and so on. Also, a model category (usually) contains non-fibrant objects, whereas a tribe doesn't. So we do need two different terms. In my paper "Univalence for inverse diagrams and homotopy canonicity" I referred to them as "type-theoretic model categories" and "type-theoretic fibration categories" respectively. Nowadays the momentum seems to be with "tribe" for the latter, which among other advantages is eleven syllables shorter. If we want to maintain some terminological parallelism and avoid confusion with Sattler/Cisinski model structures, we could start referring to the former as "tribal model categories". Note by the way that whatever we call these model categories, there is not (at the moment) really a unique definition of them, but a collection of properties that tend to be added or subtracted as needed (some are listed at https://ncatlab.org/nlab/show/type-theoretic+model+category). On Mon, Feb 18, 2019 at 2:25 AM Thomas Streicher wrote: > > 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. -- 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.