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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pl1-x63f.google.com (mail-pl1-x63f.google.com [IPv6:2607:f8b0:4864:20::63f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b0f16256 for ; Thu, 8 Nov 2018 12:28:20 +0000 (UTC) Received: by mail-pl1-x63f.google.com with SMTP id w10-v6sf17318795plz.0 for ; Thu, 08 Nov 2018 04:28:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541680098; cv=pass; d=google.com; s=arc-20160816; b=i2IB07NH6wLA9hdeTan0GPcCVo9KxpDnjX7A7o0Ldp3warx+9Fxv6hBsncOKCb3sch O+1qx/808mlrsomtZJBSLWj56PXn7VdHon8v4205pl53r0kLVgeGF/zbTD5rBgI+EFfY FaDCUViv6Jc4BGZzjYLulacb+szkNvyTFNVF3sv/bA/9Iqy57ZCX7W5sUbiaaF6BRs4P FH1Q9URkmwcw2Jn5w/sGROQQGpPohKeWzc2M9iyMsi4CZH1uRJqWKlz4azDeMNGvq1j5 O1eh9ECGsPa5NbnLAcv5lOelOPc+obcc14S/mgzTJAYwZMkQI2RHemqFIjCCyUQkyTd/ 7A0g== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:references:message-id :content-transfer-encoding:date:in-reply-to:from:subject :mime-version:sender:dkim-signature; bh=mXuWv3B2hKVh+niEiW3ULbXphV2I1uM35VknWUPtsL0=; b=hcXMmp/oIkApn3ncmOup/2Hvn5l3yaWso35ht338Lz4VghQgbWAGLUqNsU3jj3yxxK 5jJlmC3VQxFgT0pqUXVMq5ZEXyaktQdJQCxNMzdD8Fk6nFiWaQmx6xf3F9t+OHcq2FwT Oxzcydip64saHLpR2GccSxuwo3w1BXMyFhx5bfaFu52Fbrn8Esjxdda1F4fal/ZoSfd6 JNQ/twiuw79LaFgWN7X16MTK+zzrExHiM93qodDkel4PW9JPv1oTpHLmZTizg1kXIhB4 CbOdbsWlm/FJiH6K22LATh6V6oyMV3VIkxbInZLQyNLcVAr/L76Kl2qSIjkY49SXKmIx efWA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=neutral (google.com: 128.220.39.189 is neither permitted nor denied by best guess record for domain of prvs=84379032e=eriehl@math.jhu.edu) smtp.mailfrom="prvs=84379032e=eriehl@math.jhu.edu"; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=math.jhu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:subject:from:in-reply-to:date :content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=mXuWv3B2hKVh+niEiW3ULbXphV2I1uM35VknWUPtsL0=; b=HqShP/ZMpESwFYJe78vigfN88XOwLTyflLHKkj0dS0GJnuTXZgL0PJdpCU2zNToAUN bq0aIJMm3wQZEIKDLoDz+pXcK91jylnj74pUGNI3YVnFP0VzQ9WZnamXuGDE6QTAN/uS sbOOvEKyUTDfQcEWoOP0u6f3Ek7rOKlTmLywUiQvPXEUBn9AGBjYKd9Yy6oWbobDt2wU Ak/YjM40uCXj01YE0YKl3jAA8NdzJ8h65LG5bt6NRrvPgkll5W9+F5IOyq9Q+OyVK/sU KZFz21QUWr7V19xuK4sXyyZEi1AabzD/TS0o4TpGY/ynE2QfDcRUHsz/E3PAJIIOzNei VenQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:subject:from:in-reply-to :date:content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=mXuWv3B2hKVh+niEiW3ULbXphV2I1uM35VknWUPtsL0=; b=JSSd0/eIlnK4gXDlxmaVsYnMjZlYi2oMnJTTUGaA79EoLhVBuN3CN6bUph+8xb6AVE MFoEQ8dyBmQfWPafqnj0JnOvnc6F5pYB/HwHGCMKD/JCseggXMtyVG99f7ZnKc6TmunV qmSPbcnnN2mrrOxBpNTzbqY0vzeLK81G+oF1fuXbjb7Xq2bNCBmLFu7nnMTH5Euh+vFS yZRuXi70YMeUzUN2eSv7H6RzxdLZqVyizfB3djvTKW8w5WcIDsQvtnFKp4kCy2AXuuSt 1N8eJdQhTHj0eviWWyedZmIjRv7m4LtxIPBj2mnfFMomxPogVgYX4Zz1v21L6iFh00uo SgQg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJ2lwCvaXH+WF5g6CKJm5nAHcP5KBrJGS8VCDjKPfhligAIjzXQ FL9vHXT6AhSdH+yuj+gaMfc= X-Google-Smtp-Source: AJdET5cX220h/X7b+MjmmJmADFJLr5/QAtobik8GFxGfK/Z4Zx0Kr0yPHA5acBA/xWT1JZa9VVvK+w== X-Received: by 2002:a17:902:904b:: with SMTP id w11-v6mr21399plz.5.1541680098707; Thu, 08 Nov 2018 04:28:18 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:115c:: with SMTP id z89-v6ls833851pfi.2.gmail; Thu, 08 Nov 2018 04:28:18 -0800 (PST) X-Received: by 2002:a63:e944:: with SMTP id q4-v6mr365138pgj.107.1541680098292; Thu, 08 Nov 2018 04:28:18 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541680098; cv=none; d=google.com; s=arc-20160816; b=y8SnrY6udkS9sM3QDWJljGwl9/F2C+dWre2C+V2HKET388eE0OwvKMN4cHlBYn8R3o dwJtcb9AGArGcI6g2NACHLEqc8oi7EhQxGrL6MIweOgsP17K0B8MyTy/71hdYAePiBUn oG+QMaFINgHraF+hYAP8Vxv/eoqY7wMb9tgsKQaeIsY1tSZpMRHh0mGJIhj54ireWdOR yZ/UIQhcQ67mIAHn83eguC8ovlz0AanaarwXLhjto1gICzJCc9jTky7XOr6CddYLRTww FqxozCQ6cc8RbmfzB25RWG7oj6NIWEU2lHx4xOtUgwu+tmOow7py/RHMQJ3ZxX2dTPY1 mnHQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:date:in-reply-to :from:subject:mime-version; bh=tKmeBqmqV22wa47FrOh8pUe9JIhTVQv17p6y7p4Q5cU=; b=OqpKTH4SC3LDyrDiCsl8Te7Dij02dLfuvpnC57GOtGs+rCqp0vJNAakjbbBhSWu9rR mqUyKuFnTX+Z0Aw2fPN8LhNtydI7tOYc+6vqmjIVDv5x97426efMfO+cQEyPlD7Eu4oh BokZfIcR9BhXh02QYKgZx6fvPwvj4eTn97KiuLfmsQcKI7eURYu1C0WZ7dOXs2tscd46 XNOur4wICT5CVz9VAQxQgPFl0ZjqwXVRLeVqyNGAcLIzHx5rw0zaldUwpdzoLC22IP+w aUvlJGLGCMuzPq/wUR0+afEH4gujWMK1rbmgvjXNto0QbqPGoEHBkrD7NNs1BPz9hmvc 7t6w== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 128.220.39.189 is neither permitted nor denied by best guess record for domain of prvs=84379032e=eriehl@math.jhu.edu) smtp.mailfrom="prvs=84379032e=eriehl@math.jhu.edu"; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=math.jhu.edu Received: from smtpauth.johnshopkins.edu (smtpauth.johnshopkins.edu. [128.220.39.189]) by gmr-mx.google.com with ESMTPS id o12-v6si169789pfk.4.2018.11.08.04.28.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Nov 2018 04:28:18 -0800 (PST) Received-SPF: neutral (google.com: 128.220.39.189 is neither permitted nor denied by best guess record for domain of prvs=84379032e=eriehl@math.jhu.edu) client-ip=128.220.39.189; X-Amp-Result: SKIPPED(no attachment in message) X-Amp-File-Uploaded: False Received: from c-73-128-252-11.hsd1.va.comcast.net (HELO [192.168.1.2]) ([73.128.252.11]) by IronMTW8.johnshopkins.edu with ESMTP/TLS/DHE-RSA-AES256-SHA; 08 Nov 2018 07:28:16 -0500 Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Subject: Re: [HoTT] Precategories, Categories and Univalent categories From: Emily Riehl In-Reply-To: <18A8A179-4ECC-4C70-816B-0F700F47CF0E@math.jhu.edu> Date: Thu, 8 Nov 2018 07:28:16 -0500 Content-Transfer-Encoding: quoted-printable Message-Id: <3EDFBA7A-AF24-45D3-9CAD-7829239F458B@math.jhu.edu> References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> <4ae4c745-a00e-4ebd-9de2-e29474b75d48@googlegroups.com> <20181107153556.GC26970@mathematik.tu-darmstadt.de> <20181108115815.GA5022@mathematik.tu-darmstadt.de> <18A8A179-4ECC-4C70-816B-0F700F47CF0E@math.jhu.edu> To: Homotopy Type Theory X-Mailer: Apple Mail (2.3124) X-Original-Sender: eriehl@math.jhu.edu X-Original-Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 128.220.39.189 is neither permitted nor denied by best guess record for domain of prvs=84379032e=eriehl@math.jhu.edu) smtp.mailfrom="prvs=84379032e=eriehl@math.jhu.edu"; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=math.jhu.edu 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: , I should have added references. Street=E2=80=99s original papers are here: =E2=80=9CFibrations and Yoneda=E2=80=99s lemma in a 2-category" https://link.springer.com/chapter/10.1007%2FBFb0063102 =E2=80=9CFibrations in bicategories" http://www.numdam.org/article/CTGDC_1980__21_2_111_0.pdf For a rough draft of the (=E2=88=9E,1)-categorical story, see Chapter 5 of = this: http://www.math.jhu.edu/~eriehl/elements.pdf Best, Emily =E2=80=94 Assistant Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl > On Nov 8, 2018, at 7:23 AM, Emily Riehl wrote: >=20 >=20 > There=E2=80=99s a (2-categorical) characterization of fibrations due to R= oss Street that I like that works well in the (=E2=88=9E,1)-categorical con= text. In quasi-categories this captures the class of maps that Joyal/Lurie = call =E2=80=9Ccartesian fibrations=E2=80=9D but this definition can be used= for other models of (=E2=88=9E,1)-categories as well. >=20 > A functor p : E =E2=80=94> B between (=E2=88=9E,1)-categories is a cartes= ian fibration if the corresponding functor p^2 : E^2 =E2=80=94> B/p admits = a right adjoint right inverse (right adjoint whose counit is invertible).= =20 >=20 > A functor p : E =E2=80=94> B between (=E2=88=9E,1)-categories is a discre= te cartesian fibration (aka right fibration) if the corresponding functor p= ^2 : E^2 =E2=80=94> B/p is an equivalence. >=20 > Here E^2 is the (=E2=88=9E,1)-category of arrows in E (the cotensor with = the walking arrow category 2) while B/p is a pullback of B^2 along p : E = =E2=80=94> B in the codomain variable. >=20 > If p : E =E2=80=94> B is an isofibration (in models, this is the notion o= f fibration in the corresponding model category; eg the Joyal model structu= re for quasi-categories) then p^2 : E^2 =E2=80=94> B/p is also an isofibrat= ion and you can modify the right adjoint right inverse so that the right ad= joint is a strict section and the counit is an identity. This can be techni= cally convenient =E2=80=94 the adjunction is now a fibered adjunction and c= an be pulled back more easily =E2=80=94 but strict equality doesn=E2=80=99t= feel necessary to me in this context. >=20 > Best, > Emily >=20 > =E2=80=94 > Assistant Professor, Dept. of Mathematics > Johns Hopkins University > www.math.jhu.edu/~eriehl >=20 >> On Nov 8, 2018, at 6:58 AM, Thomas Streicher wrote: >>=20 >>=20 >> Thorsten asked why I prefer to have strict equality on categories. >> The answer is that one needs it in category theory typically when >> speaking about Grothendieck fibrations. >> And the latter is most useful in many contexts in particular when >> understanding geometric morphisms. This by the way also extends to >> Grothendieck fibrations in quasicategories as in Joyal and Lurie's >> accounts. >>=20 >> Thomas >>=20 >>=20 >> --=20 >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> 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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. --=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.