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-ot1-x33d.google.com (mail-ot1-x33d.google.com [IPv6:2607:f8b0:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 468f6c3c for ; Fri, 8 Feb 2019 21:06:10 +0000 (UTC) Received: by mail-ot1-x33d.google.com with SMTP id n22sf4268028otq.8 for ; Fri, 08 Feb 2019 13:06:10 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=CM8Icw+GEP6o2c5ckU2cFnG6YrC7FuY83nF8/XdkozA=; b=tEUaP/QFhT4mW16IEovxsHlADwii2b/ZsszYjQPvEL8z0pdHcbLL/Ix+wwUd72iOEW gwecxBMQW8nMTDz4mmE9KqWeqQjJTvoFKwQURke0YHWs4EMYNIwbaXaIctsQoaq1ZzWK NQ6EzJkZfhnRPwcxaFQypfYGd5jNOMbkthcIf7gTYk//yLqCIPsEDadi5IwSk0Bbi0UQ X9p6Mf914mHrKxYrtNpln2lzNV+ZyGpnEr/778Ei87FcPigJzPzsJ2uDW5IWWCpoIoA8 oX42zzN+iWE9dHTl0qV7Uoeq45ITb4PkJA45W2Te1dFkPfFcLqUFTHj5uXymU0zgBlyn /ulA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=CM8Icw+GEP6o2c5ckU2cFnG6YrC7FuY83nF8/XdkozA=; b=AYYozQ7lXwGsIKUGtpO+v4/qhR3ReWGV3VjQG8k7Zgn06GMj5IYopSATDu/ud3xhka 0rnZfLmINNN8gCQFJdKYd4lwNqzadJBb5abiD6dI6JRx8PLhJ5yAOukfYBgreu+/e6+G LV51QlkGFgP9PVHcKICEd9jwr6/191/nJV4QBhkg59MX+vLmg3GVtga/aM8+Pw8iNFhC MMh1f9YhjjhTU4Mz7H7kLXNVbDQVfm9TO3GbTcDaeMif5Ig5dgljQfbhKKbroa6HUCGj N220ZcRjUhGiUEbwzy6tDBwuCZWYUneCdvlXhq7PK3Zw0QJW1FpYW09pFlVvwKwhIoEj Wuug== 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: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=CM8Icw+GEP6o2c5ckU2cFnG6YrC7FuY83nF8/XdkozA=; b=g6WVQuB47hYLmBcTbgLM0wa0zcGn+1Bhf/9fbLiQaLNtM9VsjW5mbMN3oGAplY+Qbk s7RJErMGK75Wq8+SWkZyTuy5Gep7PNjqr2kCqXHKp/z2HpprWXq/3H/9UKk9ZZVdvCe0 tDIIgROiuIy2m6b+KYYv9EEdBXAYrmUIwpyEhOsL7VwAwU55opaH5NsN1TqZ9xB0Pb50 vOZxPjipL2ARZsnI574nZMYOCT9rzhXlMuh/IRn3uKvYi24cv7qIDfCfeMakkn5EFBvA 78F/KQcTcuA7Jy5z9UgpaUZ4ftNa3j8pZXHZGVHBKWHHaXzxxjDdoJmVSqB0RJvJWkO3 UkpQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub2vNUZ+Qaa0AZH/lnRR+Vep+49doXUD/qdaZdHTBJIh87EQttd AqLdhCLgXkkiGT8F2pkVUaM= X-Google-Smtp-Source: AHgI3Ia5fm+zgwJsmMsb0ZutcuaLqSjQEVoWfaEmNq1//R9GVLRieIF3+XNsTwHwCYGlvnnM8AliFg== X-Received: by 2002:a9d:da3:: with SMTP id 32mr307482ots.3.1549659968816; Fri, 08 Feb 2019 13:06:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:75d0:: with SMTP id c16ls4283661otl.3.gmail; Fri, 08 Feb 2019 13:06:08 -0800 (PST) X-Received: by 2002:a9d:19a4:: with SMTP id k33mr135045otk.5.1549659968182; Fri, 08 Feb 2019 13:06:08 -0800 (PST) Date: Fri, 8 Feb 2019 13:06:07 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <0cfb9acf-e5f9-4ee7-979e-f7d66b82a178@googlegroups.com> Subject: [HoTT] Question regarding terminology regarding injectivity of objects MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_539_463575738.1549659967680" 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_539_463575738.1549659967680 Content-Type: multipart/alternative; boundary="----=_Part_540_1831736429.1549659967681" ------=_Part_540_1831736429.1549659967681 Content-Type: text/plain; charset="UTF-8" Question regarding terminology regarding injectivity of objects: (1) An object D is called injective over an arrow j:X->Y if the "restriction map" hom(Y,D) -> hom(X,D) g |-> g o j is a surjection. This is fairly standard terminology (where does it come from, by the way). (2) I am working with the situation where the restriction map is a **split** surjection. I thought of the terminology "D is split injective over j", but perhaps this is awkward. Is there a standard terminology for this notion. Or, failing that, a terminology that at least one person has already used in the literature or in the folklore. Or, failing that too, a good suggestion by any of you? (Before anybody says that there is no difference assuming choice, I remark that I am interested in the "infty-category of types (in a universe)" in HoTT/UF, where the homs are infty-groupoids and so the section has to be a morphism, not just a theoretical function.) Thanks, 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_540_1831736429.1549659967681 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Question regarding terminology regarding injectivity = of objects:

(1) An object D is called injective ove= r an arrow j:X->Y if the=20 "restriction map"

=C2=A0=C2=A0=C2=A0 hom(Y,D) -> hom(X,D)
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 g=C2=A0=C2=A0 |-> g o j

is a surjection. This is fairly standard terminology (where does it com= e=20 from, by the way).

(2) I am working with the situation where the restriction map is a=20 *split* surjection.

I thought of the terminology "D is split injective over j", b= ut perhaps=20 this is awkward. Is there a standard terminology for this notion. Or,=20 failing that, a terminology that at least one person has already used in=20 the literature or in the folklore. Or, failing that too, a good=20 suggestion by any of you?

(Before anybody says that there is no difference assuming choice, I rem= ark that I am interested in the "infty-category of types (in a univers= e)" in HoTT/UF, where the homs are infty-groupoids and so the section = has to be a morphism, not just a theoretical function.)

Thanks,
Martin

--
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_540_1831736429.1549659967681-- ------=_Part_539_463575738.1549659967680--