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 2329d950 for ; Mon, 18 Feb 2019 20:30:25 +0000 (UTC) Received: by mail-wr1-x43e.google.com with SMTP id o5sf8071478wrh.7 for ; Mon, 18 Feb 2019 12:30:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550521825; cv=pass; d=google.com; s=arc-20160816; b=eg1neX2bd1+NVu50NFG3C/8ZQl6qtkIKBAmpcFHKjST77L4rB6jMqAt2cIBT6rZwEw ikF1+bWdH+VnXZXgBP+bL3POZBiqP4mdC52xuDawb1AStkH6hEmrEKb77BElUTYPMcIQ EbvAXOfZAsefS+nubrNFa5A6oBJHSf/uxpc6wjZhLV4w48wAb5Qxr3bILjiBhf6BV6Ac e7178Uqjphkm+1FdrFjN6Q5HW7gTdh48AQlT1PPrqNgbGVrjJdSlmyy2cg0XhqOR1p1z WizqXW4g4R8KgXbvcZfxh8W+1E5p3ZTyVa34d/Oo++iq7bez4WI3ZbY3HFkVMuiii+fm WfcA== 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:in-reply-to:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:sender :dkim-signature; bh=zcaBwXvSEzgOY0awQTVtyhW8tLOiD22fbkxbFAI76HQ=; b=aRmqqT2yt/CRWCNWoUJV/rcPXq9wF/c1xoed9bX9vIb7dIYc6MXm8uN3ADEBXGJ3og 30ghNIZow88OtLLEpBHrJBaRXUo+HMK5og3/TlRRgymttwhrJMWRWvnxGGhbIPhQwuqI f3eDFvw8y3r97HkpaQsZNVLOMYrS8jIyLpjg8qLQ9emJnR+Q6VZKw6K7JtzPItt+/npK oJvk37aJq5CZR7Q5azhMFPbuP+SIyoTjwAzkkVP2wYFB/BReO6QNONvk9uq9ShlUg6pr TtOIp80y8pmu37hWTf4zaGh4BQ48TCGQld0Fuz8muxEGoCKNbT2oA32ImLiJOzQksLC4 A/Ww== 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:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=zcaBwXvSEzgOY0awQTVtyhW8tLOiD22fbkxbFAI76HQ=; b=lwCUvWawgIO3UzRQBefCpQqF5H9FeLP267u/HtHHUquCY6TFugJwv8OzFv9e0utZ1g eWVtVLcSt55/WT0S+jmfNzwWviatgMIeMJG/eJizFOMdXVfam1hGqH4Qze18AdNYy94N vL+hDCfX5gf4xh8euAnxjWVG5FUvDpHXfXnRqiB+o+y44cvOi7EKzI54PnJhRsmt3KVH P/o25TdvXqVKg9LC95pk69uoquRf+WGLVGLpdzjixIHuINFE99iH7GBEhlAxtiVLnR3y zaPAeSkCX2LWLbwn0P95aL3n7B8Y2vszbqHIONA4bFG6qWd/khOZO9DvVvSBGApqBfJL 6N6Q== 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:cc:subject:message-id :references:mime-version:content-disposition:in-reply-to: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=zcaBwXvSEzgOY0awQTVtyhW8tLOiD22fbkxbFAI76HQ=; b=uBCymJ0qBfLlgdsjCDTRsN4h274WU3fo7r/XZ3ajHrujE4fr5sLP9+F63RqN7/zsg2 CEpKUNEBxhp8KMCYLERBaYjPlhtm+cz3p3GgGXpakZJvDVVEchMtmdHHYJWftUedCR2P ftehWvkwhGkIJE79ynjLRxz9mo0U9dU6BUoRuBgAE2U+HBohPZOJ6QtsKSl9c/qrFoHB oyx9kLLV6/S7vkpzSNW8lHBwUvXuREvGtnzSqQmmhu84TF33rQ/oOah9Jbwic83IpPZb dCP0gQrZvYPu3ZoIAtSpwgBeFySSuFkHYm7bsoekS2Y1w1cQv0ysXPXr+qfoFJorQQ46 7CgA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAua8ynNqbf8jxtmJtwkaDdA72KqdVfqHNTf3b14IUCo6wUT7LfRA e8Xf/hWey6A7O+1y6NhFMLo= X-Google-Smtp-Source: AHgI3IZNvlBH/VuE+pXOuMjdFXLCDV770gwFTWp0ZL1amC/tyrbyczcVuUEaK3Daed82ur/iHYoyFQ== X-Received: by 2002:a1c:96ce:: with SMTP id y197mr3307wmd.3.1550521825595; Mon, 18 Feb 2019 12:30:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f602:: with SMTP id w2ls65572wmc.3.canary-gmail; Mon, 18 Feb 2019 12:30:25 -0800 (PST) X-Received: by 2002:a7b:c349:: with SMTP id l9mr39508wmj.18.1550521825044; Mon, 18 Feb 2019 12:30:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550521825; cv=none; d=google.com; s=arc-20160816; b=FTmNx0HFtkYs/w8zDsdKe4/WmgGxYoRCbfx1zDBBte38ug1C2OnysBjWmTjjZ6uNF/ 1ILtZtFcsFsOrdxQ5cHOo1d4A9alzYkWBZRADW4b8uhx8RuqHFtkAiWDpqd3kW81s9C9 gmN30ipcMIrq2oZyyQVEGIKYTV/KQT02QKfi+eLm9Ay0JDubv6JQqmk0at6jrz4H/Ott Jo91NJu0E9xHUrYToNuRuUbH+V4G57Gr99SO6fxZlB0bHqSoBcuWne/I1wESBTWs2JS8 KTBCwema9/lcMzXHRKcNO4vc2x2gOUv3oTHV0jtmA4OZR7XMtQb9XcRt+KXX88J2G5z/ PUTg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date; bh=vookFmOx6nUbBb1nqt4IBEmeardSl0SyxkKXGYJ7Thk=; b=SMbfzRnkPRb30dJFXY8u8NJa8Okw+W7Z0JGBmelA7zSk/jx9J22/+a0c5oPiqS75CK E6gLsFHgbU1ZwQT58BL4kjR3LOVXUEfFD46Y0oD+cAPIowlQa58fY8/lmOj+Ki7BRk4H L8VC/LV9sF9Iu7v4/gqXCFC31Cxp7uZO9fn7scS+Vpcb3itIHktRJjX27cSNJSPxxSiG 6gzafDCjbHf58+JUm2WTeMitbriImwRtPu0PHCkfj2ByuaOLsYKESz2fJUT1vxVrMm+N jQVT0opEktx9WdvkQ6V7PnQFCYuE513D7KNemPxKksbJK0aeas2/XVyrH/La+9+zrT93 HUlg== 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 j12si17504wmh.2.2019.02.18.12.30.24 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Feb 2019 12:30:24 -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 443FqN5CQ1z43r5; Mon, 18 Feb 2019 21:30:24 +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 x1IKWGkU030326; Mon, 18 Feb 2019 21:32:16 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 8B94FC5D18; Mon, 18 Feb 2019 21:30:24 +0100 (CET) Date: Mon, 18 Feb 2019 21:30:24 +0100 From: Thomas Streicher To: Michael Shulman Cc: "HomotopyTypeTheory@googlegroups.com" Subject: Re: [HoTT] "type-theoretic model structures" Message-ID: <20190218203024.GB24000@mathematik.tu-darmstadt.de> References: <20190218102542.GC28450@mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: 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: , 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.