From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x238.google.com (mail-oi1-x238.google.com [IPv6:2607:f8b0:4864:20::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b843c514 for ; Tue, 7 May 2019 22:06:24 +0000 (UTC) Received: by mail-oi1-x238.google.com with SMTP id r84sf6429649oia.9 for ; Tue, 07 May 2019 15:06:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=C5lbKaBu6xhC5BE2Jxj7VRQEwovqqtWpTLMIB1Mid44=; b=Lrm4yOd7AKdI+UliUNMSnEG/iZtOdDzHtSZQZ/6GxO7RIIlDkUyIpqkfrCHq/cQuI8 y9Njy0xa1vFNm1w83YdtSrXkN3+EyTH5YBJYsbb+PzMuT/3kJIgxaHIuMyZWGbl17F/i DA3EzN8NlY2hXRWlkRufAhHR6QIeiGoImwrbhI9BYNbK4VOsV3wmFEB/Ed1X6Amm95nn JRhKbWOBDedUWHNBS0OHQ+SL9moIkXGcWKWd2H3x3jvARQiOJi1rqoFHOCLtRk7OeYwD C1WfRlCumb1CSW9LrCeAneG9bqg68USpIP+GA9PEeasC4l52Nvxht/aLzOQxuxB38mWc 174w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=C5lbKaBu6xhC5BE2Jxj7VRQEwovqqtWpTLMIB1Mid44=; b=HS3fWjTg/6F8xjn1jbNtN01HiQcUUjOvYxHenUeFiM9fXW6NyTnb9ATFFy6HQ5O4G7 5WgzTuAvPAVNS2m33PIAwg+cCY6i/K0bEk5xcl/TAmsH8EYfTvNz3GV0JRaSveohXqOD sZANQ0svwiGrooZIDFvNKyy3DMupyGkTSKbFRWoBvXXWB6Gz3yDTMsbqNUKEtEEcbJH6 u/uNKxISdEJ2ZoRs+RB4HihEcPbFMoZnWQkPfjnjMmndHbg4keYYSL4sdz33wjy1aU0/ vWHN3NJQM7iRKqNCRBpFcbtsR0OY/VFfQssUOLeyK6xDAj9ehbNAM08O4Zq7q8GhIOBS Toeg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=C5lbKaBu6xhC5BE2Jxj7VRQEwovqqtWpTLMIB1Mid44=; b=INcJmA4+9AQjm8yJ3AGEaseld2dHOpnZlSFi+7Z9FC1wnpk45N5c42EXay6nuvyC4d QXkaEji1iHZ1j9ID8g5GzJ/Gf0nDll1Cidg3c+5HgxZZ7ve2Dz9gQEDrneAjCTwMRSNM HPrO4ZfclLREUQZjEi4kgxKV1O4UnVck+RBIf4I8hUxybczcVJC3fPUGLOXZmIAIlMxB WKGDt5tbqTmve4+/at6rrVpF4Ket3knqXapRMdjj1bD7UlOC4+yXaPs7y1PZpAEJ6R4f prO6O9HkqnURmB7xvkTTNF/Q2jdcO/RbLvTTS6GU+FqlkbwMWJ4MsRaFDEeDhs2svgls 4tZw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVP49nHwlaYiv7aGe/C/Tf+OhHVKGj0Gx3OGtp5BwULizA+O0yl hLdpykgVCzRluehQET5IJ5Q= X-Google-Smtp-Source: APXvYqz+6BB4RcLGyXDWX8ImsqImgazim4giLwMK6CR/HWOPJyHzhnWaa2EyAtftPWYVgh6qpD40Iw== X-Received: by 2002:a05:6830:1d4:: with SMTP id r20mr24522846ota.350.1557266783031; Tue, 07 May 2019 15:06:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5f1a:: with SMTP id f26ls3174137oti.2.gmail; Tue, 07 May 2019 15:06:22 -0700 (PDT) X-Received: by 2002:a9d:3982:: with SMTP id y2mr11592180otb.36.1557266780975; Tue, 07 May 2019 15:06:20 -0700 (PDT) Date: Tue, 7 May 2019 15:06:20 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <6bae18da-1ecc-4633-a565-9df222140d87@googlegroups.com> In-Reply-To: <49d95599-153c-d641-4ae9-a3f7c02b1cc3@gmail.com> References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> <5fa99a80-56ed-abc5-d64f-876c192bca6a@cse.gu.se> <49d95599-153c-d641-4ae9-a3f7c02b1cc3@gmail.com> Subject: Re: [HoTT] Injective types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_46_164228169.1557266780368" X-Original-Sender: escardo.martin@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_46_164228169.1557266780368 Content-Type: multipart/alternative; boundary="----=_Part_47_60308460.1557266780368" ------=_Part_47_60308460.1557266780368 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On 07/05/2019 14:51, Andreas Nuyts wrote: > Even with cumulativity, that sounds suspicious, because cumulativity of= =20 > U in a bigger universe V does not obviously give you a map >=20 > (A B : U) -> Id V A B -> Id U A B. >=20 > The J-rule does not allow you to build this map. Indeed. In the non-cumulative system, with V bigger than U, you have a map f : U =E2=86=92 V with f A =E2=89=83 A. For example, if C is any contractib= le type in V, you can take f A :=3D A =C3=97 C. If both U and V are univalent, then any map f : U =E2=86=92 V with f A =E2= =89=83 A is an embedding for all A : U, meaning that the canonical map Id U A B =E2=86=92 Id V (f A) (f B) =20 is equivalence (or equivalently that the fibers of f are propositions). I checked this in Agda. The reformulation of your statement above with an explicit inclusion f : U =E2=86=92 V, namely (A B : U) -> Id V (f A) (f B) -> Id U A B, which amounts to the left-cancellability of f, is a consequence of f being an embedding, and in general strictly weaker than f being an embedding. But I don't see how to prove even the left-cancellability of f without assuming univalence in the smaller universe U. Assuming that V is univalent, Id V (f A) (f B) gives f A =E2=89=83 f B, and then composing with the equivalences A =E2=89=83 f A and f B =E2=89=83 B we= get A =E2=89=83 B. If U were univalent we would get Id U A B and hence f would be left-cancellable. But, as I said, the univalence of U and V gives more, namely that f is an embedding. And if V is univalent and f is an embedding, then U is univalent, for A =E2=89=83 B is equivalent to f A =E2=89=83 f B and hence to Id V (f A) (f= B), and hence to Id U A B, using the embedding property in the last step. So if V is univalent, then the smaller universe U is univalent iff every map f : U =E2=86=92 V with f A =E2=89=83 A for all A : U is an embedd= ing (iff some given such map is an embedding). Martin >=20 > On 7/05/19 14:42, Nils Anders Danielsson wrote: >> On 02/05/2019 22.46, escardo.martin@gmail.com wrote: >>> I can confirm from a 26k line Agda development (with comments and >>> repeated blank lines removed in this counting of the number of lines) >>> that not once did I need to embed a universe into a larger universe, >>> except when I wanted to state the theorem that any universe is a >>> retract of any larger universe if one assumes the propositional >>> resizing axiom (any proposition in a universe U has an equivalent copy >>> in any universe V). So I would say that such situations are *extremely >>> rare* in practice. >> >> I once wrote some code where I made use of univalence at three different >> levels. Does anyone know if one can prove that univalence at one level >> implies univalence at lower levels, without making use of cumulativity? --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/6bae18da-1ecc-4633-a565-9df222140d87%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_47_60308460.1557266780368 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On 07/05/2019 14:51, Andreas Nuyts wrote:
&= gt; Even with cumulativity, that sounds suspicious, because cumulativity of= =C2=A0
> U in a bigger universe V does not obviously give you = a map
>=C2=A0
> (A B : U) -> Id V A B -> Id= U A B.
>=C2=A0
> The J-rule does not allow you t= o build this map.

Indeed.

In the non-cumulative system, with V bigger than U, you have a map
f : U =E2=86=92 V with f A =E2=89=83 A. For example, if C is any contrac= tible type in
V, you can take f A :=3D A =C3=97 C.

=
If both U and V are univalent, then any map f : U =E2=86=92 V wi= th f A =E2=89=83 A is
an embedding for all A : U, meaning that th= e canonical map

=C2=A0 Id U A B =E2=86=92 Id V (f = A) (f B)
=C2=A0=C2=A0
is equivalence (or equivalently t= hat the fibers of f are propositions).
I checked this in Agda.

The reformulation of your statement above with an ex= plicit inclusion
f : U =E2=86=92 V, namely

=C2=A0(A B : U) -> Id V (f A) (f B) -> Id U A B,

which amounts to the left-cancellability of f, is a consequence of = f
being an embedding, and in general strictly weaker than f being= an
embedding.

But I don't see how t= o prove even the left-cancellability of f without
assuming unival= ence in the smaller universe U.

Assuming that V is= univalent, Id V (f A) (f B) gives f A =E2=89=83 f B, and
then co= mposing with the equivalences A =E2=89=83 f A and f B =E2=89=83 B we get A = =E2=89=83 B.
If U were univalent we would get Id U A B and hence = f would be
left-cancellable. But, as I said, the univalence of U = and V gives
more, namely that f is an embedding.

And if V is univalent and f is an embedding, then U is univalent, = for
A =E2=89=83 B is equivalent to f A =E2=89=83 f B and hence to= Id V (f A) (f B), and
hence to Id U A B, using the embedding pro= perty in the last step.

So if V is univalent, then= the smaller universe U is univalent iff
every map f : U =E2=86= =92 V with f A =E2=89=83 A for all A : U is an embedding (iff
som= e given such map is an embedding).

Martin

>=C2=A0
> On 7/05/19 14:42, Nils Anders Da= nielsson wrote:
>> On 02/05/2019 22.46, escardo.martin@gmai= l.com wrote:
>>> I can confirm from a 26k line Agda deve= lopment (with comments and
>>> repeated blank lines remo= ved in this counting of the number of lines)
>>> that no= t once did I need to embed a universe into a larger universe,
>= ;>> except when I wanted to state the theorem that any universe is a<= /div>
>>> retract of any larger universe if one assumes the pr= opositional
>>> resizing axiom (any proposition in a uni= verse U has an equivalent copy
>>> in any universe V). S= o I would say that such situations are *extremely
>>> ra= re* in practice.
>>
>> I once wrote some co= de where I made use of univalence at three different
>> lev= els. Does anyone know if one can prove that univalence at one level
>> implies univalence at lower levels, without making use of cumul= ativity?

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/6bae18da-1ecc-4633-a565-9df222140d87%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_47_60308460.1557266780368-- ------=_Part_46_164228169.1557266780368--