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-xb37.google.com (mail-yb1-xb37.google.com [IPv6:2607:f8b0:4864:20::b37]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d4accfab for ; Mon, 18 Feb 2019 20:45:02 +0000 (UTC) Received: by mail-yb1-xb37.google.com with SMTP id m17sf11993829ybk.21 for ; Mon, 18 Feb 2019 12:45:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550522701; cv=pass; d=google.com; s=arc-20160816; b=aHKWEQtt+WcIhPxg6e7BQraxzLCsvfuYijsW+krKWGd4b2NrRODRdl3FRLcSasc02t YsP3KZICdWCQEDGeKGbs3c6vvwHl0IBoXfIheDuzMo54zbFzUWEwy3YoqGz48MFXP9f5 fn2EZYZ2XMwaftiwjgmS64QG0S5tCH/Pe+uqrNfYR7Mb6pd237KZGbs5hvGLCjetkGxj +cyg7QJ3hkXxgTujPf3HkZ1WhV+0cN51DmbsmtJElz9sLory5FD9NPt5jPpdy8q7BIOw EoLO3WB4MvAX+4U4SSojyiEeh9uo8KD9wQNeXkKEB1AVwkztuA16SqzlNhupeCyd1gir 4qeA== 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=P0OuBJoCWCOMt8hTMnBYB33MZqUGClFjKZBjZ6/KHNw=; b=LSCJnEhQiqhZ9pbZfa4ifBC5sFqs8XLFDygbM7OYTHD73eF6w9Ax5D19kC+iNRZwFH 2sFOchIWS8gnazqSOY8q7zBp6A5uB2f12klLICITQdVyU+R9aP0YksJDiJLtJVTqAlbz yUftiv1MjVyAlKiBuSuWdTMpumo16a2FdFLmOE5iT2yp94BQlykChpQiGQxST4ib5vIG T05ESEYoovrDe6JuV6svLzjSGpsnKafjW3qZ36yOA1/Mgkl9YYF/yVyK07M2GlJxoHIW 0/vjAvvSwcdy77gxrDdKpra6wDrQ5qOSJUDwGNxIbjQc0U5ZW79oQOI2/5++NIRrWoPT PNLg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=gYJeUH+f; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c 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=P0OuBJoCWCOMt8hTMnBYB33MZqUGClFjKZBjZ6/KHNw=; b=Lo9M4vuf9uG9kWj0YLbnx0C8UnQv6N0NVfUfv1MLsjvUVuUh2OExEWzdntfVGOA2tt 1ker0sh2mOX+0zYHMN2bxpLhzUxgGTk95DuFFfyCmF0zGFTLJIkx7TESW1cMvXAVuwpI k2uTIfUB3zpD/921ULNyNzsBHcN/RrC0FMs8lMI5UGG6JSE3kI/5YpiOQsABdC6L4xuF IiKLkVMfitV7SGNwVKCZzT4zRUxSp408myoUkCC5qVgl6myhqgLMm6bV/uziJJTWZZOV c8aeEP07IwoTEVXutsLzJJwxpfOvk2x2KC8FOJt+oFEuAMZOKxTz/KsJasfaaMYAgl5j H6pw== 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=P0OuBJoCWCOMt8hTMnBYB33MZqUGClFjKZBjZ6/KHNw=; b=PuDQh7C2wxNIDK9txlh/gQDCIHQXwOMYjOuJ0KnXUOmV5guv8g2Lv25XAt5ZsgkiWU TdYH0NAqpeMPB97O2q/Te63oWcZEAf0dHHrTtuWu3mPcas91vpvvZ1/6dgIfTJIqgT5/ +nN6FIbeI4zvGJ7YLWnGD4UjXag65jv9wvr2QRmt5bVNVYj4KDyJQGadH7c8mQQpNt1L F/+2i4zGjkJiLDjyck1CuXKcASd0uj3KoNhDK/64eqwYSMjJJMOEvRuRjNLrW5M+3TrM I+zMiPeLFf/lya6nCZGaF6B2eKR01DEAnFU34g9gRr+ynaMtlT7KddSu0NIoYEI8pLyk Knqw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZb/n6cXtNXXSLi9sQBXk6sblc/EmhLEcgWDCGu9CXZcGGDnB/d 0ujJDLm/sV3VwRxgF/C3+zY= X-Google-Smtp-Source: AHgI3IZgeGXZRwb5sdakKtAzH5XF6Qor6oE0zuDe+ye9wnCbq5KNZzckGK23etC5Eq5KAHuEtAuE5A== X-Received: by 2002:a81:9984:: with SMTP id q126mr227857ywg.5.1550522701576; Mon, 18 Feb 2019 12:45:01 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:a223:: with SMTP id b32ls4868583ybi.6.gmail; Mon, 18 Feb 2019 12:45:01 -0800 (PST) X-Received: by 2002:a25:fc5:: with SMTP id 188mr11784281ybp.69.1550522701238; Mon, 18 Feb 2019 12:45:01 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550522701; cv=none; d=google.com; s=arc-20160816; b=WxmMbhmwdOzUA19MP4m0G3K82IpqUNecdz3ebrMhc1JsGYuiILc/5G1gs4b0Q4TcaT U7khD8iQRmi0e9uQxz9YROdhAHUAC+chWPrwhaFwgxbS5cfQLM4DTIWfmnI10EaedhEk ZS3PKIShg1Np6bblVRxLb73QlZYiSk9MnHmfznPGAidttqlQ8nCQmFCYTteiQVZdCOs1 0CSQy6KrhndjQ5zPFOv7Wfndvd1BpBXyMWDT+DtQdkkt7BjU/MK83/KzzTKdBNmnAWXs MgKZHX1vDfPEDC5/64ri5SLUMuQd9BhARWPqyTVVAwh22FoYtS/e4v18OVAxW+eH4rig R4AQ== 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=bqQVpKzoU824ypNmTJGHBjqHOGKmdg+yi9/O03FU9hE=; b=G5vY64u7i3QthUmmh43CRGzI52SMDjlAUU68xyzge4VMFFfn5wNE3nYyyphy21zRQ5 5n5OHdddFdl2tz8y4u7ydegZ/MgNoUZvN2qdne5bWZv3n+mfELqOc/do5a5Yx2tq7wFM bZx6krg3HqkXQHvReQNr/RiNNlu3OB7dTsbNbgqlr+7hYSeaqkO6UEhNWU9kjajjbDBL Az+4s4GbCHMnkR3erzCC2XfyrRE5fIuPbPUUcjWWtSXDfTB5tBgrcpw8b61bwfvDr18i Tdbu0x0O18R6r0Y7H7RFD78gvuKwZRByYATC8TDVGF06FZ9aLvZA0l4wASldWbWBrV6C PPGQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=gYJeUH+f; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2c.google.com (mail-yb1-xb2c.google.com. [2607:f8b0:4864:20::b2c]) by gmr-mx.google.com with ESMTPS id h5si550553ybh.4.2019.02.18.12.45.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 12:45:01 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c as permitted sender) client-ip=2607:f8b0:4864:20::b2c; Received: by mail-yb1-xb2c.google.com with SMTP id n84so3407498yba.2 for ; Mon, 18 Feb 2019 12:45:01 -0800 (PST) X-Received: by 2002:a25:2089:: with SMTP id g131mr7716432ybg.356.1550522700675; Mon, 18 Feb 2019 12:45:00 -0800 (PST) Received: from mail-yb1-f170.google.com (mail-yb1-f170.google.com. [209.85.219.170]) by smtp.gmail.com with ESMTPSA id e3sm5770917ywe.33.2019.02.18.12.44.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 12:44:59 -0800 (PST) Received: by mail-yb1-f170.google.com with SMTP id o129so5521128yba.3 for ; Mon, 18 Feb 2019 12:44:59 -0800 (PST) X-Received: by 2002:a25:6949:: with SMTP id e70mr10525069ybc.334.1550522699346; Mon, 18 Feb 2019 12:44:59 -0800 (PST) MIME-Version: 1.0 References: <20190218102542.GC28450@mathematik.tu-darmstadt.de> <20190218203024.GB24000@mathematik.tu-darmstadt.de> In-Reply-To: <20190218203024.GB24000@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Mon, 18 Feb 2019 12:44:46 -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=gYJeUH+f; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2c 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: , 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. On Mon, Feb 18, 2019 at 12:30 PM Thomas Streicher wrote: > > Haven't taken pains to examine Andre's treatise at least for the old > display map categories there was no axiom assuring that for every > object X there there is a chain of display maps from X to 1. > So tribes/display map cats are more general model cats, isn't it? > > As a model of type theory I don't see any need to have infinitary > axioms as are common in model cats. > > 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.