From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 18 Dec 2017 14:58:19 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <0c1d71ec-3e8c-4cbf-9407-534a2b1f39de@googlegroups.com> In-Reply-To: References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> <86619505-c082-4c11-8d5d-9159e1b351ec@googlegroups.com> Subject: Re: [HoTT] Yet another characterization of univalence MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_961_1789935005.1513637899780" ------=_Part_961_1789935005.1513637899780 Content-Type: multipart/alternative; boundary="----=_Part_962_1036467946.1513637899781" ------=_Part_962_1036467946.1513637899781 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I am interested in the fact that Id_X : X =E2=86=92 (X =E2=86=92 U) is an e= mbedding (in the sense of univalent mathematics), because it gives this: The injective types are precisely the retracts of exponential powers of universes, where an exponential power of a type D is a type of the form A =E2=86=92 D for some type A. Injectivity is defined as (functional) data rather than property (using =CE=A3 rather than =E2=88=83). A type D is called injective if for any embedding j:X=E2=86=92Y, every function f:X=E2=86=92D extends to a map f':Y=E2=86=92D along j. This injectivity result depends crucially on univalence (even though the fact that Id_X is an embedding depends on much weaker hypotheses, as we've found out in this thread). It is also crucial that we say that j is an embedding (its fibers are propositions) rather than merely that j is left-cancellable. The following elaborates on this, with more comments and more technical results rendered in Agda. http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html We don't postulate anything in this development. Any axiom (UA, K, or FunExt) is used explicitly as an assumption whenever needed. The reason I came across injective types was my interest in searchable and omniscient types. (In a previous research life, I had already come across injective topological spaces when working on domain theory in the sense of Dana Scott, and what we do here is partly inherited from that.) This is also reported in this development:=20 http://www.cs.bham.ac.uk/~mhe/agda-new/index.html Some of this was reported in the past in this list. But there are new=20 things, in particular regarding injectivity. Martin. On Saturday, 9 December 2017 00:27:16 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote: > > On Friday, 1 December 2017 14:53:25 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote: >> >> >> OK. Here is a further weakening of the hypotheses. It suffices to have >> funext (again) and that the map >> >> idtofun{B}{C} : A=3DB =E2=86=92 (A=E2=86=92B) >> >> is left-cancellable (that is, idtofun p =3D idtofun q =E2=86=92 p=3Dq). >> >> Univalence gives that this is an embedding, which is stronger than >> saying that it is left-cancellable. And also K gives that this is an >> embedding. >> >> > I've written this down here in Agda : =20 > http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html > > (updating a 2015 development) > > * This is self-contained (doesn't use any library). > * A main feature is that instead of J (or pattern maching on refl), thi= s=20 > uses the Yoneda machinery everywhere instead (regretably with just one=20 > exception (I'd be grateful for suggestions of how to get rid of this use = of=20 > J)). > > A syntactical novelty is a new notation for universes in Agda closer to= =20 > the notation in the HoTT book for informal mathematics in type theory. Th= is=20 > could be further improved by making it built-in in Agda (as explained in= =20 > the imported NonStandardUniverseNotation.lagda), but probably it is good= =20 > enough without any modification to Agda. > > Martin > > =20 > ------=_Part_962_1036467946.1513637899781 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
I am interested in the fact that Id_X : X =E2=86=92 (= X =E2=86=92 U) is an embedding
(in the sense of univalent mathema= tics), because it gives this:

=C2=A0 The injective= types are precisely the retracts of exponential powers
=C2=A0 of= universes, where an exponential power of a type D is a type of
= =C2=A0 the form A =E2=86=92 D for some type A.

Inj= ectivity is defined as (functional) data rather than property
(us= ing =CE=A3 rather than =E2=88=83).

A type D is cal= led injective if for any embedding j:X=E2=86=92Y, every
function = f:X=E2=86=92D extends to a map f':Y=E2=86=92D along j.

This injectivity result depends crucially on univalence (even thou= gh
the fact that Id_X is an embedding depends on much weaker hypo= theses,
as we've found out in this thread).

It is also crucial that we say that j is an embedding (its fibers a= re
propositions) rather than merely that j is left-cancellable.

The following elaborates on this, with more comment= s and more
technical results rendered in Agda.

http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html

We don't postulate anything in this development. Any ax= iom (UA, K, or
FunExt) is used explicitly as an assumption whenev= er needed.

The reason I came across injective type= s was my interest in searchable
and omniscient types. (In a previ= ous research life, I had already come
across injective topologica= l spaces when working on domain theory in
the sense of Dana Scott= , and what we do here is partly inherited from
that.) This is als= o reported in this development:=C2=A0

http://www.c= s.bham.ac.uk/~mhe/agda-new/index.html

Some of = this was reported in the past in this list. But there are new=C2=A0
things, in particular regarding injectivity.

Ma= rtin.


On Saturday, 9 December 2017 00:27:16 UTC, Ma= rt=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote:
On Friday, 1 December 2017 14:53:25 UTC, Mart= =C3=ADn H=C3=B6tzel Escard=C3=B3 wrote:

=C2=A0OK. Here is a further weake= ning of the hypotheses. It suffices to have
funext (again) and th= at the map

=C2=A0 =C2=A0 idtofun{B}{C} : A=3DB =E2= =86=92 (A=E2=86=92B)

is left-cancellable (that is,= idtofun p =3D idtofun q =E2=86=92 p=3Dq).

Univale= nce gives that this is an embedding, which is stronger than
sayin= g that it is left-cancellable. And also K gives that this is an
e= mbedding.


I'= ve written this down here in Agda :=C2=A0=C2=A0http://www.cs.bham.ac.uk/~mhe/yo= neda/yoneda.html

(updating a 2015 development)=

=C2=A0 * This is self-contained (doesn't use = any library).
=C2=A0 * A main feature is that instead of J (or pa= ttern maching on refl), this uses the Yoneda machinery everywhere instead (= regretably with just one exception (I'd be grateful for suggestions of = how to get rid of this use of J)).

A syntactical n= ovelty is a new notation for universes in Agda closer to the notation in th= e HoTT book for informal mathematics in type theory. This could be further = improved by making it built-in in Agda (as explained in the imported NonSta= ndardUniverseNotation.lagda), but probably it is good enough without a= ny modification to Agda.

Martin

=C2=A0=C2=A0
------=_Part_962_1036467946.1513637899781-- ------=_Part_961_1789935005.1513637899780--