Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: topos theory

Topic: sieves and slices

Christian Williams (Apr 09 2020 at 02:54):

I've been thinking about an odd twist on the notion of slice category. Let $C$ be a category, and define $\mathscr{S}(C,c)$
objects: $(P \rightarrowtail C(-,c), a\in C)$ -- a sieve on $c$ and an object (thought of as $P(a)\subset C(a,c)$)
homsets: $[(P,a)\to (Q,b)] = \{u:b\to a \; | \; \forall f\in P(a). \; f(u)\in Q(b) \}$
with ordinary composition and identity.

Christian Williams (Apr 09 2020 at 03:00):

I'm thinking of sieves as types, in order to get something like a "category of types and terms" in the "kind context" $c$.

Christian Williams (Apr 09 2020 at 03:02):

There are some decisions in this construction that are flexible. Right now I'm searching for good reasons for the decisions, and how to describe this construction as canonical.

Christian Williams (Apr 09 2020 at 03:02):

I know that it involves the Yoneda embedding of $C$, composed with the subobject functor -- and somehow combining this process with the Grothendieck construction.

Christian Williams (Apr 09 2020 at 03:04):

If anyone has ideas, let me know. I'll post on here when there's progress.

Christian Williams (Apr 09 2020 at 03:05):

On the type theory side, the construction is unusual. In the semantics of polymorphic type theories, one has an indexed category $F:C\to \mathrm{Cat}$ where $F(c)$ is the category of types and terms in the kind context $c$.

Christian Williams (Apr 09 2020 at 03:07):

But a morphism in this category of types and terms is a judgement of the form $c \; | \; x:P \vdash o(x):Q$ for some constructor $o$.

Christian Williams (Apr 09 2020 at 03:08):

So one thing that's odd about the construction above, besides the contravariance, is that morphisms are inputs rather than operations.

sarahzrf (Apr 09 2020 at 04:07):

im not following your explanation of the type theoretic content

Christian Williams (Apr 09 2020 at 05:20):

which part, mine or the standard semantics?

Christian Williams (Apr 09 2020 at 05:34):

Chapter 8 of Jacobs' Categorical Logic
https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/141
8.1 talks about the syntax of polymorphic type theories
8.4 talks about the semantics.
There may be better references; this is just the one I'm working with right now.

Matteo Capucci (he/him) (Apr 09 2020 at 08:21):

A way to construct that could be this: consider the functor from a site $\bf{C}\to \bf{Cat}$ sending an object to the category of sieves on that object (it occurs now to me this should be just $\rm{Sub} \circ y$, where $y$ is good ol' Yoneda embedding). Then let Grothendieck do its thing, and you get a category where

• objects are pairs (sieves on $A$, a sieve on $A$)
• morphisms are images of morphisms of sieves preserving the given sieve, which should be what you proposed as homset

Now this category should be the same as yours if you realize having an object of $\bf{C}$ and having the set of sieves on a given object is the same thing: just take the maximal sieve to recover your object.

Matteo Capucci (he/him) (Apr 09 2020 at 08:22):

Oh, now I see you specifically mentioned $\rm{Sub} \circ y$ + Grothendieck

Morgan Rogers (he/him) (Apr 09 2020 at 09:11):

I worked on exactly this with @Riccardo Zanfa last year. I have no input on the type theory stuff, but this construction leads to some very neat stuff, but which we never got around to publishing because there were several fiddly loose ends we couldn't figure out.

Morgan Rogers (he/him) (Apr 09 2020 at 09:13):

I'll ask for his permission, then share what we found!

Morgan Rogers (he/him) (Apr 09 2020 at 13:34):

So here's the situation. As you've observed, for any Grothendieck site $(\mathcal{C},J)$ we have a pseudofunctor from any category $\mathcal{C}^{\mathrm{op}}$ into $\mathrm{Cat}$ sending each object of $\mathcal{C}$ to the poset of covering sieves over it and each morphism $f$ to the mapping which pulls sieves back along $f$; this is well-defined thanks to the stability axiom for G' topologies. Applying the Grothendieck construction we get a fibration $\int\mathcal{P} \to \mathcal{C}$ which has a right adjoint, this time thanks to the maximality axiom for G' topologies. Applying Yoneda, we get an adjoint pair of essential geometric morphisms between $\mathrm{PSh}(\int\mathcal{P})$ and $\mathrm{PSh}(\mathcal{C})$:
fibrationadjunction.png

The fact that an intersection of covering sieves is a covering sieve means that the colimits defining the left-most adjoint in this situation are filtered, so this functor preserves finite limits. That is, we have a diagram of geometric morphisms of the kind that I asked about very recently. Note also that $F^*$ and $\mathrm{Ran}_m$ are full and faithful, so the upward morphisms are geometric inclusions. These geometric morphisms contain all of the information we from the Grothendieck topology, in the sense that:

• $\mathrm{Lan}_F \circ \mathrm{Ran}_m$ is precisely the plus construction(!!!!)
• The 2-equalizer of the upward geometric morphisms, or equivalently the 2-pullback of one against the other, is precisely the subtopos of $J$-sheaves on $\mathcal{C}$.

Morgan Rogers (he/him) (Apr 09 2020 at 13:41):

This establishes a special case of the fact that geometric inclusions of toposes are regular monomorphisms, but also begs the question of whether some of the general properties of the plus construction (such as idempotence) are true for general situations of this form. One is also led to wonder whether this can be generalised to give a "universal property" characterisation of geometric inclusions in the 2-category of toposes and geometric morphisms. Finally, iirc the properties of fibrations are inherited (weakly) by $\mathrm{Lan}_F$, so we wonder if this can be transformed can be expressed concisely in a 2-categorical way. These are just some of the loose ends I mentioned.

Morgan Rogers (he/him) (Apr 09 2020 at 13:43):

@Ivan Di Liberti I mentioned this unfinished work to you a long time ago in Milan, perhaps you will find this interesting

Matteo Capucci (he/him) (Apr 09 2020 at 16:00):

Wow @Morgan Rogers , that's cool! Just to clarify, did you call $F$ the fibration $\int \mathcal P \to \mathcal C$?

vikraman (Apr 09 2020 at 16:21):

Maybe I'm missing context, what is $m$ and what is the plus construction?

Morgan Rogers (he/him) (Apr 09 2020 at 16:25):

Yes, that's right @Matteo Capucci. $m$ is the adjoint to the fibration that sends an object of $\mathcal{C}$ to the maximal sieve on that object.

Christian Williams (Apr 09 2020 at 19:31):

Matteo Capucci said:

Now this category should be the same as yours if you realize having an object of $\bf{C}$ and having the set of sieves on a given object is the same thing: just take the maximal sieve to recover your object.

No, $\int \mathrm{Sub}\circ y$ is not the category that I described. But thanks; yeah this was similar to my first guess.

Christian Williams (Apr 09 2020 at 19:35):

@Morgan Rogers That sounds cool! But I don't see how those ideas could give the category $\mathscr{S}(C,c)$ above.

Christian Williams (Apr 09 2020 at 19:36):

vikraman said:

Maybe I'm missing context, what is $m$ and what is the plus construction?

I think they're referring to sheafification.

Christian Williams (Apr 09 2020 at 19:36):

(just for everyone's sake. and I do not know what $m$ is.)

Christian Williams (Apr 09 2020 at 19:45):

Sorry, I realized that I was thinking of $\mathrm{Sub}$ as a covariant functor, taking the direct image. I need to rethink this for the contravariant case by pullback/precomposition.

Christian Williams (Apr 09 2020 at 19:45):

So let me take $\int \mathrm{Sub}\circ y$ --
objects: pairs $(c,P\rightarrowtail C(-,c))$
morphisms: $(c,P)\to (d,Q)$ are pairs $(f:c\to d, P\subset f^*(Q))$

Christian Williams (Apr 09 2020 at 19:47):

Ah okay, no this is not what either. If you look up at $\mathscr{S}(C,c)$, I'm pretty sure this category is fairly unusual. But I'll be happy if it has a canonical presentation.

Morgan Rogers (he/him) (Apr 09 2020 at 20:10):

But... where did your S(C,c) come from?

Morgan Rogers (he/him) (Apr 09 2020 at 20:11):

$\int \mathrm{Sub} \circ y$ is the construction I describe above in the case where the topology $J$ contains all sieves.

sarahzrf (Apr 09 2020 at 22:40):

aaa i dont have the attention span to read this whole chapter :sob:

sarahzrf (Apr 09 2020 at 22:43):

section 8.4 seems like the relevant bit, but i'm not sure i have the CT background

sarahzrf (Apr 09 2020 at 22:47):

Christian Williams said:

I'm thinking of sieves as types, in order to get something like a "category of types and terms" in the "kind context" $c$.

ooooh, hold on—i think i was taking for granted that $C$ was supposed to be the category that you're giving semantics in, like you're saying "i have a kind of type theory in mind, and to give it categorical semantics in a category $C$, you do this..."

sarahzrf (Apr 09 2020 at 22:48):

but the point is that there's an existing notion of that, and you're trying to come up with some particular class of models that you can derive from some $C$?

Christian Williams (Apr 09 2020 at 23:03):

Yes, we're taking $C$ as some predetermined category that we care/know about. Then from it we're making not a class of models, but one specific kind of type theory.

Christian Williams (Apr 09 2020 at 23:04):

You don't need to read that chapter; it's just some background.

Christian Williams (Apr 09 2020 at 23:05):

Morgan Rogers said:

But... where did your S(C,c) come from?

Yeah, so I should explain my motivation for this construction.

Christian Williams (Apr 09 2020 at 23:10):

I'm taking $C$ to be some kind of algebraic theory. Take the theory of monoids $\mathrm{Th.Mon}$. A sieve in a theory represents a "form" which represents a subset of terms you can make in the language.

Christian Williams (Apr 09 2020 at 23:12):

For example, the operation $m:2\to 1$ generates the sieve
$S(m)=\{o:n\to 1 \; | \; \exists \langle t_1,t_2 \rangle: n\to 2. \; o=m(t_1,t_2)\}$
-- the class of all terms which are the product of two terms.

Christian Williams (Apr 09 2020 at 23:14):

The sieves generated by the theory are like "base types", and various constructions in the presheaf topos are like type constructors.

Christian Williams (Apr 09 2020 at 23:16):

Turns out you can get quite a lot from this idea -- from an algebraic theory you can get a polymorphic type theory, with subtyping, recursion, and lots of nice things.

Christian Williams (Apr 09 2020 at 23:16):

Of course for very simple theories like $\mathrm{Th.Mon}$, it's not the most useful thing until you map this onto models. A type such as
$\mathrm{prime} := \neg [e] \wedge \neg[m(\neg[e],\neg[e])]$ is empty, because there aren't any concrete elements.

sarahzrf (Apr 09 2020 at 23:17):

so, one sec

Christian Williams (Apr 10 2020 at 04:25):

Alright, well let me know if you have thoughts. This thread is (hopefully) the final key to a paper I'm writing -- the main theorem will be that this process inputs an algebraic theory and outputs a polymorphic type theory.

Christian Williams (Apr 10 2020 at 04:28):

But I'm getting the impression that formalizing polymorphism in general is not a simple task. From what I've seen in the literature so far, people usually just take the specific example of System $\mathbb{F}$ and then augment that theory as needed; I haven't found much about polymorphic type theories in general.

Matteo Capucci (he/him) (Apr 10 2020 at 09:41):

Christian Williams said:

So let me take $\int \mathrm{Sub}\circ y$ --
objects: pairs $(c,P\rightarrowtail C(-,c))$
morphisms: $(c,P)\to (d,Q)$ are pairs $(f:c\to d, P\subset f^*(Q))$

I think me and @Morgan Rogers are using pullbacks while this is proper 'morphisms of sieves' (I don't have a better word: when you take all the arrows covering $d$ factorizing through arrows covering $c$)

Morgan Rogers (he/him) (Apr 10 2020 at 10:23):

Matteo Capucci said:

I think me and Morgan Rogers are using pullbacks while this is proper 'morphisms of sieves' (I don't have a better word: when you take all the arrows covering $d$ factorizing through arrows covering $c$)

No no, I'm not assuming $\mathcal{C}$ has pullbacks; in general the stability axiom defines, for a sieve $S$ on $C$ and $f:D \to C$, $f^*(S)$ to be the sieve on $D$ of morphisms whose composite with $f$ lies in $S$, or equivalently the pullback of $S$ along $y(f)$ when $S$ is viewed as a subobject of $y(C)$ in the presheaf category :check_mark:

Morgan Rogers (he/him) (Apr 10 2020 at 10:23):

Christian Williams said:

Of course for very simple theories like $\mathrm{Th.Mon}$, it's not the most useful thing until you map this onto models. A type such as
$\mathrm{prime} := \neg [e] \wedge \neg[m(\neg[e],\neg[e])]$ is empty, because there aren't any concrete elements.

I take it square brackets in this message correspond to the "sieve generated by..." thing you wrote above..?

Morgan Rogers (he/him) (Apr 10 2020 at 10:27):

And... I still don't see where the $\mathscr{S}(C,c)$ construction comes from: you've explained why you want sieves, but not why you want to pair them with arbitrary objects.

Christian Williams (Apr 10 2020 at 17:35):

Yes, I am not assuming that $C$ has pullbacks; the $f^*$ is essentially the preimage of sieves under postcomposition by $f$. That action should certainly be part of the morphism structure as well, we need base change in addition to morphisms of terms.

Christian Williams (Apr 10 2020 at 17:35):

Yes, brackets mean that. And then I should put some symbol to mean the lifting of $m$, rather than the actual operation.

Christian Williams (Apr 10 2020 at 17:39):

Well, at first I thought that I could simply let the types be the sieves, but I realized that didn't really make sense -- one still needs to know "where the terms are coming from", or what free variables they will have. So you also need to unpack the fact that a sieve is indexed by every object of the category; then the types are of the right specificity, $S(a)\subset C(a,c)$.

Chaitanya Leena Subramaniam (Apr 11 2020 at 08:35):

Hey @Morgan Rogers, very nice! Here are some additional remarks from a paper that Mathieu Anel and I recently finished (over two years or so) that might answer some of your questions. https://arxiv.org/abs/2004.00731
As you note, $\int P$ is the small full subcategory of $\widehat{C}^\rightarrow$ on the covering sieves, the codomain functor $t : \int P \to \widehat{C}$ factors through $C$ and $t : \int P \to C$ admits a section $m$ (a right adjoint right inverse). If you replace $\int P$ by any small full subcategory of arrows $W \subset \widehat{C}^\to$ satisfying the same conditions, you get what we call a pre-modulator (Def. 2.4.6). And of course every pre-modulator has a "plus-construction" given by the formula $t_! m_*$ that you mentioned.
Now a $J$-sheaf is simply an $X$ in $\widehat{C}$ that has the unique right lifting property against every arrow in $\int P$. One can similarly define a "$W$-sheaf" for any pre-modulator, and the category of $W$-sheaves is a locally presentable, reflective and accessibly (for some $\kappa$) embedded subcategory of $\widehat{C}$ (however it's not a topos, but I'll get to that). An interesting result (follows from Th. 2.4.8 of the paper) is that the reflection from presheaves into $W$-sheaves can be calculated as the transfinite iteration of the plus-construction $t_! m_*$. In fact Th. 2.4.8 says more: there is a relative plus-construction for arrows, whose transfinite iteration is the unique factorisation of any $f$ in $\widehat{C}^\to$ for the orthogonal factorisation system $({}^\bot(W^\bot), W^\bot)$, and the plus-construction for objects of $\widehat{C}$ is just the relative plus-construction for arrows into the terminal object. Moreover, every accessible reflection (and every accessible orth. fact. system) of a locally presentable category can be calculated as the iteration of the plus-construction associated to some pre-modulator (Prop. 2.4.13).
Coming to topoi: A pre-modulator such that $t : W \to C$ is a fibration is called a modulator (Def. 3.3.1) and a modulator such that each fibre of $t$ is (finitely) co-filtered is called a lex modulator (Def. 3.4.1). The orthogonal factorisation system associated to a (lex) modulator is what's known as a (lex) modality. Every accessible (lex) modality is generated by a (lex) modulator. The reflection associated to a lex modality preserves all pullbacks (and hence all finite limits). In 1-topoi, every modality is lex but this is no longer true for $\infty$-topoi. Finally, the plus construction associated to a lex modulator on an $\infty$-topos converges in $n+2$ iterations on an $n$-truncated object of the $\infty$-topos --- this implies that the plus construction for a lex modulator on a 1-topos converges in two iterations. The general theme of this "schmilblick" is that lex modulators are a correct generalisation of Grothendieck topologies from 1-topoi to $\infty$-topoi.
The paper is a little dense but hopefully the previous remarks are enough of a foothold.

Christian Williams (Apr 14 2020 at 05:14):

So here's the basic question I'm thinking about: given a category $C$, we can consider the composite $\Omega^{(-)}\circ y:C\to \mathrm{HeyAlg}$. This is a hyperdoctrine, and hence a particularly nice indexed category. But moreover, the objects of $\int \Omega^{(-)}\circ y$ are themselves subpresheaves, each of which has a category of elements. How do I unpack all of this information canonically?

Christian Williams (Apr 14 2020 at 05:15):

(Disclaimer: I'm opening up about a research question. If you give a really good answer I'll have to credit you.)

Christian Williams (Apr 14 2020 at 05:18):

Right now I'm considering what it means to "fold in" the category of elements construction to $\int \Omega^{(-)}\circ y$.

Christian Williams (Apr 14 2020 at 05:27):

The composite of the Yoneda embedding and the category of elements $\mathrm{el}\circ y: C\to \mathrm{Cat}$ is naturally isomorphic to the slice functor $C/(-)$. Subfunctors of representables should presumably give subcategories of the slice categories.

John Baez (Apr 14 2020 at 05:38):

Can you ask a question that's more specific than "how do I unpack all of this information canonically?"

The best questions in math are the yes-or-no questions, like "is 1 + 1 = 2?", since the answer is a truth value.

The second best questions are the ones that ask for an element of a set, like "what's 1+1?" or "how do I prove P?" where P is some true statement.

Often when you have a vaguer question you can find simpler sub-questions of the above two forms, which are a lot easier for people to sink their teeth into. This increases the chance of getting good answers.

Christian Williams (Apr 14 2020 at 05:40):

Alright, just got it but I'll ask as a puzzle: is there a natural bijection between (sieves on $c$) and (subcategories of $C/c$)?

John Baez (Apr 14 2020 at 05:53):

Let's see. Suppose $C$ is some finite linear order, for example

$0 \to 1 \to 2 \to 3 \to 4$

Then $C/4$ is just $C$ since $4$ is terminal, so subcategories of $C/4$ are just subsets of $\{0,1,2,3,4\}$, e.g.

$1 \to 2 \to 4$

There are $2^5$ of them. But there aren't $2^5$ sieves on $4$. I think there are just $5$, right?

Christian Williams (Apr 14 2020 at 05:57):

Yeah, there are definitely more slice subcategories.

Christian Williams (Apr 14 2020 at 05:57):

Would you not have to include $4$ (its identity) in every subcategory?

Christian Williams (Apr 14 2020 at 05:58):

Hm, I guess not... And yes, I think just 5 sieves.

Christian Williams (Apr 14 2020 at 06:01):

We have a section-retraction pair between sieves and subslices. Given $P\subset C(-,c)$ we have $\int P \subset C/c$, and given a subcategory of $C/c$ we can saturate it (close under precomposition) to get a sieve -- but of course this destroys a lot of information.

John Baez (Apr 14 2020 at 06:05):

Okay, nice. I was gonna say the obvious thing, that every sieve gives a subcategory of the slice category but it sounds like you're saying that the functor

[sieves on $C$] $\to$ [subcategories of $C/c$]

has a left adjoint, the "saturation" process.

John Baez (Apr 14 2020 at 06:06):

I haven't checked that it's a left adjoint, it just feels like one.

Christian Williams (Apr 14 2020 at 06:07):

Yep. Well, we haven't even decided how we're making categories out of these two concepts.

John Baez (Apr 14 2020 at 06:07):

Right. I think there's a pretty obvious poset structure in both cases, right?

Christian Williams (Apr 14 2020 at 06:08):

Sieves on $c$ form a preorder by inclusion. Subcategories of $C/c$...

John Baez (Apr 14 2020 at 06:08):

Subcategories of $C/c$ are subobjects of $C/c \in \mathsf{Cat}$.

John Baez (Apr 14 2020 at 06:08):

It looks like there's a Heyting algebra structure in both cases!

Christian Williams (Apr 14 2020 at 06:09):

Yeah, of course. We're carrying some relation of $C(-,c)$ and $C/c$ through the subobject functor.

John Baez (Apr 14 2020 at 06:09):

No, maybe I'm getting carried away: there's no reason I see for the poset of subobjects of a category to form a Heyting algebra.

John Baez (Apr 14 2020 at 06:10):

$\mathsf{Cat}$ isn't a topos.

John Baez (Apr 14 2020 at 06:10):

But still subobjects of a category should form some pretty nice kind of poset, better than a mere topos.

John Baez (Apr 14 2020 at 06:13):

Puzzle. Is $\mathsf{Cat}$ locally cartesian closed?

I don't know, but I'll bet "no".

Christian Williams (Apr 14 2020 at 06:18):

No, it's not... @Mike Shulman told us about this when we visited. Some functors induce nice base change, but not all -- that's part of the motivation for the concept of exponentiable morphism in a 2-category https://ncatlab.org/nlab/show/Conduch%C3%A9+functor.

Christian Williams (Apr 14 2020 at 06:19):

The counterexample was very clever. I think it involves constructing a simple pushout which is not preserved by the base change, hence showing that it is not a left adjoint.

John Baez (Apr 14 2020 at 06:20):

Cool! I'd talked with David Spivak about Conduche functors, but I hadn't known about this more abstract way of thinking about them.

John Baez (Apr 14 2020 at 06:21):

That nLab page gives the counterexample but I'm not up to understanding it now.

John Baez (Apr 14 2020 at 06:22):

It's a pretty heavy page - it includes some generalizations of the Grothendieck construction...

Christian Williams (Apr 14 2020 at 06:25):

Oh yeah, it's a lot to think about.

Christian Williams (Apr 14 2020 at 06:26):

sieve-and-slice.jpg

Christian Williams (Apr 14 2020 at 06:27):

The left triangle is an isomorphism, and then I think the right should be a pair of natural transformations which form a section-retraction.

Chaitanya Leena Subramaniam (Apr 14 2020 at 06:31):

John Baez said:

Puzzle. Is $\mathsf{Cat}$ locally cartesian closed?

I don't know, but I'll bet "no".

On a related note I tried (and failed) yesterday to find an example of a locally presentable, locally cartesian closed 1-category that's not a quasitopos. Does anyone know of one?

sarahzrf (Apr 14 2020 at 07:07):

John Baez said:

Can you ask a question that's more specific than "how do I unpack all of this information canonically?"

The best questions in math are the yes-or-no questions, like "is 1 + 1 = 2?", since the answer is a truth value.

The second best questions are the ones that ask for an element of a set, like "what's 1+1?" or "how do I prove P?" where P is some true statement.

Often when you have a vaguer question you can find simpler sub-questions of the above two forms, which are a lot easier for people to sink their teeth into. This increases the chance of getting good answers.

"best" for different purposes...

sarahzrf (Apr 14 2020 at 07:08):

Cat is not locally cartesian closed

sarahzrf (Apr 14 2020 at 07:08):

there's a whole thing on mike shulman's sub-nlab about 2-topoi and how we shouldn't expect them to be stable under slicing

sarahzrf (Apr 14 2020 at 07:08):

but instead we should expect them to be stable under fibrational slice

sarahzrf (Apr 14 2020 at 07:10):

quick reference: https://ncatlab.org/nlab/show/regular+category
note that "a locally cartesian closed category with coequalizers is regular" but immediately lower is an example that Cat is not regular

sarahzrf (Apr 14 2020 at 07:10):

but do not ask me questions about regular categories, i dont know anything about them, im just passing on the counterargument i got from someone else :upside_down:

sarahzrf (Apr 14 2020 at 07:11):

oh wait lol i missed that @Christian Williams already responded >.<

Alexander Campbell (Apr 14 2020 at 07:17):

Chaitanya Leena Subramaniam said:

On a related note I tried (and failed) yesterday to find an example of a locally presentable, locally cartesian closed 1-category that's not a quasitopos. Does anyone know of one?

This is a difficult problem with an interesting history, see Section 4 of Borceux and Pedicchio, A characterization of quasi-toposes. One example described therein, due to Adamek and Rosicky, is the category of sets equipped with a "loop-free" reflexive binary relation. Another example (Example C.4.2.4 in the Elephant) is the Ind-completion of the category of countable (= finite or countably infinite) sets.

sarahzrf (Apr 14 2020 at 07:56):

there was that whole topic on here i opened about slices or w/e and i seem to recall coming to the conclusion that in a 2-category the 1-slice is the wrong notion of "category of things parameterized over the base" anyway

sarahzrf (Apr 14 2020 at 07:56):

like maybe local cartesian closure is the wrong thing to expect anyway

sarahzrf (Apr 14 2020 at 07:57):

maybe fibrational slice in Cat is more closely analogous to ordinary slice in a 1-category than ordinary slice in Cat is

Oscar Cunningham (Apr 14 2020 at 10:23):

Is there a definition of 'fibration' that works in an arbitrary $2$-category, or can we only define them in $\mathbf{Cat}$ by referring to morphisms directly?

Morgan Rogers (he/him) (Apr 14 2020 at 10:28):

It's only tangentially related but worth mentioning that some properties of Grothendieck topologies are easiest to express when the sieves are viewed as subcategories of slices. For example, a locally connected site is one for which the sieves are all (inhabited and) connected as subcategories of slices; these are the natural choice of sites for locally connected toposes over a given base topos.

sarahzrf (Apr 14 2020 at 15:27):

i believe theres one that works in an arbitrary 2-cat but i dont remember it

sarahzrf (Apr 14 2020 at 15:29):

oh it looks like you need finite completeness to be able to state it? not surprising

sarahzrf (Apr 14 2020 at 15:30):

oh wait maybe not

sarahzrf (Apr 14 2020 at 15:30):

anyway https://ncatlab.org/nlab/show/fibration+in+a+2-category#definition

Oscar Cunningham (Apr 14 2020 at 15:48):

Thanks! I should have been able to guess that first definition. 'Just Yoneda It'.

sarahzrf (Apr 15 2020 at 00:20):

Morgan Rogers said:

It's only tangentially related but worth mentioning that some properties of Grothendieck topologies are easiest to express when the sieves are viewed as subcategories of slices. For example, a locally connected site is one for which the sieves are all (inhabited and) connected as subcategories of slices; these are the natural choice of sites for locally connected toposes over a given base topos.

omg somehow it never occurred to me that a sieve is a subcategory of a slice o_o

sarahzrf (Apr 15 2020 at 00:21):

i should try thinking in terms of categories of elements more often...

Mike Shulman (Apr 15 2020 at 00:56):

Alexander Campbell said:

Chaitanya Leena Subramaniam said:

On a related note I tried (and failed) yesterday to find an example of a locally presentable, locally cartesian closed 1-category that's not a quasitopos. Does anyone know of one?

This is a difficult problem with an interesting history, see Section 4 of Borceux and Pedicchio, A characterization of quasi-toposes. One example described therein, due to Adamek and Rosicky, is the category of sets equipped with a "loop-free" reflexive binary relation. Another example (Example C.4.2.4 in the Elephant) is the Ind-completion of the category of countable (= finite or countably infinite) sets.

At this MO question 1-categorical motivic spaces were suggested as another example.