From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.115.15 with SMTP id o15mr1579683ljc.16.1520454608511; Wed, 07 Mar 2018 12:30:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.65.141 with SMTP id d13ls295216ljf.11.gmail; Wed, 07 Mar 2018 12:30:07 -0800 (PST) X-Received: by 10.46.67.147 with SMTP id z19mr1590570lje.24.1520454607027; Wed, 07 Mar 2018 12:30:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520454606; cv=none; d=google.com; s=arc-20160816; b=URkJEwc5lLAHaem3Cf3AqYSck6qHIIehA8l8OhaYILy/S2WuqxJGU4ElBXxekOBmAb O13JPaBnDCY2He9UN/3qv60buXZXpPdwN26eDOumddq+BTW6sGcqR83Kq9dvHHMV2VMc 37N/PjCia5KiCUCxSKyTQzYEYHtVA7+hTFi0sKdkFg1r4cfil1ulnXzEsdjaS04Iz/Ys IMinnOwQrEbz8bqfsoAM8Nmyp3CPns03eFwclZMTTxmHsFY+GA5WZM4aatawtBqepI7T 4xB2DImWzyUbQn9Z/ZR+GUM+AsphPF2pawjJ769YWYwKRY72JKjnwwNZpKUMkdc7xxTJ 2zgw== 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=jFn5U+kEYxCnTEEuGUhS32HkGmzVWaceDt+4UmiZSyI=; b=R0MORz+TKiSuDvwa7k8vA8UOTJoWyTUvc65/JOFxfAsLlK9f+3DGZp4dq1GmPcuUJp GTLTxozoqSeXYAdlsRVNe35ins+vRmMSxAQUUI8J32DV4Q9j6BnOJ9BdYAeCGnkUJfQR i3A7WBlgneSRpbcVax5EE4xHaiaHsMrDEe4cansWe6gwHA3zHsCKizJZSFMcAIe+8VaD lUxPcGCcKS8kZswMyZ4drEv4lY/hNfSUzNHr85jTlxAyftA6qwvqWqts2dmRBM0ZU1rB NmE65J63do/OMry8aB5F+55Fs+m41om9WP00vuEr2enDxq+TqOUhC7TwDbHsFdU+3T9+ 07Hg== 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.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx500.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.156.225]) by gmr-mx.google.com with ESMTPS id s26si770924lfi.1.2018.03.07.12.30.06 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 07 Mar 2018 12:30:06 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) client-ip=130.83.156.225; 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.225 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 lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id w27KTivi031052; Wed, 7 Mar 2018 21:29:45 +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 w27KU3RF018652; Wed, 7 Mar 2018 21:30:03 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id B40CC1A0A21; Wed, 7 Mar 2018 21:30:03 +0100 (CET) Date: Wed, 7 Mar 2018 21:30:03 +0100 From: Thomas Streicher To: Peter LeFanu Lumsdaine Cc: Michael Shulman , "HomotopyT...@googlegroups.com" Subject: Re: [HoTT] Categories with 2-families Message-ID: <20180307203003.GA11083@mathematik.tu-darmstadt.de> References: <20180307170902.GA5070@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.202115 X-PMX-RELAY: outgoing But if you specialize the interpretation of type theory in comprehension categories to discrete ones you wan't be able to interpret terms (since the latter are interpreted as morphism in the fibers, namely as sections). So I am not sure what you mean... Thomas