From mboxrd@z Thu Jan 1 00:00:00 1970
X-Received: by 10.99.161.10 with SMTP id b10mr78213pgf.21.1507881789436;
Fri, 13 Oct 2017 01:03:09 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.99.112.14 with SMTP id l14ls1540209pgc.19.gmail; Fri, 13 Oct
2017 01:03:08 -0700 (PDT)
X-Received: by 10.99.113.7 with SMTP id m7mr82981pgc.95.1507881788290;
Fri, 13 Oct 2017 01:03:08 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1507881788; cv=none;
d=google.com; s=arc-20160816;
b=KZ3QtExdo3y5D93gFlTatYMSBtru3joEsEkCiUZImis7VovN8L8RkqhjAQ3HA6M1nE
SD0OKIUkjDFOqTcpxYv/kIVbsx8G9JH7UnWqHShGzYYvmVhloqtLzkN2QzQo3vEUOhc/
6ODfX5TFWTrG7AF+F4yHG1ZUKbpCSNVBfPB5zwrxfoa1HeTCqb9w23vDcqaGM2YeCT/L
SMRd4onBZ6mMhgK9pMBOsQdwooGOUQnPnx4ql7twEIp+Gwz8wJyQJpxU8iqIESwGX+KF
NJLX3RjaBj+Ew0c5LCxIw2bXEALck1xCiL/iLME0n6GEW+Tr0k0157L/6H+iAN/kNiHJ
GF7w==
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=64JS0PHAtd+TjTDBFAgGUfvXUW/NfdY/gsuq2hIruGo=;
b=YTw12pMwTTDNCRMat8LDnousVlWNQxHekENhiidM4Lzt98b0r4nfcMWYHW6ZpWlbi7
NMOP8XfDmCTurNx8Jf582B6qAdyvc7OXwW7gOky98SIorQmeiMtnNGd3v2ONdovnotym
XSXJtHfp26SIzJ5W4xEaM2mX62NfN/AkxH50qFFZHQh8XVR4RV6WtDr7JUQ28Ispt2BW
eLDK9KLrmP/Sya8y0HczaTk8Y8wQkGa28LDDydgIGVsMxQ5s07MPvSPiA+qtMzJuIOn6
MQ/hvKi9kIQYPhtIapZQAzV2MXU0MfqhbyQFEi1XZc0uwF/UMLyAG07J6xv+o1NBOYa/
Iqvw==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
dkim=pass head...@gmail.com header.s=20161025 header.b=s5rDV4ko;
spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com;
dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com
Return-Path:
Received: from mail-ua0-x22d.google.com (mail-ua0-x22d.google.com. [2607:f8b0:400c:c08::22d])
by gmr-mx.google.com with ESMTPS id w5si17328pfw.3.2017.10.13.01.03.08
(version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
Fri, 13 Oct 2017 01:03:08 -0700 (PDT)
Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) client-ip=2607:f8b0:400c:c08::22d;
Authentication-Results: gmr-mx.google.com;
dkim=pass head...@gmail.com header.s=20161025 header.b=s5rDV4ko;
spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com;
dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com
Received: by mail-ua0-x22d.google.com with SMTP id v27so4739603uav.7;
Fri, 13 Oct 2017 01:03:08 -0700 (PDT)
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=64JS0PHAtd+TjTDBFAgGUfvXUW/NfdY/gsuq2hIruGo=;
b=s5rDV4koFd2FAKQMc/E0sp/bRZ4eBiZG3I/qjDiVp5sJWH+rzowTwOEGrJMLG+5Hl/
qNiORvuOSMe28d15qAEuNxb0wMVn9V37bC9bBJ7/nQIw1RZYuppktOEn2Lw8+RTCXalt
VGrfwBi/pMBHhsBe3M7XZeK1RE3m+yo5usIL1UjhR4RVzyo7Tw5ZekP7j+6U5ICbv/rP
eCMDWQbp6Ck9VL2zOmHJT1RVCXl5nX/jPLKp2JEuE9SwQtK7acoME0GdCemU8pPWdDK3
FiHOjdQZS2cL8j0ai61QvhFZcau9Hs3UrtfcPyIX+BdohZIbe8nbCaxte0bNGF8srbWU
w7Eg==
X-Gm-Message-State: AMCzsaVqe3EqBLX6+n4tjWCe0ul/2aihmxDIN1fvlMM2wMdvsm6Erim1
zpZkhC5xWxeF7SoLsownMC9AkpCc2uSb9GUBhRE=
X-Received: by 10.176.82.36 with SMTP id i33mr500941uaa.117.1507881787475;
Fri, 13 Oct 2017 01:03:07 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.159.63.205 with HTTP; Fri, 13 Oct 2017 01:03:06 -0700 (PDT)
In-Reply-To:
References:
From: Peter LeFanu Lumsdaine
Date: Fri, 13 Oct 2017 10:03:06 +0200
Message-ID:
Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality
To: Dimitris Tsementzis
Cc: Homotopy Type Theory ,
Univalent Mathematics
Content-Type: multipart/alternative; boundary="94eb2c1907b84e4990055b6916f9"
--94eb2c1907b84e4990055b6916f9
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis wrote:
> Dear all,
>
> Let=E2=80=99s say a type theory TT is *initial* if its term model C_TT is=
initial
> among TT-models, where TT-models are models of the categorical semantics =
of
> type theory (e.g. CwFs/C-systems etc.) with enough extra structure to mod=
el
> the rules of TT.
>
I like the examples, but I would give a different analysis of what they
tell us.
The definition of =E2=80=9Cinitial=E2=80=9D presupposes that we have alread=
y defined what
=E2=80=9CTT-models=E2=80=9D means =E2=80=94 i.e. what the categorical seman=
tics should be. There
is as yet no proposed general definition of this (as far as I know).
Heuristically, there=E2=80=99s certainly a large class of type theories whe=
re we
understand what the categorical semantics are, and all clearly agree. But
rules like un-annotated cumulativity are *not* in this class. It=E2=80=99s=
not
clear what should correspond to un-annotated cumulativity, as a rule in
CwA=E2=80=99s (or CwF=E2=80=99s, C-systems, etc). A certain operation on t=
erms? An
operation, plus the condition that it=E2=80=99s mono? An assumption that t=
erms of
one type are literally a subset of terms of the other? Some of these will
make initiality clearly false; others may make it true but very
non-obviously so (that is, more non-obviously than usual).
So I don=E2=80=99t think we can say =E2=80=9CThese theories aren=E2=80=99t =
initial.=E2=80=9D =E2=80=94 but more
like =E2=80=9CWe=E2=80=99re not sure what the correct initiality statement =
is for these
theories, and some versions one might try are false.=E2=80=9D But I defini=
tely
agree that they show
> the claim that e.g. Book HoTT or 2LTT is initial cannot be considered
obvious
=E2=80=93p.
Then we have the following, building on an example of Voevodsky=E2=80=99s.
>
> *OBSERVATION*. Any type theory which contains the following rules
> (admissible or otherwise)
>
> =CE=93 |- T *Type*
> =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =
(C)
> =CE=93 |- B(T) *Type*
>
> =CE=93 |- t : T
> =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =
(R1)
> =CE=93 |- t : B(T)
>
> =CE=93 |- t : T
> =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =
(R2)
> =CE=93 |- p(t) : B(T)
>
> together with axioms that there is a type T0 in any context and a term t0
> : T0 in any context, is not initial.
>
> *PROOF SKETCH.* Let TT be such a type theory. Consider the type theory
> TT* which replaces (R1) with the rule
>
> =CE=93 |- t : T
> =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =
(R1*)
> =CE=93 |- q(t) : B(T)
>
> i.e. the rule which adds an =E2=80=9Cannotation=E2=80=9D to a term t from=
T that becomes a
> term of B(T). Then the category of TT-models is isomorphic (in fact, equa=
l)
> to the category of TT*-models and in particular the term models C_TT and
> C_TT* are both TT-models. But there are two distinct TT-model homomorphis=
ms
> from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends
> p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empt=
y,
> B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as
> they are interpreted in the term model C_TT).
>
> *COROLLARY. *Any (non-trivial) type theory with a =E2=80=9Ccumulativity" =
rule for
> universes, i.e. a rule of the form
>
> =CE=93 |- A : U0
> =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =
(U-cumul)
> =CE=93 |- A : U1
>
> is not initial. In particular, the type theory in the HoTT book is not
> initial (because of (U-cumul)), and two-level type theory 2LTT as present=
ed
> here is not initial (because of the
> rule (FIB-PRE)).
>
> The moral of this small observation, if correct, is not of course that
> type theories with the guilty rules cannot be made initial by appropriate
> modifications to either the categorical semantics or the syntax, but rath=
er
> that a bit of care might be required for this task. One modification woul=
d
> be to define their categorical semantics to be such that certain identiti=
es
> hold that are not generally included in the definitions of
> CwF/C-system/=E2=80=A6-gadgets (e.g. that the inclusion operation on univ=
erses is
> idempotent). Another modification would be to add annotations (by replaci=
ng
> (R1) with (R1*) as above) and extra definitional equalities ensuring that
> annotations commute with type constructors.
>
> But without some such explicit modification, I think that the claim that
> e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even
> entirely correct.
>
> Best,
>
> Dimitris
>
> PS: Has something like the above regarding cumulativity rules has been
> observed before =E2=80=94 if so can someone provide a relevant reference?
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
--94eb2c1907b84e4990055b6916f9
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
--94eb2c1907b84e4990055b6916f9--