From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.46.147 with SMTP id u141mr10281962ywu.114.1520455143655; Wed, 07 Mar 2018 12:39:03 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.224.135 with SMTP id j129ls157321ywe.28.gmail; Wed, 07 Mar 2018 12:39:02 -0800 (PST) X-Received: by 10.129.153.71 with SMTP id q68mr11283326ywg.29.1520455142753; Wed, 07 Mar 2018 12:39:02 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520455142; cv=none; d=google.com; s=arc-20160816; b=xAPFxlFXeS1i4SVE/AGgH35g5F+f8fzc8rE2o7DgNbkS1jcUrEEsBaOvijuXO6Qw9d RWyPZs6uPf8SwC/Zoptqjnx9L8k93yi0/sciA9jt8Q1vqHodRbjSkvHIonTu8nTKXXw2 gwc/BXPmaNEa+6BnC/lEvrkPPhRhhHOnbfFTBXhAZ8JQ3jn5vO5k8tWBrIUwAeO+cQcP r5LScX4ULRSwmOy6OUkLUnlwswar5ooUxkeii/8uI9SuWKBKyoUXmnvCTQoew+4GkMsU XAllEuKHGiYgeFdK28cDL/zp/ehC242QyTg3Ae6ORhXO0lXU3LcPJ0G7UdVxx1PtoDtr /11w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=z4aYeHi7QaBFDkWUrIkX5cTeKrkxYFRjJbyx8w8fGgA=; b=hodp6hTgd8hiwYivLCh5m4G08TPTC+fRRH2zLci22OmE0RAoFAWZ7K3j/sdiQVYCIA 6G/6TkGOdVB6Je/wIJB+RdVr9dHqbgEleOmtzkpEZdeKbvQFHwe1bpYJSrgJwFQS/A5v ELlMEVguTOW1k9v6KjxRLjSOPD0hnpn7AMNr34RItSgr9RA3+xl1JuVp+pRhGHOQkgzi SCBtdh9c45SnJk1WzBBe8hXTZZOv7sX+9F/e3Wv/B+hjGRxggNdJjAfnSD1ia7KGjAfR Nlq7Vk2ZvpcHrbA4+ywJfltCNmMYnOBV6dVpAoZy5NG8zg6sTXaYaz5W7bpIQEX8x54r fAlw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=imNjHNIe; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22c as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x22c.google.com (mail-vk0-x22c.google.com. [2607:f8b0:400c:c05::22c]) by gmr-mx.google.com with ESMTPS id s5-v6si1049842ybk.4.2018.03.07.12.39.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Mar 2018 12:39:02 -0800 (PST) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22c as permitted sender) client-ip=2607:f8b0:400c:c05::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=imNjHNIe; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22c as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-vk0-x22c.google.com with SMTP id z190so2226000vkg.1 for ; Wed, 07 Mar 2018 12:39:02 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=z4aYeHi7QaBFDkWUrIkX5cTeKrkxYFRjJbyx8w8fGgA=; b=imNjHNIevkufvXci08LMyKpQKIkNADYov+xD0h3uYNsmaZ5hYto3EXkt1MfoOGgSOQ wa2jiRnUTj93rBrd/UrX9z8NTcperBRVuubrBf1i89FdtOt/HPmU8q32ek9n2s1ZZ6QL KOnMg7w938UhadSDdNpD6Gvog6nnb9JgXzuyRmzI/1Q1oCnimCrurnsm1ElEvL/nWgZo ojTqkZFZ4yM711ECLHgyE9G1xIOryP9eldavSq8p8dDbRqgrpRr8iYksFGggVUfhoH2t JnOWMewasVnWqOzuFJqxqYRs18PT5e1oGGeuU3CzrY5b9+QUnzMXi8XIl09399PDgkj7 Fkcw== X-Gm-Message-State: APf1xPALU3G0SPVZebqzcCIBViC/AGB9rRWlEMublkoG+a5GXc5zYBnb TuJTNdvyp4jhJ8U2sL3hRW/Ub4pe2S0Dr9fTVXU= X-Received: by 10.31.134.147 with SMTP id i141mr16796091vkd.128.1520455142278; Wed, 07 Mar 2018 12:39:02 -0800 (PST) MIME-Version: 1.0 Received: by 10.176.48.209 with HTTP; Wed, 7 Mar 2018 12:39:01 -0800 (PST) In-Reply-To: <20180307203003.GA11083@mathematik.tu-darmstadt.de> References: <20180307170902.GA5070@mathematik.tu-darmstadt.de> <20180307203003.GA11083@mathematik.tu-darmstadt.de> From: Peter LeFanu Lumsdaine Date: Wed, 7 Mar 2018 21:39:01 +0100 Message-ID: Subject: Re: [HoTT] Categories with 2-families To: Thomas Streicher Cc: Michael Shulman , "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary="001a11411038a719480566d88c58" --001a11411038a719480566d88c58 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Wed, Mar 7, 2018 at 9:30 PM, Thomas Streicher < stre...@mathematik.tu-darmstadt.de> wrote: > 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). To clarify, by =E2=80=9Cdiscrete comprehension categories=E2=80=9D I mean t= he ones Mike was talking about, i.e. where the fibration of types is a discrete fibration; I don=E2=80=99t mean that the base category is discrete. So there=E2=80=99s = no problem here =E2=80=94 terms are still interpreted as sections of dependent projections,= just as usual. =E2=80=93p. --001a11411038a719480566d88c58 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

= On Wed, Mar 7, 2018 at 9:30 PM, Thomas Streicher <stre...= @mathematik.tu-darmstadt.de> wrote:
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).

To clarify, by= =E2=80=9Cdiscrete comprehension categories=E2=80=9D I mean the ones Mike w= as talking about, i.e. where the fibration of types is a discrete fibration= ; I don=E2=80=99t mean that the base category is discrete.=C2=A0 So there= =E2=80=99s no problem here =E2=80=94 terms are still interpreted as section= s of dependent projections, just as usual.

=E2=80= =93p.

--001a11411038a719480566d88c58--