From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.28.50.68 with SMTP id y65mr2219719wmy.11.1520503869983;
        Thu, 08 Mar 2018 02:11:09 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.1.73 with SMTP id 70ls892952wmb.12.canary-gmail; Thu, 08
 Mar 2018 02:11:08 -0800 (PST)
X-Received: by 10.28.105.80 with SMTP id e77mr2048485wmc.26.1520503868689;
        Thu, 08 Mar 2018 02:11:08 -0800 (PST)
ARC-Seal: i=1; a=rsa-sha256; t=1520503868; cv=none;
        d=google.com; s=arc-20160816;
        b=osJxPzeVXsICQ28glTQjxiopKtvt3gQ7V4kSbVzKVRJPqh1EeJjk3e5/YPT+CxtjNq
         AOMCYKbp3UQIP+jE+bwSopeJQwqcNTQ4zl3zTjk4ZBf8a2uqi6d6ptlA7Fbz2Mkp+mxL
         y+fe4qn09l1q3jnJB6uQO0F0qHh1PuskopPae2RxdgCDp2oi1vdLJXTB/ZFCRiJhma5C
         JCEMbttRq9wSrU1Q9X4hWImRl+B7RkZMlOPhG+5HbSm3agq64bEc8nIdjKQXMi7gEUKK
         DL+x8GwwzeBNE823VCX40xxEopvHF0gDFHxdaEipdNNRJK5+c45pooI5XfoV+Emr6Sl3
         XPbw==
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:arc-authentication-results;
        bh=YvUbr9QYq+9yxXjfNoipOvzFV/X+b29Fsb4xetfmtws=;
        b=GJLORsTI8H3gu7qxemWi6b27lrOuPAZYKSWj02Yys2U5gIOIucKdYqG7O7EFIwCJnC
         uUkppdhFuBqG30lyooaewQRVDVp/LdaCvrWfrABCl6oVELOFjCBu94mfuovy7CPp+ntL
         8mgUsN1v0ZqXeR4BvMQSokzGYb8MKjeJnKZQfXsZu80dRApV8b6AOT/N0U/aH09/bOrV
         iEGxP+kRsQxH6YgFO9TI651cq9xInosX3InBPLIZfdkAJf6Bx+AE9EqVWP423291bZiH
         CR0wE+LBiSd105CZVj29AcQD4M7P+Nt0rAgvjc8yWt9JiuAcDoCDkZbNHYzlzLr2P1PZ
         qYfQ==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx503.hrz.tu-darmstadt.de (mail-relay239.hrz.tu-darmstadt.de. [130.83.156.239])
        by gmr-mx.google.com with ESMTPS id r10si631411wmg.2.2018.03.08.02.11.08
        for <homotopyt...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Thu, 08 Mar 2018 02:11:08 -0800 (PST)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239;
Authentication-Results: gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21])
	by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id w28AAq9A029100;
	Thu, 8 Mar 2018 11:10:53 +0100
	(envelope-from stre...@mathematik.tu-darmstadt.de)
Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209])
	by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id w28AB6RF025067;
	Thu, 8 Mar 2018 11:11:06 +0100
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 7106F1A0A8F; Thu,  8 Mar 2018 11:11:06 +0100 (CET)
Date: Thu, 8 Mar 2018 11:11:06 +0100
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>
Cc: Michael Shulman <shu...@sandiego.edu>,
        "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Categories with 2-families
Message-ID: <20180308101106.GA2197@mathematik.tu-darmstadt.de>
References: <CAOvivQwEH927TWF2OMFpeg9YYSArDDGiQRmtfJGjj0qsJzSQDA@mail.gmail.com>
 <20180307170902.GA5070@mathematik.tu-darmstadt.de>
 <CAAkwb-mqv8AfJJrJNqXw71op7nk0iPDfGvq5qTWUL8fz0LQJqw@mail.gmail.com>
 <20180307203003.GA11083@mathematik.tu-darmstadt.de>
 <CAAkwb-kBBk3=Lzmb-sn47N8mtXZUe6Y=3pQChFcnYXP=d2pdRg@mail.gmail.com>
 <20180307210109.GA12590@mathematik.tu-darmstadt.de>
 <CAAkwb-nuDxBq+Ths0MWRqfraMT4U9fHUk7t4Br1Xt3E+UzP8NQ@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <CAAkwb-nuDxBq+Ths0MWRqfraMT4U9fHUk7t4Br1Xt3E+UzP8NQ@mail.gmail.com>
User-Agent: Mutt/1.5.23 (2014-03-12)
X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2018.3.8.95416
X-PMX-RELAY: outgoing

Dear Peter and Michael,

in full comprehension cats there is no difference between interpreting
in the fibers and interpreting in the base and that's why it doesn't
make a difference. As I said for type theoretic purposes there is not
much use for non-full comprehension cats. But I agree with Peter that
there is no point in considering non-identity morphisms in the fibers
since we interpret in the base anyway. Considering full comprehension
cats leads to unnecessary doubling of information.

Thomas