From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.0.87 with SMTP id 84mr1982636wma.31.1520456473711; Wed, 07 Mar 2018 13:01:13 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.157.140 with SMTP id p12ls796173wre.2.gmail; Wed, 07 Mar 2018 13:01:12 -0800 (PST) X-Received: by 10.223.139.198 with SMTP id w6mr2150640wra.27.1520456472115; Wed, 07 Mar 2018 13:01:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520456472; cv=none; d=google.com; s=arc-20160816; b=jRyJ/4uQxDXbP8uNQBTt2VIQAeV7SOiU24MEvScwVM4gqWjlVMMRPFuCWvWXMyIapb 1XBJZ+6Z150gtJ69dhLDvsl9+12oZi2xgMrTK5k3uReA/KbVldXEPevckZ/m+tU2/33m 7tAZUaX7rbdiI+8cDzaN4oExSFbevsSo1KobBIs9QU47VpfaVHfiZENWC/ZxAaUiTuat 9KGz1xHqJu3jZ9r0N9UYYfbB0cn3+dod8uCkgI5wql7wRf3+3+PX30tKCIeRbTH8Vk1H By33ybIGmbJd7UrMGmVa2Wmht/Llyt6/7LpphK27CEscy+/UEhBln/ul2dMdc/jZPtdR fxEw== 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=+Jr8YDkigLMyzcJFww41d82ZOZvQsh/5sN/QBC3LkwI=; b=Os3lteTEVJhR0yNGlg9jhOh9ps5gstFaoqDaAoIQlCqqdT+2a0MvQn7T8pea1KJFXe J0j0u2Ho8GgIoVQUvTEaiDmEvZTWCXHx5vYNZxFy08g2NhVn+LDQ/SQeh2lzYawW4WZq kcaFwyHnn8ZppPfoqI5baIRqNO0VGN7epCgkj899aSPqYoC6MwAPIRwH8Pr5lBul+Bta WKuYPbasP42p6UoJ3Lp2+dZorXfy55sdf0ODpdHUV9i3S7lslOtY4uCdTHtoTmYx1gX6 YyigODwMfe8nBjBVKzZVqmDcxww96PJKWcc+/sJpa1ik1zi6cDcFvRgTntHg1iOCgYaW lT7g== 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: 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 d4si134744wmh.2.2018.03.07.13.01.11 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 07 Mar 2018 13:01:12 -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 w27L0uTH027074; Wed, 7 Mar 2018 22:00:56 +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 w27L19RF018801; Wed, 7 Mar 2018 22:01:09 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id B80C51A0A21; Wed, 7 Mar 2018 22:01:09 +0100 (CET) Date: Wed, 7 Mar 2018 22:01:09 +0100 From: Thomas Streicher To: Peter LeFanu Lumsdaine Cc: Michael Shulman , "HomotopyT...@googlegroups.com" Subject: Re: [HoTT] Categories with 2-families Message-ID: <20180307210109.GA12590@mathematik.tu-darmstadt.de> References: <20180307170902.GA5070@mathematik.tu-darmstadt.de> <20180307203003.GA11083@mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: 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.7.205116 X-PMX-RELAY: outgoing > To clarify, by ???discrete comprehension categories??? I mean the ones Mike was > talking about, i.e. where the fibration of types is a discrete fibration; I > don???t mean that the base category is discrete. So there???s no problem here > ??? terms are still interpreted as sections of dependent projections, just as > usual. Ok, that's like interpretation in categories with attributes, where terms are interpreted in the base and only types in the fibers of the presheaf of types. But such guys considered as comprehension cats are full. Maybe you just say that non-full comprehension cats are not useful for type theory which I fully agree with! (In other contexts like fibrational approach to geom.morph's non-full comprehensions cats are most useful but not in full generality, one just requires the fibrations to have comprehension which is a property not structure.) But it's not enough to require the splitting for types. One also has to require it for the associate FULL comprehension cat. E.g. it's not sufficient to have it for Pi, you must also have it for eval. Thomas