Product in `over X` vs fibered product

Stream: Is there code for X?

[Adam Topaz]

If X : C with C a category, do we have any way of relating the product of two (or more) objects in over X to the fibered product (over X) in C? @Scott Morrison @Bhavik Mehta

[Bhavik Mehta]

There's some stuff in constructions/over for this!

[Bhavik Mehta]

But I made that to show products in over X exist given the fibered products exist - it might not be the most convenient for relating between the two

[Adam Topaz]

Gotcha.

[Bhavik Mehta]

For the latter, I think there's something helpful buried deep in the topos project which I can try to dig up, but there ought to be something like this in mathlib

[Adam Topaz]

Ah don't worry about it. I'm writing up some code now.

[Adam Topaz]

Hmm... it looks like wide_pullback_shape.lift and wide_pullback_shape.map are missing?

[Bhavik Mehta]

I wouldn't be surprised! The wide_pullback API is very minimal

[Bhavik Mehta]

The closest thing I could find in the topos project is here but I agree we're probably better off just starting this from scratch

[Adam Topaz]

Oh, actually what I mean by wide_pullback_shape.lift is docs#category_theory.limits.wide_pullback_shape.wide_cospan

[Adam Topaz]

Bah what namespace is this!? :expressionless:

[Bhavik Mehta]

#where :)