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=-0.9 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-ot1-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c9af1ec1 for ; Thu, 15 Nov 2018 11:05:46 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id m52sf7144579otc.13 for ; Thu, 15 Nov 2018 03:05:45 -0800 (PST) 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=75iEBLrmqHCwAaBfZbte2yC99KCEI5d4XUhiJ6kQNT0=; b=eUIbi5Ybh0pelkkfG3mawXjbHSFrLiOetRxNU6WBna41gOaVLV6CHrLjSnb3MTwfXw w9hkq/dY0rfpDj+XwGJzMz/GgC7cVZiHTwO2+vk22mqCgFD1U2vRkdBbUMpxeGyvzp7m JNM2szgBDjmeEF+iRUWSxpSOZnYpPYY9W/+OnRwP0bVMmcL8xia5BHhSSRRMs2Jv+UXg JoPknUsg0FE8DrO1sDudmTgSqOzC3zezPrtKaBm9KNumPVQDAKwQLg0TbGDiSDl2c5n5 U0DQ3V3FvGIZ8olJx1r4B4y87gLTfyjwQD5nQ9rmJw89akhNuLHfRoImnTy16IjDj8i9 F73w== 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=75iEBLrmqHCwAaBfZbte2yC99KCEI5d4XUhiJ6kQNT0=; b=UePe4e94qb7EcrBqlrajNcReUJAS0BYik9FknJ1i9H5lDI1WK8JTA4ybrwtKLAh57b ySVohrONXsGdY/j7rmkWmECnUK7vi8mP/N++0gPxkWzBg6qoIzrGfh+GvHB6r8p+wfd0 GG6BVisSQMRp3tJO3T2ckj4c32SS244reJqQ9LfoU8bloAR/d+dEpj67muHmzvOR852Z +KJp9ktFlVaECNgDmPfFiA4j4j3zulVyTtkB0JtuLlis+y0b0WNDhTFyfu0/bMjk8Doc UWTOi7a2fstog9+2ZVFXzBu2HpqTrJ+VN9Sz0S2NLrnHyEpSdHj2oJ5gIvuzn6Evfg4G SQnw== 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=75iEBLrmqHCwAaBfZbte2yC99KCEI5d4XUhiJ6kQNT0=; b=LcWQc7RLx5mq58PVtK7cewYV2trl5A2huWG7x9zDmLr3XoznwlqEvwTizLAxtPvP4w WDshV7OaHMUVvyNmFmHL1NdnqoRtYrWXlvd5sQfL3b9bwE6635IHC4duNpazBrp1ZpfR iaBh4K27qrPEX+twd7d+7t0JSu73npm8NaHxvK/6jSSNs29rE+m6by0uj+xgEpfFiawu gXcdqFyudRyiAXEZQ9JQs0+SSBJxC/OPiuWtfAE83MCFmCB9Q0qYrtg1KORmVdlx8bu6 q9sNUVxWzLkCCvvyNCrm1wrwiwXRkooy/gCphVFZ5lo1DEbSNqQr1y2lTrrXAY/5hyJF szMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKTZIykBEB/VVh9wkg77MKr07Ku9RtUVmiPvJKDYccGpBlb8Np6 JDNFjDPDtvUp2OZKgvXp4Mc= X-Google-Smtp-Source: AJdET5e71yJf0hCQrX6ipi6+8t5V9CdPHsFtM+YJEpSY8KpP1rU8sax7FzC5Xe3293eHvfHbfZ7JLQ== X-Received: by 2002:aca:889:: with SMTP id 131-v6mr27459oii.3.1542279944113; Thu, 15 Nov 2018 03:05:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d784:: with SMTP id o126-v6ls7980778oig.9.gmail; Thu, 15 Nov 2018 03:05:43 -0800 (PST) X-Received: by 2002:aca:308d:: with SMTP id w135mr254oiw.0.1542279943441; Thu, 15 Nov 2018 03:05:43 -0800 (PST) Date: Thu, 15 Nov 2018 03:05:42 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <246b6c0d-39c6-4279-8149-40d1129047fc@googlegroups.com> In-Reply-To: References: <0090c5e9-8e11-484c-953c-bf2958d03b72@googlegroups.com> <0472bc2b-0212-48b9-bfe7-fb98c7916763@googlegroups.com> <5b276491-e7b8-442a-b76a-d395f8e916a6@googlegroups.com> Subject: Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_401_68456287.1542279942557" 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_401_68456287.1542279942557 Content-Type: multipart/alternative; boundary="----=_Part_402_25827181.1542279942557" ------=_Part_402_25827181.1542279942557 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Here is my take on the independent proofs by Mike and Paolo. My aim in this version is to avoid calculations as much as possible. We want to show that the following map s is an embedding: s : (P =E2=86=92 =F0=9D=93=A4) =E2=86=92 =F0=9D=93=A4 s =3D =CE=A0 Our strategy will be to exhibit s as a composition of an equivalence followed by something that is clearly an embedding: (P =E2=86=92 =F0=9D=93=A4) =E2=89=83 M =E2=86=AA =F0=9D=93=A4 We take M :=3D =CE=A3 (X : =F0=9D=93=A4), is-equiv (=CE=BA X), where the function =CE=BA X : X =E2=86=92 (P =E2=86=92 X) is defined by =CE= =BA x p =3D x. The map M =E2=86=AA =F0=9D=93=A4 is simply the first projection. It is an e= mbedding because "being an equivalence" is a proposition. The equivalence (P =E2=86=92 =F0=9D=93=A4) =E2=89=83 M is easy. Given A : P= =E2=86=92 =F0=9D=93=A4 we take X to be the type s A, with a short argument to show that the map =CE=BA(s A) is an equivalence. Conversely, given X : =F0=9D=93=A4 such that =CE=BA X is an eq= uivalence, we take A to be the constant family (p =E2=86=A6 X). It is direct and short= to check that this does give an inverse (using function extensionality and=20 univalence). By construction, the map s is the composition of the equivalence followed by the projection. Because equivalences are embeddings, and compositions of embeddings are embeddings, it follows that s is an embedding. I coded this in Agda here: http://www.cs.bham.ac.uk/~mhe/agda-new/UF-InjectiveTypes.html#17057 Thanks for your input! Martin On Wednesday, 14 November 2018 15:52:45 UTC, Michael Shulman wrote: > > Here's a sketch of a more conceptual argument. Both =F0=9D=93=A4 and P = =E2=86=92 =F0=9D=93=A4 are=20 > the object-types of (oo-)categories, and =CE=A0 is the object-map of a=20 > right adjoint functor whose counit is an equivalence. Thus, by a=20 > standard argument, it is fully faithful, and hence also fully faithful=20 > on equivalences (which, by univalence, are the equalities). Of course=20 > we can't define the whole oo-categories in Book HoTT, but I think this=20 > is one of those arguments that only needs the 1- or 2-dimensional=20 > structure.=20 > On Wed, Nov 14, 2018 at 3:07 AM Paolo Capriotti > wrote:=20 > >=20 > > On Tue, 13 Nov 2018, at 8:32 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 w= rote:=20 > > > Let P be a subsingleton and =F0=9D=93=A4 be a universe, and consider = the=20 > > > product map=20 > > >=20 > > > =CE=A0 : (P =E2=86=92 =F0=9D=93=A4) =E2=86=92 =F0=9D=93=A4=20 > > > A =E2=86=A6 =CE=A0 (p:P), A(p).=20 > > >=20 > > > Is this an embedding? (In the sense of having subsingleton=20 > > > fibers.)=20 > > >=20 > > > It is easy to see that this is the case if P=3D=F0=9D=9F=98 or P=3D= =F0=9D=9F=99 (empty or=20 > > > singleton type).=20 > > >=20 > > > But the reasons are fundamentally different:=20 > > >=20 > > > (0) If P=3D=F0=9D=9F=98, the domain of =CE=A0 is equivalent to =F0=9D= =9F=99, and =CE=A0 amounts to=20 > > > the map =F0=9D=9F=99 =E2=86=92 =F0=9D=93=A4 with constant value = =F0=9D=9F=99.=20 > > >=20 > > > In general, a function =F0=9D=9F=99 =E2=86=92 X into a type X is = *not* an=20 > > > embedding. Such a function is an embedding iff it maps the=20 > > > point of =F0=9D=9F=99 to a point x:X such that the type x=3Dx is = a=20 > > > singleton.=20 > > >=20 > > > And indeed for X:=3D=F0=9D=93=A4 we have that the type =F0=9D=9F= =99=3D=F0=9D=9F=99 is a singleton.=20 > > >=20 > > > (1) If P=3D=F0=9D=9F=99, the domain of =CE=A0 is equivalent to =F0=9D= =93=A4, and =CE=A0 amounts to=20 > > > the identity map =F0=9D=93=A4 =E2=86=92 =F0=9D=93=A4, which, bein= g an equivalence, is an=20 > > > embedding.=20 > > >=20 > > > Question. Is there a uniform proof that =CE=A0 as above for P a=20 > > > subsingleton is an embedding, without considering the case=20 > > > distinction (P=3D=F0=9D=9F=98)+(P=3D=F0=9D=9F=99)?=20 > >=20 > > I think one can show that ap =CE=A0 is an equivalence by giving an inve= rse.=20 > Given X, Y : P =E2=86=92 =F0=9D=93=A4, first note that the equality type = X =3D Y is equivalent=20 > by function extensionality to (u : P) =E2=86=92 X u =3D Y u. Since one ca= n prove=20 > easily that (u : P) =E2=86=92 X u =3D =CE=A0 X, it follows that X =3D Y i= s equivalent to P =E2=86=92=20 > =CE=A0 X =3D =CE=A0 Y. Hence we get a map =CF=89 : =CE=A0 X =3D =CE=A0 Y = =E2=86=92 X =3D Y. To show that it is=20 > indeed an inverse of ap =CE=A0, start with some =CE=B1 : =CE=A0 X =3D =CE= =A0 Y. By following the=20 > construction above, we get that ap =CE=A0 (=CF=89 =CE=B1) maps a function= h : =CE=A0 X to =CE=BB u .=20 > =CE=B1 (=CE=BB v . tr^X [u,v] (h u)) u, where [u,v] : u =3D v is given by= the fact that=20 > P is a proposition. Now, within the assumption u : P, the =CE=BB expressi= on in=20 > brackets is equal to h itself, hence ap =CE=A0 (=CF=89 =CE=B1) =3D =CE=B1= . The other composition=20 > is easier, since it can just be checked on reflexivity.=20 > >=20 > > Best,=20 > > Paolo=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com = .=20 > > > For more options, visit https://groups.google.com/d/optout.=20 > --=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. For more options, visit https://groups.google.com/d/optout. ------=_Part_402_25827181.1542279942557 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Here is my take on the independent proofs by Mike and= Paolo. My aim in
this version is to avoid calculations as much a= s possible.

We want to show that the following map= s is an embedding:

=C2=A0s : (P =E2=86=92 =F0=9D= =93=A4) =E2=86=92 =F0=9D=93=A4
=C2=A0s =3D =CE=A0

<= /div>
Our strategy will be to exhibit s as a composition of an equivale= nce
followed by something that is clearly an embedding:

=C2=A0 (P =E2=86=92 =F0=9D=93=A4) =E2=89=83=C2=A0 M =E2=86= =AA =F0=9D=93=A4

We take M :=3D =CE=A3 (X : =F0=9D= =93=A4), is-equiv (=CE=BA X),
where the function =CE=BA X : X =E2= =86=92 (P =E2=86=92 X) is defined by =CE=BA x p =3D x.

=
The map M =E2=86=AA =F0=9D=93=A4 is simply the first projection. It is= an embedding
because "being an equivalence" is a propo= sition.

The equivalence (P =E2=86=92 =F0=9D=93=A4)= =E2=89=83 M is easy. Given A : P =E2=86=92 =F0=9D=93=A4 we take X to be
the type s A, with a short argument to show that the map =CE=BA(s A= ) is an
equivalence. Conversely, given X : =F0=9D=93=A4 such that= =CE=BA X is an equivalence,
we take A to be the constant family = (p =E2=86=A6 X). It is direct and short to
check that this does g= ive an inverse (using function extensionality and=C2=A0
univalenc= e).

By construction, the map s is the composition = of the equivalence
followed by the projection.

Because equivalences are embeddings, and compositions of embeddings<= /div>
are embeddings, it follows that s is an embedding.

=
I coded this in Agda here:
http://www.cs.bham.ac.uk/~m= he/agda-new/UF-InjectiveTypes.html#17057

Thanks fo= r your input!

Martin


On We= dnesday, 14 November 2018 15:52:45 UTC, Michael Shulman wrote:
Here's a sketch of a more conceptual a= rgument. =C2=A0Both =F0=9D=93=A4 and P =E2=86=92 =F0=9D=93=A4 are
the object-types of (oo-)categories, and =CE=A0 is the object-map of a
right adjoint functor whose counit is an equivalence. =C2=A0Thus, by a
standard argument, it is fully faithful, and hence also fully faithful
on equivalences (which, by univalence, are the equalities). =C2=A0Of co= urse
we can't define the whole oo-categories in Book HoTT, but I think t= his
is one of those arguments that only needs the 1- or 2-dimensional
structure.
On Wed, Nov 14, 2018 at 3:07 AM Paolo Capriotti <p.cap...@gmail.com&= gt; wrote:
>
> On Tue, 13 Nov 2018, at 8:32 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 wrote:
> > Let P be a subsingleton and =F0=9D=93=A4 be a universe, and c= onsider the
> > product map
> >
> > =C2=A0 =CE=A0 : (P =E2=86=92 =F0=9D=93=A4) =E2=86=92 =F0=9D= =93=A4
> > =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0A =C2=A0 =C2=A0 =E2=86=A6 = =CE=A0 (p:P), A(p).
> >
> > Is this an embedding? (In the sense of having subsingleton
> > fibers.)
> >
> > It is easy to see that this is the case if P=3D=F0=9D=9F=98 o= r P=3D=F0=9D=9F=99 (empty or
> > singleton type).
> >
> > But the reasons are fundamentally different:
> >
> > (0) If P=3D=F0=9D=9F=98, the domain of =CE=A0 is equivalent t= o =F0=9D=9F=99, and =CE=A0 amounts to
> > =C2=A0 =C2=A0 the map =F0=9D=9F=99 =E2=86=92 =F0=9D=93=A4 wit= h constant value =F0=9D=9F=99.
> >
> > =C2=A0 =C2=A0 In general, a function =F0=9D=9F=99 =E2=86=92 X= into a type X is *not* an
> > =C2=A0 =C2=A0 embedding. Such a function is an embedding iff = it maps the
> > =C2=A0 =C2=A0 point of =F0=9D=9F=99 to a point x:X such that = the type x=3Dx is a
> > =C2=A0 =C2=A0 singleton.
> >
> > =C2=A0 =C2=A0 And indeed for X:=3D=F0=9D=93=A4 we have that t= he type =F0=9D=9F=99=3D=F0=9D=9F=99 is a singleton.
> >
> > (1) If P=3D=F0=9D=9F=99, the domain of =CE=A0 is equivalent t= o =F0=9D=93=A4, and =CE=A0 amounts to
> > =C2=A0 =C2=A0 the identity map =F0=9D=93=A4 =E2=86=92 =F0=9D= =93=A4, which, being an equivalence, is an
> > =C2=A0 =C2=A0 embedding.
> >
> > Question. Is there a uniform proof that =CE=A0 as above for P= a
> > subsingleton is an embedding, without considering the case
> > distinction (P=3D=F0=9D=9F=98)+(P=3D=F0=9D=9F=99)?
>
> I think one can show that ap =CE=A0 is an equivalence by giving an= inverse. Given X, Y : P =E2=86=92 =F0=9D=93=A4, first note that the equali= ty type X =3D Y is equivalent by function extensionality to (u : P) =E2=86= =92 X u =3D Y u. Since one can prove easily that (u : P) =E2=86=92 X u =3D = =CE=A0 X, it follows that X =3D Y is equivalent to P =E2=86=92 =CE=A0 X =3D= =CE=A0 Y. Hence we get a map =CF=89 : =CE=A0 X =3D =CE=A0 Y =E2=86=92 X = =3D Y. To show that it is indeed an inverse of ap =CE=A0, start with some = =CE=B1 : =CE=A0 X =3D =CE=A0 Y. By following the construction above, we get= that ap =CE=A0 (=CF=89 =CE=B1) maps a function h : =CE=A0 X to =CE=BB u . = =CE=B1 (=CE=BB v . tr^X [u,v] (h u)) u, where [u,v] : u =3D v is given by t= he fact that P is a proposition. Now, within the assumption u : P, the =CE= =BB expression in brackets is equal to h itself, hence ap =CE=A0 (=CF=89 = =CE=B1) =3D =CE=B1. The other composition is easier, since it can just be c= hecked on reflexivity.
>
> Best,
> Paolo
>
> --
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.go= ogle.com/d/optout.

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_402_25827181.1542279942557-- ------=_Part_401_68456287.1542279942557--