From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.41.205 with SMTP id p196mr890263vkp.71.1513654611160; Mon, 18 Dec 2017 19:36:51 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.176.73.235 with SMTP id f40ls5344477uad.0.gmail; Mon, 18 Dec 2017 19:36:50 -0800 (PST) X-Received: by 10.176.85.209 with SMTP id w17mr978569uaa.21.1513654610155; Mon, 18 Dec 2017 19:36:50 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513654610; cv=none; d=google.com; s=arc-20160816; b=UPsSMbUzmzu3np+argfys0kLkG0cyZyDt9+Pb3WxHLSGiZaWUZ3CKyyn9iGcSgXjLn UY2+oS/hs+1F5qSWBVo4XfzkOXrjgNUB4cEHnnygQ6TM4ti8xlAIbBS+HPvhJ1EwvEkM xbHsFqyF60IhkMZSYolt+DVw2I5R8M2Qyan0EOte8JaI551iCdUp6IxUs9rTjncqBX3n 89dMV+oF2MNv1KaqxW1gZQrswDnUnJSOHD/DAmmpPy14p42FohDH+7bA7vx/Tl0pDv6Z bmGcjRWJtCxBMClVWhxWX2u411/FDrCFLBVazt+WVcYdz9VEv3YudOQquSJRvnMZK9Zb MkcQ== 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=h+JGs21uLrp4WHk9HiXeP2KGojGBS42IiUj/KIem/Kg=; b=kaJ/I5LvH2Lr/dZehes/+JHPmYEKxxqxLaqZiiVfcpR7azbfBJ4axfVdohHN4J4vnV rs+UGst5VAvhF6kyHn7Mi6jRqJNe/FVPBY3bgn5ng0RfZpwmxGjk5lEp+2rvUXwN/Dze x7IF0QthyYkHJX6e5R6urpal+JqTvdgU2Ypi+LuShQ3Zjgrj8+J1Bp6t29v+9aizC1j4 INbH2ZydS48MvJb5G/b7CErU/kWaafepzwG3HprtjKcDTinZHaeZuQjx3dYwmkNQ6OQz miQ9QdT7zdPcQ7x8f001eFyDDxb76NOk2v9kh7Vg7hh0GczbSfJolhSxwgDQIUEPxsHK x5Ng== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=eM7dRgKY; spf=pass (google.com: domain of gers...@gmail.com designates 2607:f8b0:400c:c05::234 as permitted sender) smtp.mailfrom=gers...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x234.google.com (mail-vk0-x234.google.com. [2607:f8b0:400c:c05::234]) by gmr-mx.google.com with ESMTPS id 68si825384uaj.0.2017.12.18.19.36.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Dec 2017 19:36:50 -0800 (PST) Received-SPF: pass (google.com: domain of gers...@gmail.com designates 2607:f8b0:400c:c05::234 as permitted sender) client-ip=2607:f8b0:400c:c05::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=eM7dRgKY; spf=pass (google.com: domain of gers...@gmail.com designates 2607:f8b0:400c:c05::234 as permitted sender) smtp.mailfrom=gers...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x234.google.com with SMTP id s197so10712434vke.11 for ; Mon, 18 Dec 2017 19:36:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=h+JGs21uLrp4WHk9HiXeP2KGojGBS42IiUj/KIem/Kg=; b=eM7dRgKYO39giWH5pxFYuxIlCipPcFw4J9J5kJsK1H08aUHfsxfJWA5v4BwgolCjII AfSx1rMFNKlDND4rhjaUk61/yk8HHJE/3XuUCEpA+HM+ycRdnlxU5PX5QzNSyvSMW4aq pLKCm8+8JVQiaxH3QDMfPKJslkYHrGg0dsm8zn0/9pflN9K7HnEbHZBygip1CHYjYZMn UGQXI3ItYVF5cs0XaZG34MDA916iguPQiBEaiv4n9jVbF3KzCRij3XmGfCQqGnKdQC5F 5e5jRYiswEm6woWdxTpul4ZWCeb+5HEtKOpNaAZ1046S1niM/gOnSMOSiabM80kRiF7F U1YA== X-Gm-Message-State: AKGB3mIyQ9F2LYG49Ng0YoKepExScdDpRdS/gr8S7JtcptwlAE7U2aF7 0W/CbPt9tTMWJHHdcDgFKO+CqHN0pzQE+yrd6+Q= X-Received: by 10.31.133.206 with SMTP id h197mr1696774vkd.99.1513654609655; Mon, 18 Dec 2017 19:36:49 -0800 (PST) MIME-Version: 1.0 Received: by 10.159.41.227 with HTTP; Mon, 18 Dec 2017 19:36:29 -0800 (PST) In-Reply-To: <0c1d71ec-3e8c-4cbf-9407-534a2b1f39de@googlegroups.com> 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> From: Gershom B Date: Mon, 18 Dec 2017 22:36:29 -0500 Message-ID: Subject: Re: [HoTT] Yet another characterization of univalence To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On December 18, 2017 at 5:58:22 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 (escardo...@gmail.com) wrote: > > > 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. > Here is a question: given a local operator (Lawvere-Tierny topology) j, an object D is a sheaf if for any j-dense subobject X >-> Y, every function f : X -> D extends to a map f=E2=80=99 : Y -> D. Is there a way in which we can view injective types as sheafs in some appropriate sense? Regards, Gershom On Mon, Dec 18, 2017 at 5:58 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > 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 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: > > 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 > 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 : >> 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), th= is >> 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 novelty is a new notation for universes in Agda closer to >> the notation in the HoTT book for informal mathematics in type theory. T= his >> could be further improved by making it built-in in Agda (as explained in= the >> imported NonStandardUniverseNotation.lagda), but probably it is good eno= ugh >> without any modification to Agda. >> >> Martin >> >> > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.