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
--001a11411038a719480566d88c58--