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-yb1-xb39.google.com (mail-yb1-xb39.google.com [IPv6:2607:f8b0:4864:20::b39]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 73e1bd5f for ; Mon, 18 Feb 2019 21:07:35 +0000 (UTC) Received: by mail-yb1-xb39.google.com with SMTP id j4sf12117017ybp.3 for ; Mon, 18 Feb 2019 13:07:35 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550524054; cv=pass; d=google.com; s=arc-20160816; b=Nq/Qy/yBu2NjlWUELLpftkJKh8JQLIQGzRkETJSX0cNzCR9XnXewz65P410LD3r8qs bNIeZWCYjF2fajnZbIQYyWY9x+H9VKVPDKw/jUccx1GG/KXvoohxFDLnw6OQQGLL9KIn miosz0J6fUGSvyIX7+hV8M1VY+7eQr5mV4H9wfO4hziNhsXVxgOpqueByGqrbU8hn5RF KHdlqg3wxBYLohxZFC1wj/dOTAs2PyMy1keGpgMDM5EjKH1k/5z00Z/CNi64VbrtY63D xv0k6KIV6mPEdZ33DTqI+mTmfvth3/LylXkWEyzEboS6AV8Vw6/HfEkCP6YGWmcNJwuB nTtQ== 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=yor3CZX98cyWmx0S1D1F049Ge/N/AVs8+a00w6p06YM=; b=KjHf05TFVPFV4ScCXmv3tAM5lUyDFMznYfWoP0LrgyFUHROyaqtuVdhBn+ObPg0Vr/ OqweNDP4SqTUui6TagRb+89AlblH7Wz+G9LvIfiMxcWqg40bqa5/153D0TKEeN2qRmql v2lHSp/W++s67EZGogJslNnYtvulhcmy1ClFfOufDkNrMWphGqfz05hYfZguxPIxv+8N epYIYmlcWXom5X3Da72Q2WddtIg99Cu4DLR2N09gbzYoex45vARkHXwQy5tnSkUFGZ0C p++ddVBJYJFAtJsDzW3ovj9D104Wd6atAxZXBmeGPCTX4xvQ90n4Qhum7YVNngSleClr +fqg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=x2EWAdI5; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 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=yor3CZX98cyWmx0S1D1F049Ge/N/AVs8+a00w6p06YM=; b=r1iANYNeM3z4BGsfMjw1BKzTiHEW5fnsLE7ew6j9SYd8AUSlDNDu8qRkwmUITk2tgL qrm5XLqfDuwoFXbw5zjPxhoSfABmyPK1duy6y8ivL8yvwiC1XAiGsQUH2FlzGvMG9pSi wB+ohGVuHoRzonqoGSPt0D8wx/sxf1S98X+SjitEBb7sy8ZlU7HhyAHTrQKwa9/6Iz+r s9SsNx1lhhbr3+6uMa/0q38iHd2JdqL7gRUBrzHsq6jqEC5R2EQOQLj/qyxD/aEW6Jgu 79XVe9hvI87GKIqkx9EWfUY++jt7L7UszIvL24CRhQZ5ATEHAZ5rfScw9EnqUjpB45Pq 72ug== 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=yor3CZX98cyWmx0S1D1F049Ge/N/AVs8+a00w6p06YM=; b=IO/7l4lynKS8ZkRwVjm5wRHCFU4MAEnBsVUR1g4TsYhS/WZ1xaaAOGPBC4QVsuXTEn NI3Q0kh75jGFYpWPcTi6Rd+wk3mzKhSjAxj3EHTPHk7Omi5Ot/zy/wqB0W0wIpeLLuJt rbC4J1KSvLw7EbxTP7l/Ur/ArwqaR8iQnDXyk4ptUfv+zLaJtNSFJRl2/699OiioYYq9 +MxOIV6/OovpGewE2e5FB1bVM6TpJ82jNbLb6K7c3jOLei/e0fLWvfCPji5BQeVioXPN dDNjABuGGrybnzyyQrAfYwwNzHezxp0iLjhUIreDgERZqBPammtHpevYN/xSkkRvSadu lWuw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYLanlmY9LvPPhXYOoMniRBnI92rdEshIXuriOu6QWTDGLF6/nI MEY8YNjg6uOryGoancRqNek= X-Google-Smtp-Source: AHgI3IYhtSrgvIgsx9CkYHAlZAmv6Cd1OgnpnSIyhXnEkaHHZobliniMHlGXICP5aMGu+40+/xkI5Q== X-Received: by 2002:a81:6d8b:: with SMTP id i133mr230799ywc.1.1550524054588; Mon, 18 Feb 2019 13:07:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:9109:: with SMTP id i9ls5481923ywg.6.gmail; Mon, 18 Feb 2019 13:07:34 -0800 (PST) X-Received: by 2002:a81:9ac5:: with SMTP id r188mr12488424ywg.3.1550524054147; Mon, 18 Feb 2019 13:07:34 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550524054; cv=none; d=google.com; s=arc-20160816; b=Sebw8ebqNfNIaQFTozrnhKya8oiO2OomLRUjGWktUHloq/d6U5IJW30KyQTk2rUgbo +wrtfVVREmAqhPm2TJwMx5QrMxTEj3XRUoW5qAcdcPCU22aTSQ4OUvwR2HIqk2+0Z0p+ LPSRmwNzJcUgDNyaDwyEKBGHNMS+ojGSX0YmlVuwhwVUXMTIgrBqL/kzEJBGgHhQCw/a l5KswgdnJp+uRDimQVyfLreFa6GnabDtr7T3z5CZWRnLBT8hi3m67vLjCGZJSOaXXH7Y smh0+f3bevVPfSYUyuDx8RJ+QBgiPp0c7vKDvf5A3mGQPrpQ0irx+Y9U1G2HumIxQOmm q/Cg== 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=bG+Y+4naAuEomfoARFW0CFUUbOzzWovNbA26c1WQk/s=; b=cCJWTY1HiZS2XGwipD7RLLDTE4skUpm2na85+3ynWmIZ3mZB/TDDZ7aVjfJoUIe47H gBDMURgtXOW+PLbMARI1eYtlkcxigqQvHNgeWTkS5K0KNPDKN1SuQurqFyvqbqlxXnz0 SRYwzc4V8+jEuiHJ34PgL4NM3u+4tUbZIZFMvoGdq71pQuOc43uBoNVDF7GfwqsNNA9X RtY0+sIJyS/9ih1tAkTT0fzowp033kpxDUv5tO+PiJpajghW6L1cwrZZah7l+K84aTIK +F5P8XbnVS27gabIvEK3RowFa3TVW+rK7zPqMMRG/qWRK7W/c/8PO5NEtW3a9ESG4RDq Ccsg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=x2EWAdI5; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb30.google.com (mail-yb1-xb30.google.com. [2607:f8b0:4864:20::b30]) by gmr-mx.google.com with ESMTPS id c6si879118ybo.0.2019.02.18.13.07.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 13:07:34 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) client-ip=2607:f8b0:4864:20::b30; Received: by mail-yb1-xb30.google.com with SMTP id 2so7294455ybw.4 for ; Mon, 18 Feb 2019 13:07:34 -0800 (PST) X-Received: by 2002:a25:cb11:: with SMTP id b17mr9646528ybg.92.1550524053663; Mon, 18 Feb 2019 13:07:33 -0800 (PST) Received: from mail-yb1-f180.google.com (mail-yb1-f180.google.com. [209.85.219.180]) by smtp.gmail.com with ESMTPSA id a72sm6347808ywh.42.2019.02.18.13.07.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 13:07:32 -0800 (PST) Received: by mail-yb1-f180.google.com with SMTP id n84so3430936yba.2 for ; Mon, 18 Feb 2019 13:07:32 -0800 (PST) X-Received: by 2002:a25:d4d:: with SMTP id 74mr20985802ybn.357.1550524052643; Mon, 18 Feb 2019 13:07:32 -0800 (PST) MIME-Version: 1.0 References: <20190218102542.GC28450@mathematik.tu-darmstadt.de> <20190218203024.GB24000@mathematik.tu-darmstadt.de> <20190218205750.GE24000@mathematik.tu-darmstadt.de> In-Reply-To: <20190218205750.GE24000@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Mon, 18 Feb 2019 13:07:19 -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=x2EWAdI5; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 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: , Identity types do not by themselves require all objects to be fibrant. Sorry, my parenthetical was intended to mention *another* way in which tribes are more specific than display map categories, since you seemed to be conflating the two. I think a clan is just a display map category in which all objects are fibrant. A tribe adds to this a weak factorization system suitable for modeling identity types. On Mon, Feb 18, 2019 at 12:57 PM Thomas Streicher wrote: > > I don't see why identity types require every object to be fibrant. > But Andr'e has this requirement also for clans which really are > display map cats with a few more additional requirements. > > Thomas > > > Every object in a tribe is fibrant. (A tribe is not just a display > > map category; it also has the categorical structure corresponding to > > identity types.) For purposes of modeling type theory, the > > non-fibrant objects are of course irrelevant, since every concrete > > context does have a chain of display maps to 1. And yes, of course, > > one doesn't need infinitary structure to model type theory; as I said, > > that's one of the differences between a tribe and a type-theoretic > > model category, that the latter has infinitary structure but the > > former doesn't. > > -- > 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.