From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 20 Dec 2017 12:46:39 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <7f3e4d3e-9204-4ca9-9a8c-7c8c5ed7936b@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> <0c1d71ec-3e8c-4cbf-9407-534a2b1f39de@googlegroups.com> Subject: Re: [HoTT] Yet another characterization of univalence MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2751_1985282777.1513802799310" ------=_Part_2751_1985282777.1513802799310 Content-Type: multipart/alternative; boundary="----=_Part_2752_1991421289.1513802799310" ------=_Part_2752_1991421289.1513802799310 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Tuesday, 19 December 2017 03:36:51 UTC, Gershom B wrote: On December 18, 2017 at 5:58:22 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3=20 (escar...@gmail.com) wrote:=20 > >=20 > > A type D is called injective if for any embedding j:X=E2=86=92Y, every= =20 > > function f:X=E2=86=92D extends to a map f':Y=E2=86=92D along j.=20 >=20 > Here is a question: given a local operator (Lawvere-Tierny topology)=20 > j, an object D is a sheaf if for any j-dense subobject X >-> Y, every=20 > function f : X -> D extends to a map f=E2=80=99 : Y -> D. Is there a way = in=20 > which we can view injective types as sheafs in some appropriate sense?=20 I don't think so, because we don't have the required uniqueness of the sheaf condition here. In general, if a type D is injective, many extensions of any f:X=E2=86=92D along an embedding j:X=E2=86=92Y exist. In the file http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html,=20 two canonical extensions are shown to exist, a minimal one f\j using =CE=A3, and a maximal f/j one using =CE=A0.=20 In fact they are left and right Kan extensions, in the sense that we have equivalences Nat f (g =E2=88=98 j) =E2=89=83 Nat f=E2=88=96j g and Nat g f/j =E2=89=83 Nat (g =E2=88=98 j) f of natural transformations involving the "presheaves" g : Y =E2=86=92 U and f\j, f/j : X =E2=86=92 U. Although these two extensions are canonical in the above sense, they are no= t unique. Martin ------=_Part_2752_1991421289.1513802799310 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable 
On Tuesday, 19 December 2017 03:36:51 UTC, Gers=
hom B wrote:
On December 18, 2017 at 5:58:22 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3=20
(escar...@gmail.com) wrote:=20
> >=20
> > A type D is called injective if for any embedding j:X=E2=86=92Y, =
every=20
> > function f:X=E2=86=92D extends to a map f':Y=E2=86=92D along =
j.=20
>=20

> Here is a question: given a local operator (Lawvere-Tierny topology)=
=20
> j, an object D is a sheaf if for any j-dense subobject X >-> Y, =
every=20
> function f : X -> D extends to a map f=E2=80=99 : Y -> D. Is the=
re a way in=20
> which we can view injective types as sheafs in some appropriate sense?=
=20


I don't think so, because we don't have the required uniqueness
of the sheaf condition here.

In general, if a type D is injective, many extensions of any
f:X=E2=86=92D along an embedding j:X=E2=86=92Y exist.

In the file
http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html,=20
two canonical extensions are shown to exist, a minimal one f\j
using =CE=A3, and a maximal f/j one using =CE=A0.=20

In fact they are left and right Kan extensions, in the sense that we
have equivalences

 Nat f (g =E2=88=98 j) =E2=89=83 Nat f=E2=88=96j  g

and

 Nat g f/j =E2=89=83 Nat (g =E2=88=98 j) f

of natural transformations involving the "presheaves" g : Y =E2=
=86=92 U and
f\j, f/j : X =E2=86=92 U.

Although these two extensions are canonical in the above sense, they are no=
t unique.

Martin
------=_Part_2752_1991421289.1513802799310-- ------=_Part_2751_1985282777.1513802799310--