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: learning: questions

Topic: "monoidal limit"

Bruno Gavranović (Dec 20 2021 at 23:18):

Hi, I'm trying to figure out what completes the following pattern:

product  : monoidal product : coproduct
pullback :         ?        : pushout

That is, if monoidal product is the common generalization of a product and coproduct, what the common generalization of pullback and pushout?
Similarly for other limits - do they have a "monoidal variant"?

A possible hint is that a product in the slice category $\mathcal C / X$ is a pullback in the underlying category $\mathcal C$. And a coproduct in the coslice category $X / \mathcal C$ is a pushout in the underlying category $\mathcal C$. It should be possible to fill in the pattern for the monoidal case, but I don't know how.

Ralph Sarkis (Dec 20 2021 at 23:32):

Isn't the unit (terminal : unit : initial) kind of important in the first line ? You'd have to translate that first.

Bruno Gavranović (Dec 20 2021 at 23:51):

Ralph Sarkis said:

Isn't the unit (terminal : unit : initial) kind of important in the first line ? You'd have to translate that first.

Hmm, good point - the empty case always gives lots of hints. What does "unit" mean here, is that just the unit of the monoidal product? If that is so, it doesn't seem like there's much to do. It does feel strange to write "unit" there, though, since it's a part of the definition of a monoidal product. On the other hand, the terminal object is needed to define a cartesian product.

Edit:
I'll keep the table concise in the original question, but I'll add your suggestion (and others) here:

terminal  : monoidal unit    : initial
product   : monoidal product : coproduct
pullback  :         ?        : pushout
equalizer :         ?        : coequalizer

Nathanael Arkor (Dec 21 2021 at 00:20):

I'm skeptical you can complete this table. One reason product and coproduct structure can both be instances of monoidal structure is that they're discrete, i.e. the shape of a product and the shape of a coproduct are identical (ignoring the (co)projections). However, pullbacks and pushouts are non-discrete, involving morphisms that are in direction for pullback and another for pushouts. The only way I could see them both being integrated into a single structure is if you have an operator on (not-necessarily-commutative) squares in the category.

Bruno Gavranović (Dec 21 2021 at 00:23):

Interesting point, I was just thinking something similar looking at this diagram from Math3ma's blog. Screenshot_20211221_012135.png

It does look like there's directionality at play :thinking: That is, given a discrete diagram, computing its limit I get a product, and its colimit I get a coproduct. But given the diagram in the top left, computing the limit gives me the pullback, while computing its colimit gives me something trivial.

Bruno Gavranović (Dec 21 2021 at 00:31):

At the very least, I'd still like to figure out what completes the pattern

terminal : monoidal unit
product  : monoidal product
pullback :        ?

This should still have an unambiguous answer.

Nathanael Arkor (Dec 21 2021 at 00:34):

You can consider categories $\mathbf C$ equipped with a functor $[\bullet \to \bullet \leftarrow \bullet, \mathbf C] \to \mathbf C$, subject to suitable axioms (the analogues of the pasting lemmas for pullbacks).

Nathanael Arkor (Dec 21 2021 at 00:34):

Here $\bullet \to \bullet \leftarrow \bullet$ is the free cospan.

Bruno Gavranović (Dec 21 2021 at 00:41):

Oh, I assume this is because a monoidal category has the data of, among other things, a functor $\otimes : \mathcal C \times \mathcal C \to \mathcal C$. And this functor can be rewritten as $\otimes : [2, \mathcal C] \to \mathcal C$, where $2$ is the discrete two-object category.
I've never seen monoidal categories presented as such, this perspective is entirely novel to me!

Nathanael Arkor (Dec 21 2021 at 01:00):

Yes, this is really just a categorification of the notion of algebra for an endofunctor. For instance, a magma is a set $X$ equipped with a function $X \times X \to X$ or, alternatively, a function $X^2 \to X$.

Nathanael Arkor (Dec 21 2021 at 01:00):

But when we move to (2-)algebraic structure on categories, we can now use more interesting exponents, namely categories.

Bruno Gavranović (Dec 21 2021 at 01:02):

Right, so a monoidal category (together with the unit) can be described as a functor of type $\mathcal{C}^2 + 1 \to \mathcal{C}$. I suppose algebra laws (pseudo in this case) recover all the coherence rules for a monoidal category.

Nathanael Arkor (Dec 21 2021 at 01:13):

Well, the functor just captures the tensor product and unit. The natural transformations and coherence laws have to be provided on top of that. (Alternatively, all the data can be packaged up as the data for an algebra for a certain 2-monad.)

Mike Shulman (Dec 21 2021 at 01:33):

Perhaps one could produce examples of "monoidal pullbacks" from a context like Weisbart-Yassine Constructing Span Categories From Categories Without Pullbacks.

Nathanael Arkor (Dec 21 2021 at 01:54):

Street also has a notion of "fake pullbacks" that he uses to construct more general categories of spans. (I'm not familiar with either framework, though.)

Ralph Sarkis (Dec 21 2021 at 07:20):

Bruno Gavranovic said:

What does "unit" mean here, is that just the unit of the monoidal product? If that is so, it doesn't seem like there's much to do. It does feel strange to write "unit" there, though, since it's a part of the definition of a monoidal product.

Yes, my idea was more that in that the monoidal unit is in the definition of the monoidal product while a category with binary (co)product doesn't necessarily have a terminal (initial) object. I realize now that saying

finite products : monoidal products : finite coproducts

works too. Still, I think this maybe needs translating to the second line, pullbacks and pushouts are usually binary, but I see a straightforward generalization (as products in the (co)slice category) to a finite number of morphisms. The unit would be the "family" (maybe a more formal sense of family) of all identity morphisms. Anyway, all of this falls in the try to see how to suitably combine monoidal products on each (co)slice category into a convenient definition in the base category.

Patrick Nicodemus (Dec 21 2021 at 07:23):

I would write
product : biproduct : coproduct

Patrick Nicodemus (Dec 21 2021 at 07:27):

Anyway I don't feel there's a good answer to your question. My favorite example of a monoidal product is the tensor product of modules over a ring, which seems to be somewhat unrelated to products and coproducts except that it distributes over them. I'm not sure how this would fit into your schema.

Ralph Sarkis (Dec 21 2021 at 07:35):

Nathanael Arkor said:

You can consider categories $\mathbf C$ equipped with a functor $[\bullet \to \bullet \leftarrow \bullet, \mathbf C] \to \mathbf C$, subject to suitable axioms (the analogues of the pasting lemmas for pullbacks).

This goes in another direction I think could be quite interesting. Here are some questions that fed my insomnia last night. Let $\mathbf{J}$ be a finite (or small) category and $\mathbf{C}$ be a category with limits of shape $\mathbf{J}$. Given an isomorphism $\mathsf{swap} : \mathbf{J} \rightarrow \mathbf{J}$, you have the following two adjunctions (where $\Delta$ is the diagonal functor):
image.png

In the case where $\mathbf{J} = \mathbf{2}$, the top composition is naturally isomorphic (using choice --- edit: I am doubting myself, now I think you don't need choice) to $\lim_{\mathbf{J}}$. This is because $\mathsf{swap}$ is either the identity or the swapping of the two objects and products are commutative (up to isomorphisms). Is this also true for any $\mathbf{J}$? What about $\mathbf{J}$ finite or discrete? Can we characterize the properties of $\mathsf{swap}$ that make this true?

Paolo Perrone (Dec 21 2021 at 08:22):

The conditional product in the category of measure spaces could be an example of this "monoidal pullback". (It's not very well behaved though.)
A relevant paper is here.

Paolo Perrone (Dec 21 2021 at 08:24):

Also, Tobias Fritz and Eigil Rischel defined "Kolmogorov products", which can be thought of as monoidal analogues of infinite products. Paper here.

Paolo Perrone (Dec 21 2021 at 08:31):

There's also David Spivak's idea of exact square.

Morgan Rogers (he/him) (Dec 21 2021 at 09:26):

One way that people study "locally monoidal" categories which works in a category with pullbacks is to only allow slicing at coalgebras for the monoidal product, and to pull back along the comonoid structure maps to obtain a monoidal product in the slice

Bruno Gavranović (Dec 21 2021 at 09:46):

Nathanael Arkor said:

Well, the functor just captures the tensor product and unit. The natural transformations and coherence laws have to be provided on top of that. (Alternatively, all the data can be packaged up as the data for an algebra for a certain 2-monad.)

Does that monad have the same underlying endofunctor as what I wrote? That is, is it $[2, -] + 1 : \mathbf{Cat} \to \mathbf{Cat}$, or something different? Unpacking the unit, we'd need a functor $\eta_{\mathcal C} : \mathcal C \to [2, \mathcal C] + 1$ which we can define (for $A : \mathcal C$ always returns the left summand, the constant functor at $A$), but I'm not sure if this is the right direction. (The join is also a bit complicated, and I'm not sure how to interpret it)

I'm asking because it feels like this could help with the original question: if a monoidal category is an algebra for a 2-monad, perhaps a product category is too? It looks like the underlying endofunctor there is something like $[2, -]$.

Bruno Gavranović (Dec 21 2021 at 09:47):

Patrick Nicodemus said:

I would write
product : biproduct : coproduct

A biproduct is both a product and a coproduct. Which seems like a specialization of both, rather than a generalization

Bruno Gavranović (Dec 21 2021 at 09:52):

Ralph Sarkis said:

Bruno Gavranovic said:

What does "unit" mean here, is that just the unit of the monoidal product? If that is so, it doesn't seem like there's much to do. It does feel strange to write "unit" there, though, since it's a part of the definition of a monoidal product.

Yes, my idea was more that in that the monoidal unit is in the definition of the monoidal product while a category with binary (co)product doesn't necessarily have a terminal (initial) object. I realize now that saying

finite products : monoidal products : finite coproducts

works too. Still, I think this maybe needs translating to the second line, pullbacks and pushouts are usually binary, but I see a straightforward generalization (as products in the (co)slice category) to a finite number of morphisms. The unit would be the "family" (maybe a more formal sense of family) of all identity morphisms. Anyway, all of this falls in the try to see how to suitably combine monoidal products on each (co)slice category into a convenient definition in the base category.

Uh yeah, I meant finite for all of them

Tobias Fritz (Dec 21 2021 at 10:09):

Another paper where we had explored a related idea is Compositories and Gleaves. The idea was that while the gluing of sections in a sheaf is unique, one can imagine a structure where the gluing of compatible pairs of local sections is instead an algebraic structure satisfying conditions such as an associativity axiom. This was intended to axiomatize the conditional products of probability distributions that @Paolo Perrone mentioned.

There is some more theory that one can develop of these gadgets than what is in the paper. But ultimately this hasn't appeared, mainly because there seems to be a lack of good examples other than conditional products. So if Bruno or anyone else can think of additional ones, then I'd be eager to hear about them.

Tobias Fritz (Dec 21 2021 at 10:13):

There's also another MO discussion where a very similar question was asked by David Spivak.

Sam Speight (Dec 21 2021 at 10:23):

Possibly relevant MO discussion: https://mathoverflow.net/questions/205902/what-is-the-monoidal-equivalent-of-a-locally-cartesian-closed-category

Martti Karvonen (Dec 21 2021 at 13:48):

This MO question asks the same thing about equalizers

Martti Karvonen (Dec 21 2021 at 13:59):

Bruno Gavranovic said:

Does that monad have the same underlying endofunctor as what I wrote? That is, is it $[2, -] + 1 : \mathbf{Cat} \to \mathbf{Cat}$, or something different? Unpacking the unit, we'd need a functor $\eta_{\mathcal C} : \mathcal C \to [2, \mathcal C] + 1$ which we can define (for $A : \mathcal C$ always returns the left summand, the constant functor at $A$), but I'm not sure if this is the right direction. (The join is also a bit complicated, and I'm not sure how to interpret it)

I'm asking because it feels like this could help with the original question: if a monoidal category is an algebra for a 2-monad, perhaps a product category is too? It looks like the underlying endofunctor there is something like $[2, -]$.

Strict monoidal categories can be captured as the (strict) algebras of the free strict monoidal category 2-monad, sending $C$ to $\coprod_{n\in\mathbb{N}} C^n$. For unbiased monoidal categories, you can take the pseudoalgebras for this 2-monad, whereas if you want to capture monoidal categories on the nose, you need a different 2-monad which I don't know off the top of my head.

Categories with finite products also form the algebras for a 2-monad, but I haven't looked up the construction. I guess the finite product completion will do the job?

Nathanael Arkor (Dec 21 2021 at 15:31):

In other words, the 2-monad is defined by closure under the operations (i.e. all induced n-ary operations, not just the generating ones).

Nathanael Arkor (Dec 21 2021 at 15:32):

Martti Karvonen said:

Categories with finite products also form the algebras for a 2-monad, but I haven't looked up the construction. I guess the finite product completion will do the job?

Yes, that's right.

Nathanael Arkor (Dec 21 2021 at 15:32):

I.e. the dual of the family (Fam) construction.

Matteo Capucci (he/him) (Dec 21 2021 at 17:42):

Bruno Gavranovic said:

Nathanael Arkor said:

Well, the functor just captures the tensor product and unit. The natural transformations and coherence laws have to be provided on top of that. (Alternatively, all the data can be packaged up as the data for an algebra for a certain 2-monad.)

Does that monad have the same underlying endofunctor as what I wrote? That is, is it $[2, -] + 1 : \mathbf{Cat} \to \mathbf{Cat}$, or something different? Unpacking the unit, we'd need a functor $\eta_{\mathcal C} : \mathcal C \to [2, \mathcal C] + 1$ which we can define (for $A : \mathcal C$ always returns the left summand, the constant functor at $A$), but I'm not sure if this is the right direction. (The join is also a bit complicated, and I'm not sure how to interpret it)

I'm asking because it feels like this could help with the original question: if a monoidal category is an algebra for a 2-monad, perhaps a product category is too? It looks like the underlying endofunctor there is something like $[2, -]$.

Cartesian monoidal categories (i.e. categories with a functorial choice of products) are algebras of a 2-monad described by Lack and Kelly here:

• Kelly, Lack - On property-like structures, 1991, TAC

Matteo Capucci (he/him) (Dec 21 2021 at 17:50):

Bruno Gavranovic said:

Hi, I'm trying to figure out what completes the following pattern:

product  : monoidal product : coproduct
pullback :         ?        : pushout

That is, if monoidal product is the common generalization of a product and coproduct, what the common generalization of pullback and pushout?

Btw, why do you think those things fit in that pattern?
In better words, what do the : mean in the above?

Bruno Gavranović (Dec 21 2021 at 21:25):

Matteo Capucci (he/him) said:

Btw, why do you think those things fit in that pattern?
In better words, what do the : mean in the above?

You're right, : is probably a very misleading character there. I don't mean to impose some linear order there, but merely say that product and coproduct are generalised by a monoidal product. Perhaps it should be something like a span whose apex is "monoidal product". Then similarly I expected to find the apex for the span whose feet are "pullback" and "pushout".

But as someone pointed out, there's the issue of directionality, and there's the question of whether this pattern can even be competed.

But that's fine, I'd be happy to figure out what completes just the following pattern:

product   : monoidal product
pullbacks :      ?

Paolo Perrone (Dec 21 2021 at 21:39):

Bruno Gavranovic said:

But that's fine, I'd be happy to figure out what completes just the following pattern:

product   : monoidal product
pullbacks :      ?

But how do you want to complete the pattern above? By taking the pushout of that table, or with something more 'monoidal' in flavour? :p

Bruno Gavranović (Dec 21 2021 at 22:01):

Something monoidal in flavour. The idea is that a product is a limit of a discrete diagram. Monoidal product generalises that notion. Pullback is a limit of a cospan diagram. I'm wondering whether there's a suitable "monoidal" notion that generalises it.
(There's been many responses in this thread and I haven't yet had a chance to meditate on some of them)

Matteo Capucci (he/him) (Dec 22 2021 at 08:09):

Bruno Gavranovic said:

I don't mean to impose some linear order there, but merely say that product and coproduct are generalised by a monoidal product.

But what does it mean here to 'generalise'? Also 'limits' generalise products, or '2-products', or Sigma-types, or indexed products, etc. This applies to : but also to \n: what's the relationship between 'product' and 'pullback'?
I'm not asking these questions to annoy you, on the contrary, it's to focus the question. Choosing the 'right' point of view is a crucial step, and the answer you seek is dependent on this choice.
For instance, if the : is interpreted as 'has the algebraic structure of', and \n as 'slice-wise' (pullbacks are cartesian products in a slice), then ? is automatically replaced by 'pseudofunctor $\mathcal C^\circ \to \mathbf{MonCat}_{st}$ factoring $\mathcal C/-$ equipping each slice with a monoidal structure'.

Paolo Perrone (Dec 22 2021 at 12:04):

Would the conditional product of probability be an example of the construction you want?
Or do you have any other concrete examples in mind?

Bruno Gavranović (Dec 23 2021 at 00:23):

Matteo Capucci (he/him) said:

Bruno Gavranovic said:

I don't mean to impose some linear order there, but merely say that product and coproduct are generalised by a monoidal product.

But what does it mean here to 'generalise'?

I'm thinking of it like this: a product is a pair, it's something where I can not just put two things in parallel, but I can uniquely copy and delete things. I can generalise this setting by not requiring unique copying and deletion: this lands me in the setting of linear types, i.e. the theory of monoidal categories.
This is the whole setting of lenses (which involve products) and optics (which involve monoidal products).

But I'm interested in the same relationship, but with dependent types: i.e. dependent lenses (which involve pullbacks) and dependent optics (which involve ??). You know all this already - just thought I'd unpack this to be on the same page.
Now, when thinking about pullbacks (i.e. products in a slice category), I still have unique copy and deletion, and it seems sensible to ponder how to generalise this in the same way. But I don't know what that would even mean.
I suppose understanding what I'm trying to do would give me the answer. Maybe I'm hoping someone here has intuitions about what I should be expecting.

is automatically replaced by 'pseudofunctor $\mathcal C^\circ \to \mathbf{MonCat}_{st}$ factoring $\mathcal C/-$ equipping each slice with a monoidal structure'.

Okay, I'm not sure I see how that follows exactly (I remember we might've talked about this...)

Bruno Gavranović (Dec 23 2021 at 00:28):

Paolo Perrone said:

Would the conditional product of probability be an example of the construction you want?
Or do you have any other concrete examples in mind?

I'm afraid I'm not even sure which definition in that paper is the one you're referring to. This paper assumes lots of things I don't know, and it's hard for me to say right now.

At the very least, it would seem strange that such an abstract definition popped up in such a concrete setting, as is the one of probability distributions. I'm assuming the paper deals with something like Markov categories, which are natural w.r.t. deletion - but the thing I'm curious about in its full generality ought to work in a purely monoidal setting, where we might not have unique delete maps.

Dylan Braithwaite (Dec 23 2021 at 01:09):

Bruno Gavranovic said:

This is the whole setting of lenses (which involve products) and optics (which involve monoidal products).

It sounds like maybe the table you’re really interested in is something like

lenses           : cartesian category
optics           : monoidal category
dependent lenses : category with pullbacks
dependent optics : ?

Which also begs the question of whether ‘category with pullbacks’ is the right thing to associate with dependent lenses.

Another candidate might be

lenses           : cartesian category
optics           : monoidal category
dependent lenses : codomain fibration
dependent optics : ?

The codomain fibration existing (as opposed to just the codomain opfibration) implies the existence of pullbacks, but that maybe isn’t what we should be focusing on when thinking about dependent lenses. It just happens to be what’s required to define the reindexing functor for that fibration.
In which case, as we’ve seen, the ‘?’ could be something like ‘monoidal bifibration’.

Dylan Braithwaite (Dec 23 2021 at 01:28):

Put another way, the codomain fibration is a setting where we can talk about dependent pairs and form cartesian products in the fibres (by pullback). And a monoidal bifibration is a setting where we can talk about dependent pairs and form monoidal products in the fibres

Matteo Capucci (he/him) (Dec 23 2021 at 09:49):

Bruno Gavranovic said:

Now, when thinking about pullbacks (i.e. products in a slice category), I still have unique copy and deletion, and it seems sensible to ponder how to generalise this in the same way. But I don't know what that would even mean.

If you decided products should become monoidal products in this generalisation, then 'products in a slice category' should become 'monoidal products in a slice category', no?
Hence pullbacks = 'locally cartesian' (each slice has a cartesian product, and reindexing preserves is) gets automatically translated to 'locally monoidal' (each slice has a monoidal product, and reindexing preserves it)
It's a matter of choice if you want reindexing in the second instance to be given again by pullback or you also abstract that away. In any case you get an indexed monoidal category $\mathcal C^{op} \to \mathbf{MonCat}$

Matteo Capucci (he/him) (Dec 23 2021 at 09:53):

Or as Dylan put it:
Dylan Braithwaite said:

Put another way, the codomain fibration is a setting where we can talk about dependent pairs and form cartesian products in the fibres (by pullback). And a monoidal bifibration is a setting where we can talk about dependent pairs and form monoidal products in the fibres

Matteo Capucci (he/him) (Dec 23 2021 at 09:56):

Dylan Braithwaite said:

The codomain fibration existing (as opposed to just the codomain opfibration) implies the existence of pullbacks, but that maybe isn’t what we should be focusing on when thinking about dependent lenses. It just happens to be what’s required to define the reindexing functor for that fibration.

I agree with this sentiment, it seems a bit of an accident that in the codomain fibration (aka the slice indexing) pullbacks give you both local monoidal structure and reindexing operations. The two things could be formally unrelated, with the only requirement reindexing should be compatible with the local monoidal structure (i.e. 'the pasting lemma holds')

Matteo Capucci (he/him) (Dec 23 2021 at 09:56):

Indeed, F-lenses are dependent lenses constructed from any indexed category

Graham Manuell (Dec 23 2021 at 11:32):

I haven't read the above discussion carefully enough to see if anyone has already mentioned this, but a good generalisation of pullbacks to monoidal categories is given by composition ('tensor products') in the associated bicategory of comonoids and bicomodules. See here and here.

Bruno Gavranović (Dec 27 2021 at 23:05):

Matteo Capucci (he/him) said:

Dylan Braithwaite said:

The codomain fibration existing (as opposed to just the codomain opfibration) implies the existence of pullbacks, but that maybe isn’t what we should be focusing on when thinking about dependent lenses. It just happens to be what’s required to define the reindexing functor for that fibration.

I agree with this sentiment, it seems a bit of an accident that in the codomain fibration (aka the slice indexing) pullbacks give you both local monoidal structure and reindexing operations. The two things could be formally unrelated, with the only requirement reindexing should be compatible with the local monoidal structure (i.e. 'the pasting lemma holds')

Yeah, this resonates with me too. It would be very surprising if codomain fibration is somehow central to dependent lenses. After all, the fibration corresponding to the slice functor is the one that defines dependent lenses: having a different fibration play a central role would be strange.

If you decided products should become monoidal products in this generalisation, then 'products in a slice category' should become 'monoidal products in a slice category', no?

Yeah! But here's where I'm stuck at: if pullbacks in the base correspond to products in the slice, then what construction in the base gives us monoidal products in the slice?

Dylan Braithwaite (Dec 27 2021 at 23:12):

Bruno Gavranovic said:

It would be very surprising if codomain fibration is somehow central to dependent lenses. After all, the fibration corresponding to the slice functor is the one that defines dependent lenses: having a different fibration play a central role would be strange.

I’m not sure if I’m understanding correctly what you’re saying here, but the codomain fibration is the fibration corresponding to the slice functor

Bruno Gavranović (Dec 27 2021 at 23:14):

Huh, what? Are you saying that the indexed category corresponding to the codomain fibration is the functor $\mathcal{C} / - : \mathcal{C}^{op} \to \mathbf{Cat}$?

Zhen Lin Low (Dec 27 2021 at 23:15):

Yes, that's right.

Bruno Gavranović (Dec 27 2021 at 23:16):

Okay, I thought these were different things :sweat_smile: I also now see on nLab the slice functor is mentioned practically in the beginning, I don't know how I've missed that...

Dylan Braithwaite (Dec 27 2021 at 23:16):

Where the codomain fibration in this context is $\mathbf{Arr}(\mathcal C) \to \mathcal C$ as opposed to the one we have also been working with that maps onto the delooping

Bruno Gavranović (Dec 27 2021 at 23:19):

But something is confusing to me, if the fibration is $\mathbf{Arr}(\mathcal{C}) \to \mathcal{C}$, this means the total space is $\mathbf{Arr}(\mathcal{C})$. But we know that applying the Grothendieck construction to the slice functor gives us dependent lenses, and dep. lenses are not equivalent to $\mathbf{Arr}(\mathcal{C})$?

Dylan Braithwaite (Dec 27 2021 at 23:20):

Applying the grothendieck construction to the opposite of the slice functor gives us dependent lenses

Dylan Braithwaite (Dec 27 2021 at 23:21):

Ie the codomain fibration is the fibrewise opposite of the view fibration

Bruno Gavranović (Dec 27 2021 at 23:22):

Dylan Braithwaite said:

Applying the grothendieck construction to the opposite of the slice functor gives us dependent lenses

You mean "pointwise opposite", right?

Dylan Braithwaite (Dec 27 2021 at 23:22):

Yeah

Bruno Gavranović (Dec 27 2021 at 23:24):

Okay, this might explain my confusion. So this is fibrewise opposite of the view fibration, as you say. That makes sense!

Dylan Braithwaite (Dec 27 2021 at 23:27):

The thing that Matteo and I were saying seems like a coincidence is that reindexing is the same thing as taking a product in the fibres of this fibration. So when you want to generalise pullbacks, you have to decide whether you’re trying to generalise the operation of reindexing or of taking a product in the fibres.

Zhen Lin Low (Dec 27 2021 at 23:37):

I don't think it's good to say that reindexing is the same thing as taking a (ahem) fibre product. There is a type error here! But you can take the pushforward of the reindexing and then you really do get two objects in the same fibre that are naturally isomorphic.

Zhen Lin Low (Dec 27 2021 at 23:40):

I think the indexed monoidal category of modules over commutative rings is instructive as a non-cartesian example. But here too there is a natural isomorphism between pushforward-of-reindexing and the tensor product, albeit with some difference in handedness...

Dylan Braithwaite (Dec 27 2021 at 23:49):

Zhen Lin Low said:

I don't think it's good to say that reindexing is the same thing as taking a (ahem) fibre product. There is a type error here! But you can take the pushforward of the reindexing and then you really do get two objects in the same fibre that are naturally isomorphic.

Right yeah, this is the issue I was trying to point at. When talking about dependent lenses they’re usually described in terms of pullbacks in $\mathcal C$. But thinking about them in terms of the codomain fibration adds finer-grained typing. You have to decide whether the pullback is an instance of a reindexing or a product