From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.50.4 with SMTP id y4mr2046928wmy.1.1520442550832; Wed, 07 Mar 2018 09:09:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.152.137 with SMTP id a131ls548761wme.2.gmail; Wed, 07 Mar 2018 09:09:09 -0800 (PST) X-Received: by 10.28.190.24 with SMTP id o24mr2054038wmf.10.1520442549027; Wed, 07 Mar 2018 09:09:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520442548; cv=none; d=google.com; s=arc-20160816; b=JXTIV/BlQvHbNmq98PTsr1IkzjstmVn95IQBPOd5ZsDq8xaQNADgxpJ1M+MhBBnIxH J+EdM69Nvu7BvHApfke4jlQj8et0pINpWvhynNyLh9kLhABhs0gUuxEki/OK0ZiVLbnm ej7uWfg1gZpzERBweqy3VSnd5sH/NzCTHbBfha/91vjohuHc0zV63lztC6tP8kLSp/GH ESV9/Pk49kxLQl0i7Cu7WC0z9EL25CwBJinlOY6zmGSxMVwtABY+hiMYcNjwn7z4+uQB s5GBksPRjnOn5X+uzJ3efKyzTInsicbjWZo7mWXQK81eeAHbWACZJ2HmX0kQifoCyo/y DC9Q== 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=mJ8O9hICi9GbI9R6/M8g4EP7X35Y0zXATsYzAh9y0dM=; b=HePmoChecS7/aJY7WBSTpjMzty0lvz1kei/8djID0zkFLJ59qP4QWuF/WU4LMhzXEo QoI8PWDhgbxe295lA7Qgkqz/sKuYFjqwwb+RKVC4RsbNhnb5zcckCbrQfEaCJgzbjoUU +QS6wlujN03+a5UeRg+KtS6dv1z11JAiHoEypeVmjAKzshhiddo6rFqiSGG1Q70Gcda5 iValdreGSskU9smOwgyyOP+z3FGLFsWeQAvxEc5DQUJh4+yEilFAZMnijjGpf6KTuZ2E 81KBMVqdlUExOZ+8c4GD4ikzIkgD8tsMVA9R9Np1rXDdSrUknlqxhcgcTTHr6wfM3I1M bX3g== 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 r10si565046wmg.2.2018.03.07.09.09.08 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 07 Mar 2018 09:09: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 w27H8sbd003661; Wed, 7 Mar 2018 18:08:55 +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 w27H92RF015902; Wed, 7 Mar 2018 18:09:02 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id A3F501A0AC4; Wed, 7 Mar 2018 18:09:02 +0100 (CET) Date: Wed, 7 Mar 2018 18:09:02 +0100 From: Thomas Streicher To: Michael Shulman Cc: "HomotopyT...@googlegroups.com" Subject: Re: [HoTT] Categories with 2-families Message-ID: <20180307170902.GA5070@mathematik.tu-darmstadt.de> References: 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.170016 X-PMX-RELAY: outgoing On Mon, Mar 05, 2018 at 01:29:56PM -0800, Michael Shulman wrote: > By a standard construction (described for example at > https://ncatlab.org/nlab/show/categorical+model+of+dependent+types), > categories with families are equivalent to categories with attributes, > i.e. to comprehension categories that are discrete fibrations. That's misleading I think. One rather should think categories with attributes as full comprehension categories (like any surjective map from a class S to Ob(C) allows one construct a category equivalent to C whose collection of objects is S). Thomas