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-qk1-x739.google.com (mail-qk1-x739.google.com [IPv6:2607:f8b0:4864:20::739]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 23e199d9 for ; Thu, 8 Nov 2018 12:23:56 +0000 (UTC) Received: by mail-qk1-x739.google.com with SMTP id h68sf37602081qke.3 for ; Thu, 08 Nov 2018 04:23:56 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541679835; cv=pass; d=google.com; s=arc-20160816; b=FoYYHkJfkpoEf5plGnmMMbzqfVMVX0JTQuWCfxoU63+dB+iNcrAOR8Bxv77Dt0UVFJ xMbD8B3ZGtjESZVZp/yeEw5Un8cOm/w2na6SvJ3Oj7mzLs3uErOZR6LQot9tE506Uvus Eyocr2v4ey52jnGRwZu8RYFnuA3fCb+UFs0m6kMzg0UvEmJDs8ZfQmH8WYg7JF1g7IN9 6Z+wTKgoHH8C99ngb4SDHkC45FppK1oDUaJ2shztMrGOR1j9ATMJ+ba4mh8ULU3u7e4A 5mk5gOHUQnYApRIp2Wwc0LPQ6qXCshEDwr1lztwIctDHU1PtyBGooX6OqPvX6AMqED3+ vVEA== 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=c0KN2AdqN/xqc7gjJ/ETpQoz+uLJvJUvZtXLSsirhBU=; b=USpo1h85emkgpx/3sYwPFGSDbd0UP4GzunJZIgukIlXdqnXDeQleUnBlf5ZmFOEJ2I vuPWuoZQnxJWPBAnqlod7waUSDK7cRQBvWRC2GVZYLw0wn6au2y08YAFCwrl0aiyBhPP kpdmraPmZN7/X1ofqa8/acQH4aikAmEGFsqgwFC/W/ciK3xBi/mSEbtVU1xKeermoGKy LBK0NLwe3vvtpEjhyPvgVOAW3OKX+S+0VtNNs3G5LSAfhpRaimQRdaOJMA5G9GBt9bdy Z2gTH4ZS23aZsx6KKY/todeBIy+6KB0dHBqeZXU1UbwvKByv3KB30PkyS6fWzZGNt9d9 CpBg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=neutral (google.com: 128.220.39.159 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=c0KN2AdqN/xqc7gjJ/ETpQoz+uLJvJUvZtXLSsirhBU=; b=FQdkr3ZqsJQPVayFezIjTn03xfSzpbLB/OIWY35K7UhYvIxsvVMGi82sJ2USasrFCU fMIBcgkTjQJ2dUAPiYUEl2yAjpuckmzwDHOk2Y1JQnvwO0aed8AfImjXHICqftG9wUhY PaRfJScUfgndwopShhi7IPlkrCOIgNofHmjN4uc2GIxUxjETqi8bfbReMOEeOmKiPjNY oQT+xp5yAWKl64avt2DAdlALFyFnZwJ78tHnV982obBtijcz3himHWVO5wcMixfQfLkQ nASWELtpQJlvlvPSXjQWAUw3Xz3Rj4pKbtECsmmeIN04d1GZQzi2jxdZfQ5v/Rbl+qp1 2NdQ== 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=c0KN2AdqN/xqc7gjJ/ETpQoz+uLJvJUvZtXLSsirhBU=; b=FxwNrMikK3g4UWMRqjilyOgW7rYECSXAkI3psYxchXXaEUFB5jvY10oA+Zpu2dr3oJ P7O3tJDwP4oFZg0Eqgu32WN/s0R1+QCozq6hy7ciEQaAcvTfPMt+vmKjCbK9s1LrAHLi PvDm8Lyaf6hVWj9en+zEKVMFbgdGFxVeeNkpzRh2eggrOlLo8gwI90GrmBITL+xBbhtU n6xXaKH1pTHEvQ2t2KyM/8wApcbSl7sVGFWL+DFEKHkCcEGTSdjpcVxyM5kWwwA/UYyp S3klsXwQ/48ksmvMjLnYVe/ynVpiCXLt7rlpKj9tqXp02SV/pXoJmnOD31DaJO+UuA/s ud7g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJsSoMbntXggeYMMBcFSe/y1S7YqkC7a21jnBdMumsSD9Cl86bl egF2gdIQ5rqfayW9rVPOjrE= X-Google-Smtp-Source: AJdET5epihzWqeEIqpEsrj1X6LyHFCDEdrCBLOX7RWFSx29Hb0t0FgNheTpNy/xpkr3qsCOfIUkepw== X-Received: by 2002:a37:2b04:: with SMTP id r4mr48138qkh.7.1541679835690; Thu, 08 Nov 2018 04:23:55 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:4902:: with SMTP id w2-v6ls669420qka.3.gmail; Thu, 08 Nov 2018 04:23:55 -0800 (PST) X-Received: by 2002:a37:110d:: with SMTP id b13mr2672262qkh.15.1541679835376; Thu, 08 Nov 2018 04:23:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541679835; cv=none; d=google.com; s=arc-20160816; b=d3IKU/WEr63uSh0CLJk7iCZ+sYM8a2DWIdui+KF9szeaOisgoGmHrf2fgCtvt1r4gl 05h+kuSqfoNPHfoX4PveZekiz0CTwd54eG8LP+PWh5+lmoL0Wt75paN9MHLLjO1lUdkV y4y/4qrD3e2C0P4inXYSt5hQgKY8FYOH80etgHOhsW7dzcyenuW8J95ae5G2zHTabBXm 7nrHF0xMPXVXR2zI+xWUVnr870EKwiE5qsQq1z98ZFoCV+TJLIjEk881/V73ZVJZHn13 sohApzE65E1PBqJK0jALU4dreWTN5TaTzOlHOc5vs7mb0lVA7mw+i+5VYNrnFU2GhA/4 7WAg== 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=13ttj2t7ilcCNypjdWXssqcC24cRtqlfk/Rv6iE4Trc=; b=iLcTyZFpz1Gg9s8RHvsO/l1JIskR5lZV9a1KF3ghdVld0RPrkA+5gZFxI5o1LrLUjc FibSDYK0R/NNwsbeAaARi6/HXsep9eyiXm7ezi74EKudQNWS9b/2mBU05MLKeP2LkiyP b7rkVBk7mMgNtsq8PqHdaCfRrPFQtYWlAcao5QAS/XKLvoksD1L+/gvbZAmdLPX/uCma Wbkhz4MoBh0mA3laaU9Mfq3w7G6L9pTQnEGaLeT07vZ1jFQjBY2ZrjnlXSqFpULo2dJm lR+gKoiAO6Th++lVEREYNVJSoHSGKIJUG5KW8+OXFjOqiYsur8HZew/IWDs8OiYeXu4k ZqzA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 128.220.39.159 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.159]) by gmr-mx.google.com with ESMTPS id q124-v6si186651qkb.0.2018.11.08.04.23.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Nov 2018 04:23:55 -0800 (PST) Received-SPF: neutral (google.com: 128.220.39.159 is neither permitted nor denied by best guess record for domain of prvs=84379032e=eriehl@math.jhu.edu) client-ip=128.220.39.159; X-Amp-Result: SKIPPED(no attachment in message) X-Amp-File-Uploaded: False Received: from c-73-128-252-11.hsd1.md.comcast.net (HELO [192.168.1.2]) ([73.128.252.11]) by IronMTW5.johnshopkins.edu with ESMTP/TLS/DHE-RSA-AES256-SHA; 08 Nov 2018 07:23:55 -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: <20181108115815.GA5022@mathematik.tu-darmstadt.de> Date: Thu, 8 Nov 2018 07:23:54 -0500 Content-Transfer-Encoding: quoted-printable Message-Id: <18A8A179-4ECC-4C70-816B-0F700F47CF0E@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> 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.159 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: , There=E2=80=99s a (2-categorical) characterization of fibrations due to Ros= s Street that I like that works well in the (=E2=88=9E,1)-categorical conte= xt. In quasi-categories this captures the class of maps that Joyal/Lurie ca= ll =E2=80=9Ccartesian fibrations=E2=80=9D but this definition can be used f= or other models of (=E2=88=9E,1)-categories as well. A functor p : E =E2=80=94> B between (=E2=88=9E,1)-categories is a cartesia= n 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 A functor p : E =E2=80=94> B between (=E2=88=9E,1)-categories is a discrete= cartesian fibration (aka right fibration) if the corresponding functor p^2= : E^2 =E2=80=94> B/p is an equivalence. Here E^2 is the (=E2=88=9E,1)-category of arrows in E (the cotensor with th= e walking arrow category 2) while B/p is a pullback of B^2 along p : E =E2= =80=94> B in the codomain variable. If p : E =E2=80=94> B is an isofibration (in models, this is the notion of = fibration in the corresponding model category; eg the Joyal model structure= for quasi-categories) then p^2 : E^2 =E2=80=94> B/p is also an isofibratio= n and you can modify the right adjoint right inverse so that the right adjo= int is a strict section and the counit is an identity. This can be technica= lly convenient =E2=80=94 the adjunction is now a fibered adjunction and can= be pulled back more easily =E2=80=94 but strict equality doesn=E2=80=99t f= eel necessary to me in this context. Best, Emily =E2=80=94 Assistant Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl > 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 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.