Making Over.pullback computable

Stream: mathlib4

[Sina Hazratpour]

In #31033 I am making Over.pullback computable (at least not noncomputable). This is part of (re)developing the theory of locally cartesian closed categories (LCCCs) (see old #22340), using ChosenPullback.pullback instead of already existing Over.pullback.

Over.pullback defined in Comma.Over.Pullback uses pullback and the limit API which uses choice, hence noncomputable.

One advantage gained by building LCCCs on ChosenPullback.pullback instead is that in the category of types we have ChosenPullbacks, and indeed we get good defeq properties:

example : pullbackObj (C:= Type u) f g = Types.PullbackObj f g := rfl

example : ChosenPullbacks.fst (C:= Type u) g f = fun p => p.1.1 := by rfl

example : ChosenPullbacks.snd (C:= Type u) g f = fun p => p.1.2 := by rfl

etc. Moreover right adjoint to ChosenPullback.pullback (namely the pushforward functor) is then computed by Π, i.e. the dependent function type.

Here comes the question:

In developing LCCCs I need toOver (I : C) : C ⥤ Over I which is the computable version of already existingOver.star and also toOverUnit : C ⥤ Over (𝟙_ C). These are defined in #30373 but assuming a CartesianMonoidalCategory structure on C. They can be defined more generally though: toOver uses only ChosenBinaryProduct and toOverUnit could be written in a way to use only ChosenTerminal.

But afaik we don't have ChosenBinaryProduct and ChosenTerminal. Is it worth adding them to mathlib?

Hope to hear from @Kim Morrison @Joël Riou @Robin Carlier @Yaël Dillies and anyone else who has an opinion on this.

[Andrew Yang]

I am slightly concerned if this is the right direction or if this will lead to large API duplication.

[Sina Hazratpour]

@Andrew Yang
I should have mentioned that we had a bit of discussion on this with @Johan Commelin and @Joël Riou about this direction. See #21525

In the beginning that was my sense too, but so far it has not been too bad. However, with adding ChosenBinaryProduct and ChosenTerminal this might indeed create a lot of duplicates, thought I am curious to hear what others think. The idea of needing ChosenTerminal has also come up in our HoTTLean downstream project.

[Robin Carlier]

I think the choice was made to have Cartesian monoidal categories be the preferred spelling of ChosenBinaryProduct + ChosenTerminal.
I'm kind of worried that if we were to introduce these and spell things using them we'd end up with possible "multiple spellings" of e.g products (either the monoidal spelling, and the other), and then losing the advantage of monoidal notations (e.g coherence) when both a chosen binary and terminal are present (and for the same reason that motivated the move from ChosenFiniteProducts to CartesianMonoidalCategory, we don't want auto instances "chosen binary products and terminal -> Cartesian monoidal" here I think?)

[Chris Henson]

^I had the same thought, how does what you envision for ChosenBinaryProduct compare to the now deprecated ChosenFiniteProducts?

[Andrew Yang]

See #21525

Would you mind giving a more precise link? I cannot find the relevant discussion.

[Sina Hazratpour]

@Chris Henson
ChosenFiniteProducts is the same as ChosenBinaryProduct + ChosenTerminal however sometimes you want one summand only because that is the weaker assumption.

[Sina Hazratpour]

Andrew Yang said:

See #21525

Would you mind giving a more precise link? I cannot find the relevant discussion.

Maybe @Joël Riou can provide more context about his discussion with @Johan Commelin about this. I'm also curious what are his motivations. My motivation is explained in above (i.e. in types we know what pullbacks are exactly and the LCCC constructs when specialized to Types should match definitionally to dependent sum and function types.)

[Sina Hazratpour]

Robin Carlier said:

I think the choice was made to have Cartesian monoidal categories be the preferred spelling of ChosenBinaryProduct + ChosenTerminal.
I'm kind of worried that if we were to introduce these and spell things using them we'd end up with possible "multiple spellings" of e.g products (either the monoidal spelling, and the other), and then losing the advantage of monoidal notations (e.g coherence) when both a chosen binary and terminal are present (and for the same reason that motivated the move from ChosenFiniteProducts to CartesianMonoidalCategory, we don't want auto instances "chosen binary products and terminal -> Cartesian monoidal" here I think?)

That was also my sense and that is why so far I opted for CartesianMonoidalCategory instead of the weaker assumptions ChosenBinaryProduct for defining toOver (I : C) : C ⥤ Over I. But I was wondering if there could be other workarounds.

[Chris Henson]

Sina Hazratpour said:

Chris Henson
ChosenFiniteProducts is the same as ChosenBinaryProduct + ChosenTerminal however sometimes you want one summand only because that is the weaker assumption.

I'm not sure of the broader impact, but I agree this is sometimes useful.

[Andrew Yang]

Without seeing the discussions my first questions would be

1. Is the defeq really that useful? In the end you still wouldn't be able to make them reducibly equal so that rw still wouldn't work etc and you will still need to build API on top of it. And regardless of the defeq you can always write the recursor ((x : X) -> (y : Y) -> (h : f x = g y) -> P) -> (pullback f g -> P) and it usually doesn't matter if this recursor comes from inductive types or not.
2. If we were to adopt this, to what extent are you duplicating the Mathlib/CategoryTheory/Limits/Shapes/Pullback folder?

[Sina Hazratpour]

@Andrew Yang My sense is that for LCCCs basically what is in #31033 which is to say not much. Once you obtain the adjunction, you basically use mate stuff so you don't need to work with actual pullbacks that much. I needed to prove ChosenPullback yields a IsPullback so that i could actually prove existence of pushforwards implies slices are cartesian closed (i.e. local cartesian closure). But most of the theory of LCCCs goes thru pull-push adjunction not thru API of pullbacks.

[Adam Topaz]

I think we have seen that chosen finite products are quite useful in practice. I think having a ChosenPullbacks class would be similarly useful.

[Sina Hazratpour]

@Adam Topaz And my question of this thread was basically could having ChosenBinaryProduct be also useful, or not worth the tradeoff?

For instance the category of topological spaces and local homeomorphisms does not have a terminal object but has (chosen) binary product so it is not monoidal cartesian but you could define the functor I care about

def toOver (I : C) : C ⥤ Over I where
  obj X := Over.mk <| CartesianMonoidalCategory.snd X I
  map {X Y} f := Over.homMk (f ▷ I)

[Adam Topaz]

Maybe we should go all the way and make ChosenLimitsOfShape?

[Christian Merten]

And then you duplicate all of the limits API?

[Adam Topaz]

It wont be too much duplication, just a thin wrapper around the existing cones and IsLimit

[Adam Topaz]

Aside: ive been thinking a lot about categorical logic recently, and having categorical constructions be computable would be genuinely useful since it would allow you to actually “program” with categories.

[Christian Merten]

But to make this ergonomic, I would expect you would want to have analogs of docs#Limits.prod.fst, docs#Limits.prod.lift etc. for every standard shape.

[Chris Henson]

Adam Topaz said:

Aside: ive been thinking a lot about categorical logic recently, and having categorical constructions be computable would be genuinely useful since it would allow you to actually “program” with categories.

This is close to what I had in mind as well. For say categorical semantics of lambda calculi, we sometimes care about terminal objects and products separately, and it would be nice to be able to specifically and computably specify this.

[Ruben Van de Velde]

Sina Hazratpour said:

In #31033 I am making Over.pullback computable (at least not noncomputable).

Maybe I'm reading too quickly, but I haven't seen an actual motivation behind this

[Joël Riou]

Ruben Van de Velde said:

Sina Hazratpour said:

In #31033 I am making Over.pullback computable (at least not noncomputable).

Maybe I'm reading too quickly, but I haven't seen an actual motivation behind this

Having chosen finite products is extremely useful. Without this, I would certainly not have been able to formalize the homotopy theory of simplicial sets (and having chosen pullbacks may have helped a little bit also). Similarly, we have quite explicit constructions of "chosen" pullbacks in certain categories, and using an explicit "Over.pullback" functor would make it easier to prove things (for example, in #28908, I had to transport an adjunction via an isomorphism, which would be unnecessary using ChosenPullbacks).
Similarly, in monoidal closed categories, the internal hom is a data: it does not have to be the right adjoint which is given by using AC.

[Joël Riou]

I am not sure there is a need for ChosenTerminal (why not use a IsTerminal X variable at all times in such situations?). For ChosenBinaryProduct, if significant results really need this, this could be considered, but it seems difficult to keep the monoidal notations (which is part of the very nice recent CartesianMonoidalCategory refactor) as @Robin Carlier pointed it out.
I am not convinced about ChosenLimitsOfShape because part of what the chosen finite products API facilitates is the packaging/unpackaging of binary fans into pairs of objects.

[joseph hua]

Joël Riou said:

I am not sure there is a need for ChosenTerminal (why not use a IsTerminal X variable at all times in such situations?). For ChosenBinaryProduct, if significant results really need this, this could be considered, but it seems difficult to keep the monoidal notations (which is part of the very nice recent CartesianMonoidalCategory refactor) as Robin Carlier pointed it out.
I am not convinced about ChosenLimitsOfShape because part of what the chosen finite products API facilitates is the packaging/unpackaging of binary fans into pairs of objects.

If I want to say that an object X : Grpd is fibrant, meaning the unique map to the terminal groupoid is an isofibration, I wouldn't want that definition to have a variable T : Grpd satisfying hT : IsTerminal T. I think it is reasonable to ask for the unique map to a chosen terminal object to be an isofibration

[Joël Riou]

This is a situation where we should use the terminal object from the limits API (using AC) , and the isofibrations API should allow the user to specify their preferred terminal object (see https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.html)
For example, in the category of simplicial sets, there are three reasonable terminal objects : ⊥_ SSet, 𝟙_ SSet and Δ[0].

[Bhavik Mehta]

Sina Hazratpour said:

In #31033 I am making Over.pullback computable (at least not noncomputable).

I'm completely in favour of this change: Over.pullback was intended to be computable from the start, and one of the main reasons I objected to computable pullbacks being removed was precisely for formalising LCCCs.

[Edward van de Meent]

out of curiosity, what kind of considerations did you have when designing the ChosenPullback class? Did you consider having it be a class which takes two morphisms as arguments, and contains the data of IsLimit (PullbackCone.mk _ _ _)? (since this would make it possible to have more control over what pullbacks do/don't have a computable/chosen representation)

[Edward van de Meent]

as is, maybe a better name would be ChosenPullbacksAlong?

[Joël Riou]

We have a general limits API which allow to construct certain (computable or not) co(cones) and IsLimit/IsColimit structures. For pullbacks, we have PullbackCone (and the noncomputable IsPullback).
But, I agree that ChosenPullbacksAlong would be a better name (@Sina Hazratpour: could you make the change?).

[Sina Hazratpour]

I am actually not a fan of ChosenPullbacksAlong; ChosenPullback f says we have a _choice_ of _pullback_ for very morphism g with the same codomain as f, hence ChosenPullback. To me, ChosenPullbackAlong sounds more like the category C has chosen pullbacks along f. But ChosenPullback is not so much the property/structure of the category but the property/structure of f itself. Also, ChosenPullback is shorter.

[Joël Riou]

This is to parallel HasPullbacksAlong.

[Sina Hazratpour]

Even for HasPullback, I would argue HasPullback f is the correct naming, and it should mean \all g, HasPullback f g which is compatible with viewing HasPullback as a two-variable function to Prop.

[Joël Riou]

We are not going to change HasPullback.

[Edward van de Meent]

Sina Hazratpour said:

ChosenPullback f says we have a _choice_ of _pullback_ for very morphism g with the same codomain as f, hence ChosenPullback. To me, ChosenPullbackAlong sounds more like the category C has chosen pullbacks along f.

You seem to be arguing that there is a difference in meaning between the names... However, to me these descriptions seem like the same thing? A pullback of g along f is precisely the right/left (i forget which one) projection from the pullback of f and g, no? So if you say for every g, we choose a pullback of f and g, you choose all pullbacks along f?