From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.37.97.1 with SMTP id v1mr788734ybb.85.1507847504626; Thu, 12 Oct 2017 15:31:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.129.122.7 with SMTP id v7ls391993ywc.10.gmail; Thu, 12 Oct 2017 15:31:43 -0700 (PDT) X-Received: by 10.129.172.25 with SMTP id k25mr7843335ywh.228.1507847503861; Thu, 12 Oct 2017 15:31:43 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507847503; cv=none; d=google.com; s=arc-20160816; b=pFrHZowfY8rZlRPbof4CJWh7U5gw2s8Pcjm8GGuBb/aqRlzpGuD9t8O63kUi/EJcC8 KSDMTP5GakD5cF44/GqMi4MvdJYW3IYJ9+Z4ht7r/49XxDTw5bWDOcQz+q0/DqZEOTr+ KsStEUtVIz1ZqFjofYLqM0mCJs2ie5A2v+n26Or0Ujoi03Um6gEpcpufGGGQEQblmaiN ktkOLfIXYywZzX3tsjfvtfbYLrVW+CAfjUhkL+ilH/FJZ7m7QWeOT/ptkSUdQ2iPPXNs QQnDFpBmpgTT3OLzn8Vu8Ri362r0r+XoVQP0IQaQTBXxHyWL2ni4g7l8uy3WQOxXgNFk LuJQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=7xLdFCqI4gmJxXJuF6MMG17tobvfgRLCTFmqtu4FfLs=; b=FfDlkPhor/i4aN/kHsbLfbrLLiW2Lj6B2yvfsSU/H/o2XfFH1r61vXdBfErO1Q2s/w HDPtimxbA7d70vHIUfHlm8wQhFJHG8MPjvGnZsqEcnkeZOksTmECeO/oNt3lnWsE4iMC zvrVTcUUio5kq4EKcRu8SHYykU8AFptcOX9Kqm3nPcGhBtmZ1OLLH3Dm8dB1JAm11A48 cSBZ2PkuFacc9UMR6RpfB+V39G4IzdggO+EmLSOX82KHTAlk1AhBwsIA0Yjkraqg8uDJ qzOtrQz88n/92kjfQaOaJVFa1ZX0O9SktBKkf92dj9CFJl8fwfG6WckaONzkIsRHkKv5 KzZw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Q3/perSc; spf=neutral (google.com: 2607:f8b0:400d:c0d::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x22c.google.com (mail-qt0-x22c.google.com. [2607:f8b0:400d:c0d::22c]) by gmr-mx.google.com with ESMTPS id d62si67998ybc.4.2017.10.12.15.31.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 15:31:43 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22c is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Q3/perSc; spf=neutral (google.com: 2607:f8b0:400d:c0d::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x22c.google.com with SMTP id k31so16426612qta.6 for ; Thu, 12 Oct 2017 15:31:43 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=7xLdFCqI4gmJxXJuF6MMG17tobvfgRLCTFmqtu4FfLs=; b=Q3/perScT4oTC8+BnHtUcRzTxvmkpaRQLCmlWVDYO/5RKzy4DdiK40HbtsYx/kxStD Xc7KrhxeH2czRp+O2+/6V0MZYk+fUvZ4eR83YdOsstqyz0WQsJs3WLEuOykSN3cxyTQo 4wqGwftrB+774BwBsN6MT+yhWTwWJ0e8Iuuyzd4BpE7r4FJ3Gwk44hKzlALf72GUcBHb zwtSTHGuRSrtsBHr2FZinxXJyTUa5kxQPbyHsyM3NFaEuHwTROlSL9nxdhVRpz509amC zyZIPlRVaHvVaAjMIMrjotLlbit4tBqsN/HKunECJCk+n++9KW0RitNyeb0U5DA8x5Md P3fA== X-Gm-Message-State: AMCzsaUQ2tA9TT2pvi/EzayVGOh+5QtFEU3a5Bx8u6MFkkoM+DL20YSp qA8XYXfovB5RlMiJRTpp1P5H62qe X-Received: by 10.37.37.131 with SMTP id l125mr2695076ybl.399.1507847503441; Thu, 12 Oct 2017 15:31:43 -0700 (PDT) Return-Path: Received: from mail-oi0-f49.google.com (mail-oi0-f49.google.com. [209.85.218.49]) by smtp.gmail.com with ESMTPSA id x189sm8077302ywx.90.2017.10.12.15.31.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 15:31:42 -0700 (PDT) Received: by mail-oi0-f49.google.com with SMTP id q4so10809931oic.7 for ; Thu, 12 Oct 2017 15:31:42 -0700 (PDT) X-Received: by 10.202.196.135 with SMTP id u129mr2195654oif.48.1507847502585; Thu, 12 Oct 2017 15:31:42 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Thu, 12 Oct 2017 15:31:21 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Thu, 12 Oct 2017 15:31:21 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Dimitris Tsementzis Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Oct 12, 2017 at 11:43 AM, Dimitris Tsementzis wrote: > But there are two distinct TT-model homomorphisms > 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 t= hey > are interpreted in the term model C_TT). I don't know how to interpret this. What is T0? What is t0? If t0:T0 then p(t0) : B(T0), so it seems that it can't be sent to qp(t0) or pq(t0) which belong to B(B(T0)). > COROLLARY. Any (non-trivial) type theory with a =E2=80=9Ccumulativity" ru= le 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. How does this yield an instance of the previous claim? What is B? What is= p?