From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: **** X-Spam-Status: No, score=4.7 required=5.0 tests=AXB_X_FF_SEZ_S,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,T_SCC_BODY_TEXT_LINE, URIBL_BLACK autolearn=no autolearn_force=no version=3.4.4 Received: from au-smtp-delivery-110.mimecast.com (au-smtp-delivery-110.mimecast.com [103.96.23.110]) by inbox.vuxu.org (Postfix) with ESMTP id 9B744238E6 for ; Wed, 31 Jan 2024 01:47:06 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=mq.edu.au; s=mimecast20180308; t=1706662025; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=cH+Arod+6ThuYE1nHc29PoSh/S9WKFAHFE6MSwj00rU=; b=cIy8d23i7TYNVVFuX0g3mYzrRpE8fL60Q6GxelW9t9BEmGOdz8K95FjxHnlVUWSEf8nc2k B9N+eMWZA3foQemAifFkDNekp2Q9VJ2u91AWFqHl2mDsvf28k0pLUgH3BU5lYXUUKUi+kr RbR8UANl03/dXjAl2wnl2MODspn7uYk= Received: from AUS01-ME3-obe.outbound.protection.outlook.com (mail-me3aus01lp2233.outbound.protection.outlook.com [104.47.71.233]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id au-mta-14-2wR2eg33Pw2eBGfbp72pNw-4; Wed, 31 Jan 2024 11:44:53 +1100 X-MC-Unique: 2wR2eg33Pw2eBGfbp72pNw-4 Received: from SYBPR01MB7018.ausprd01.prod.outlook.com (2603:10c6:10:14d::9) by SY6PR01MB7471.ausprd01.prod.outlook.com (2603:10c6:10:172::9) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7228.34; Wed, 31 Jan 2024 00:44:35 +0000 Received: from SY4PR01MB6899.ausprd01.prod.outlook.com (2603:10c6:10:140::5) by SYBPR01MB7018.ausprd01.prod.outlook.com (2603:10c6:10:14d::9) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7249.23; Wed, 31 Jan 2024 00:44:31 +0000 Received: from SY4PR01MB6899.ausprd01.prod.outlook.com ([fe80::a632:c532:a4b6:7433]) by SY4PR01MB6899.ausprd01.prod.outlook.com ([fe80::a632:c532:a4b6:7433%7]) with mapi id 15.20.7249.023; Wed, 31 Jan 2024 00:44:31 +0000 References: User-agent: mu4e 1.8.14; emacs 28.2 From: Richard Garner To: David Roberts Cc: Thomas Streicher , Jon Sterling , "categories@mq.edu.au" Subject: Re: Fibrewise opposite fibration Date: Wed, 31 Jan 2024 11:35:01 +1100 In-reply-to: Message-ID: X-ClientProxiedBy: SY4P282CA0018.AUSP282.PROD.OUTLOOK.COM (2603:10c6:10:a0::28) To SY4PR01MB6899.ausprd01.prod.outlook.com (2603:10c6:10:140::5) MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: SY4PR01MB6899:EE_|SYBPR01MB7018:EE_|SY6PR01MB7471:EE_ X-MS-Office365-Filtering-Correlation-Id: ccba7e07-db4c-41f6-42f6-08dc21f5c958 X-LD-Processed: 82c514c1-a717-4087-be06-d40d2070ad52,ExtAddr,ExtAddr X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0 X-Microsoft-Antispam-Message-Info: =?us-ascii?Q?XEX3P0AhUbgeDJwGxPZCTuk9pD/0SHp8KXyrIbsgBF8/srQIoz1Csbtv4Kdb?= =?us-ascii?Q?zW+niAUCMox51O8uM+2074oRZIxc5w6LSIu62Lzup2tW4dXSWt68u4mYeoq7?= =?us-ascii?Q?xATpIov2Y6gKaecUJAlXwfTKb7PNCIOJG99aC+NUb/9Omx2DNOqcmOKeJ32k?= =?us-ascii?Q?7lYJCI5DVx3YFWuCsaUTZq3H3gYDuwzICJhBsOZJJMGznYIyatH2mAvioiva?= =?us-ascii?Q?Ic8qP+6/9OQyZkDkaU1K5niqOv4njKmQxTWAbyvVFMJu3+gU1yNdYAp6DBd5?= =?us-ascii?Q?vRTbkTTCjbWbf4egBfCWPLPQdkfJ3X4md3l3cqZU4SiE+hcOkTUOdcPxo84d?= =?us-ascii?Q?LxZBw2aSncepcSuYcarKp+X86Z9bH9YBisxg3fS6fsSK1yNHua/dNe3Hp1s7?= =?us-ascii?Q?6ULmhc0E48tWTdJmS66hLnbjrAUO2ZozHNu04Nj+LaBXqVUOZF3mX/XykuLD?= =?us-ascii?Q?Q1Y/f5pruFhIePElglOcjnJn366MQDaZDXLEnR8A2PRy+hFYjc1Ct6XYLDnl?= =?us-ascii?Q?rEhbgoSQnQMhupNneXjgGvcxXJk9NBlxldU/l3Mf3l8qysnkd4cfKTLGClS8?= =?us-ascii?Q?Ue88d2ipR+RX0nFv0jr8NOf8ijF8DBHCUf0TCWFOo1NsacVzKtmMMI6WvKfj?= =?us-ascii?Q?yepTZ0zzTexHEih9d4+KRsh32+lElqLUEzU+6ab45xx2jyojqD3bglJ+JGxi?= =?us-ascii?Q?zJJbx2GO6aTihlcIAWunxtYwP5CclxSq95OKTYRJNozdlpXCcCKrZAtUO0fA?= =?us-ascii?Q?+9wNGCk4BcGy+aDVqqc4913oViJ8cSA3XO44QO4PhKNkZJe4riI74o0VfyaK?= =?us-ascii?Q?dP0PkhFI78qtKrYR2eYciVNwfSw2R8lZxxSgd27os81hN7KqHnxN//3Ea5/Z?= =?us-ascii?Q?Gfezr6W4sQp/EuKZHOnEvU1BRfgDjupPIaGW7Sx/Unpjs8yyE2UyxhVEL/um?= =?us-ascii?Q?5Ggy6ndY67wMjhrtka2VQlqvgbUckRJXkf99vL867mGNiGLN+/UOEnbZQtkQ?= =?us-ascii?Q?WD1c9DlRWWdnufrFMytR4PMOu52wyYMqYcO9xE2+Gh7AnjDFqKj0Bq1QoE84?= =?us-ascii?Q?vWa/bZh15w1FPepclYhYF0eJhPts2jsdVkQnB+HfdqsgvZzyaL/FdvtdMlOM?= =?us-ascii?Q?ptPIdwgH0cqHvrrbXdbU991fImCRB+uAMm4rLNAAvRiTcfS/9rXlGb8JhYhi?= =?us-ascii?Q?U6A1QHT4dlJ2wlsH514+U2gEi3Kon6BSxgiC63lOO8Y6y6w1ycSzNTwsw1yS?= =?us-ascii?Q?Mu+IgrZTw5gqDWioAhZd6R28uwuFd2M90sNGQbUtKNw/0HH67JhAbE0q5Ric?= =?us-ascii?Q?Gd1Fx5uizkkhd2xkK8oMK7Q2?= X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:9;SRV:;IPV:NLI;SFV:SPM;H:SYBPR01MB7018.ausprd01.prod.outlook.com;PTR:;CAT:OSPM;SFS:(13230031)(39860400002)(136003)(376002)(396003)(346002)(366004)(230273577357003)(230922051799003)(230173577357003)(64100799003)(451199024)(1800799012)(186009)(41300700001)(2906002)(7416002)(5660300002)(36756003)(7336002)(7406005)(7366002)(7276002)(66476007)(6506007)(89122003)(66556008)(54906003)(6486002)(66946007)(83380400001)(6512007)(786003)(86362001)(316002)(2616005)(966005)(26005)(8936002)(88732003)(76576003)(6666004)(478600001)(3480700007)(4326008)(44832011)(8676002)(7116003)(6862004)(38100700002)(41080700001);DIR:OUT;SFP:1501 X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: =?us-ascii?Q?qunFSCp8JGxnYoQCp9J32ODY/7rpo6QUnUojoS7cHOOkBhUJ4LcHEpp+tGFW?= =?us-ascii?Q?keWnAAUdLl6zlRpecnGmKCExBh4UI37fPn1AsAaPkNQyiwzNB3SehH1jBgCT?= =?us-ascii?Q?oAzUPft7xX3hP9S2WNpdMVHuknDTKpbDjgJl1DQmmSjQnGjc3vjEdz4j1LyM?= =?us-ascii?Q?jaw0k9OOuaxXzsIs1Ka5M334dV2U+Yvam9+kODKP+Cv7deA3JuyZ+pH8dqGY?= =?us-ascii?Q?cl/EMpqquo4PU/Y3jmDIb4JpGlqcECqF/A0zX0eD52n08emDAdlsg71LSt3Y?= =?us-ascii?Q?Hc6NOLbXQCBHO7LVQNoTGbedMzObgje+h0SeQ8LRQnjMkqwhoXq1a/9se9b0?= =?us-ascii?Q?9UtpVrE41Y0prIelnQNtW6MIzIdXHcg+VgxkdIHwaXqRxzOzHRDcQ0m2gqms?= =?us-ascii?Q?J72r/HLZehn7hgrA9obA/Bz3XbjMQNLd3i8yO8TiON7II8tJq718cp/ewD2A?= =?us-ascii?Q?QQJ2uk1u/VNskFAju1y+vOoQHhDxsv6RhUAI6EkmagM28SD1GgefSXWq6Y6R?= =?us-ascii?Q?w2M6edeKxrl5FqvOTTBN5y0Y1gd5F2siHSIIDjvISP4jjQNznupjVcP5PXcR?= =?us-ascii?Q?aMKGylv3SbA7c3Sw96/lmAsAEaV2lGUAoYBBKaXKCoXLwAa3CE8BjvRkhYQ/?= =?us-ascii?Q?YYCpnW6waN16aH3Vie6+ObziJQqjVMA9gp0tUWFn6Jjcn+spJ2UxQDjK+klX?= =?us-ascii?Q?fPv3KqiYOVvPzkbjIus27D8185cltZtuOlYCAPIWwyGSDTcJu1iXb7P34mjL?= =?us-ascii?Q?Ck1c+gY2Xdb+NjxwKcklC+T1CUE4dqxX05LbQNQbpDHOrNWXU/za55Yxy1AQ?= =?us-ascii?Q?+ht8MFL4c8zYEoMxbhbV7Iq2MKuMKnJAQItCDXBa3dypFmZknDeoKaun/5ur?= =?us-ascii?Q?GU6noz5qdw2yEdyCkOF6XYqxaUsaiVR1FxudTjbnO9IFvvJzaL7n+SM40JIa?= =?us-ascii?Q?xudXwkWudlGu2j5cJMqRnm0V5Bik9VwqeSPNtamBsIWE+9aenQX+nU0OmiO9?= =?us-ascii?Q?o/VtYFRWKlXyXLNgpdHoSPePYGcz9gn23eYQlc5qVOSHI2D41Bao/cxUFZCC?= =?us-ascii?Q?sbx2yEhe8aelm9Dp2gSdEbKtsZhN6K9bgN4FsGMuf8PI1ylj1w3FL3HhZFn0?= =?us-ascii?Q?2973HNYR6oUWsRkf78kEknLwVuDPR48LQXcjxa8wXxPDPzapeM3irEjcyfBF?= =?us-ascii?Q?tkQlrXOg+ap600vbO+bLk0fAi7VvA0Z/FVarA3l/EEiQxXzlCqTlMMySqucz?= =?us-ascii?Q?RJTn7fJGWYNDYtb6ukXorpwQVaySKiNAlPLa9x0u39UKLJ3LJtGUQS6zVWl1?= =?us-ascii?Q?J8cDd9dD2LAXQ45mX4CUIe+HBIujjBueit/a9CosegbuMTDgOiIogIBfCXb6?= =?us-ascii?Q?PY2qXnJu30v1KzMANon7PVZREQGR+sfAEBfi+E48T2090wwR1J7m3DjdFG/Y?= =?us-ascii?Q?Cldq0NT6yZL7gFaIg56xWmTy0kX/kCJedMtt50YSvCubg0QBJSRXPtAcuT5I?= =?us-ascii?Q?qmgldFbwet28KdxwEl4L0oUwi10vomFFT0BussFSjM5BBUJDfqIgw/Zb370U?= =?us-ascii?Q?o3Shr45ahEQF8cmbipc25ESqNSq9H9mosh4LWCUhPKaJG4MT3v5NtKndszsF?= =?us-ascii?Q?PA=3D=3D?= X-Auto-Response-Suppress: DR, OOF, AutoReply X-MS-Exchange-AntiSpam-ExternalHop-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-ExternalHop-MessageData-0: AJ4SOEVElqsS2GCTwNuNrsTiYhgVv815I9KMU2pNWINKLTvW3Up4QPGQkHK92yCYWJr55kYOiPmYvNet7Tg+yWNSYWKqytEkU6r6Bn/W8MrojhpNEQHrgld+DL3rObrT/gEzTkRHl4oCRyr2mz0C8E9qdY/gcJAr1e92BDOqxC2ayZeNxj4pNfUvxRaaXoET70b9n/pB1rxFxue70Lf+SSOGZuBhQsur6kKCoeaqR4H+nlqXAX+M4cUrNJYXxl2I4Y6YJ2oZYgEhNq4jWr4so3H3KFBH5xDkgkF+SYeDEnYt8XbsDyyH/7UiKZyE4mh2L9y4sMhI5nt+Nqmu/NnMGfJlJr1z7rclANQDf+l3Let5CoJBHNHTLELaCSU2VbzHc1tMcJpLppEWtTYDMvl+nk3uq6b2D9wvj+OiKPmqxCRXVQT0qR0884gZ5h2UIGSw17958WE1I3YosQ8sL7mJRPsDaKlYP6I9WFdoxA57gSRUh2f2lvI+hXggO1eR6GFvWyqyMJTvmy+rOpucdyRe7GKs/KD5+GbQW9sJDJzrrm5U7gav2W1XSMwIYWd0gTdL4WEHdNzQ/lREZKFPj1KHhATHNgVi54qoYeJialXHcB5xVIazdjsPGDVw0CcyahH5fJY35ykw5WYplpMxlc3u3g== X-OriginatorOrg: mq.edu.au X-MS-Exchange-CrossTenant-Network-Message-Id: ccba7e07-db4c-41f6-42f6-08dc21f5c958 X-MS-Exchange-CrossTenant-AuthSource: SY4PR01MB6899.ausprd01.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 31 Jan 2024 00:44:31.2150 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: 82c514c1-a717-4087-be06-d40d2070ad52 X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: yYnbdNOiQ8kGxyu8zzVrQCVXv5q72bo7FUt/9dkRS95mBJ4JyGKr0se6f6kw8OOLBwlKf33InwfjJqmTR/5/6rVTLABXPfLnW2vrLkXwSbI= X-MS-Exchange-Transport-CrossTenantHeadersStamped: SY6PR01MB7471 X-Mimecast-Spam-Score: 0 X-Mimecast-Originator: mq.edu.au Content-Type: text/plain; charset=WINDOWS-1252 Content-Transfer-Encoding: quoted-printable Could you not also work representably? Given a fibration p: E --> B a map in the opposite fibration from e to e' comprises some f: pe --> pe' in B together with a map f*(e') --> e in E over 1_e. If you hom into this from an arbitrary object e'' in E this amounts to giving a family of functions which assign to each map h: e'' -> e' and factorisation p(h) =3D f.k a map e'' -> e over k, naturally in e''. Erik Palmgren did something similar to this in defining LCCCs without chosen pullbacks. Of course for this you have to quantify over objects and morphisms of E which may be more or less palatable. Richard David Roberts writes: > Thanks to those that replied. > > In the setting I'm interested in, a cleaving would be tantamount to > choosing class-many pullbacks, where I am working in Algebraic Set > Theory, with the base category of the fibration the category of > classes, and the fibration one of a number of given subfibrations of > the codomain fibration. In some examples there is a cleaving (for > instance working with the definable classes of ZF(C)). But the whole > point of the project is to avoid global choice, so avoiding it in one > place only to use it to assume a cleaving doesn't sit well with me. > Further, I am not committing to an ambient metatheory (like type > theory or set theory), where I might get some cleavings for free. > > Regarding taking a quotient, I am also considering foundations where > one might not even have something like (or analogous to) Scott's > trick, where you can take a quotient by an equivalence relation on a > proper class. Saying, for instance, that a morphism consists of a > collection of things with conditions assumes one can collect those > things! > > I don't think I need to quantify over fibrations in my intended > application: it's constructing a single fibred anafunctor between two > canonical fibrations attached to a class category. I'm pretty sure I > don't need universes anywhere in what I'm doing. > > I agree with Thomas that this is really a curiosity that it's on the > very short list of things where fibrations do not give a clean > abstract picture. > > I'll have to ponder what is my best option. > > Regards, > David > > David Roberts > Webpage: https://ncatlab.org/nlab/show/David+Roberts > Blog: https://thehighergeometer.wordpress.com > > On Mon, 29 Jan 2024 at 06:34, Thomas Streicher > wrote: >> >> Dear David and Jon, >> >> when constructing the opposite of a fibrations one usually takes quotien= ts. >> But isn't that harmless in topos logic since after all toposes have >> quotient types. >> However, when doing fibered categories one hardly ever studies only a >> finite number of those but has to quantify over them. So when >> proceeding formally one has to adopt some universes be they Grothendieck >> or type-theoretic in nature. >> >> Most constructions are easier on the fibered side. Taking the opposite >> of a fibration is the only example I know which is a bit easier on the >> indexed side. >> But think of facts like closure of fibrations inder composition. That >> is sort of impossible to express on the indexed side. >> >> Of course, for split fibrations things are easier. One obtains fibered >> categories and cartesian functors by freely inverting split cartesian >> functors that are fiberwise ordinary equivalences. The spotted problem >> with the op-construction is thus not unexpected. >> >> Moreover, it is the only thing which is easier on the indexed side. I >> rather find it surprising that most things are easier on the fibered sid= e. >> Technically at least. And for intuitions and motivation it is quite ok >> to work on the indexed side. >> >> It is also ok to choose cleavages when this allows one to express >> things in a more intuitive way. >> >> Thomas >> >> PS Maybe the following metaphor is helpful. In topos theory one >> performs some arguments in the internal logic and others externally >> depending on what appears as more easy. But the external reasoning is >> more powerful. For example one cannot express internally something >> like well pointedness. >> >> For indexed vs fibered I rather have the impression that fibered is >> more flexible. At least emprirically. One usually has no problem to >> reformulate indexed as fibered. The other way is less evident as >> exemplified by closure of fibrations under composition.