has_* limit classes

Stream: maths

[Reid Barton]

We now have a whole slew of limit-related classes beyond has_limit, has_limits_of_shape and has_limits, namely
has_terminal, has_binary_products, has_finite_products, has_products, has_equalizers, has_pullbacks, has_finite_limits.
What is the plan for making instances of all these classes?

[Reid Barton]

For example, here is a concrete question. In Top the binary product is given by the usual product of spaces, whose underlying type is the product of the underlying types. Should that be how has_binary_products Top is defined?

[Reid Barton]

Or should it agree with the product which comes from has_limits, which will be of the form a subtype of a Pi type, and will definitely not be equal (at least not provably equal) to X × Y?

[Reid Barton]

I tried looking at other category theory libraries, namely the Lean 2 HoTT library and UniMath, although they may have different concerns than we do.
In the Lean 2 HoTT library, has_binary_products is simply defined to be (reducibly) has_limits_of_shape for a particular shape category (just two objects and no nonidentity morphisms). That is one extreme option. However, using a class that is reducible doesn't seem to work very well in Lean 3 (based on comments in that file, it might not have worked very well in Lean 2 either).
UniMath has two (or sometimes even more) definitions of each of these special types of limits, one defined generically as a limit and one which is direct, and prove their equivalence. They're not afraid to write a lot of stuff! On the other hand they don't use type classes at all, so they don't have the question of which of these relationships to make into instances.

[Reid Barton]

Trying to define an instance has_binary_products Top by hand, I'm quickly led to the conclusion that one ought to define a specialized is_binary_product (like UniMath does) and then prove its equivalence to the general limit concept.

[Reid Barton]

Actually it's surprisingly awkward even to prove that anything has binary products

[Reid Barton]

That is, other than by some general limit construction. If you really want to make use of the fact that you're defining a binary product.

[Scott Morrison]

So I guess two questions are:

[Scott Morrison]

1) How often can you construct binary products but not general limits? What are some good examples?

[Scott Morrison]

2) How often to you want to know that your "categorical" binary product is actually the "native" binary product, rather than just something satisfying the categorical binary product API?

[Scott Morrison]

If either of those is "often", then yes, we need a specialized is_binary_product and all its relatives.

[Scott Morrison]

This is not particularly hard or onerous to do, and I'm not too worried about the API surface area growing too large just because of this.

[Scott Morrison]

I do think it will have a slightly dangerous effect --- we'll see people defining instances of has_binary_product not because they actually needed a tight connection with a "native" binary product, but just because they didn't think hard enough about constructing more general shapes.

[Scott Morrison]

(I think, Reid, you saw me doing exactly this for both Type and Top during my initial experimentation. :-)

[Reid Barton]

1) How often can you construct binary products but not general limits? What are some good examples?

I found it difficult to come up with one which is really compelling and feasible to add to mathlib, but here are some examples:
Schemes (only finite limits, and it seems you have to build them out of pullbacks). Manifolds (but they don't care about category theory). The category of sets and relations is a simple one, it has products (which are disjoint unions) but not equalizers. Suitable subcategories of nice categories, e.g., Kan complexes. Lawvere theories (e.g., the opposite of the category of free groups) have finite products and generally not other limits.

[Reid Barton]

2) How often to you want to know that your "categorical" binary product is actually the "native" binary product, rather than just something satisfying the categorical binary product API?

This I think is a lot more common. For example, in lean-homotopy-theory I need the fact that the functor $X \times -$ on topological spaces preserves pushouts when $X$ is locally compact. (In particular, when $X = I = [0, 1]$; that lets me define a homotopy between maps on a pushout by gluing homotopies together.) The proof is that $X \times -$ is left adjoint to $C(X, -)$ with the compact-open topology. The "math part" of that is here and it uses the fact that we're really talking about the product space, using is_open_prod and so on.

[Reid Barton]

Now technically for my purposes it doesn't matter that the cylinder functor $I \times -$ is actually a categorical product, so I don't bother to formalize products. But if we're going to have notation for the categorical product on Top, it seems rather convenient for it to be the actual product defined using prod.

[Reid Barton]

For example, suppose we define a cartesian closed category and then we want to prove Type is one

[Reid Barton]

Presumably the first thing you would have to do is show that the crazy subtype-of-a-Pi-type definition of the product is isomorphic to prod

[Reid Barton]

Which is not specific to proving cartesian closedness, so you'd want to record that fact somewhere