# Zulip Chat Archive

## Stream: maths

### Topic: has_* limit classes

#### Reid Barton (Sep 06 2019 at 15:32):

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 (Sep 06 2019 at 15:33):

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 (Sep 06 2019 at 15:35):

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 (Sep 06 2019 at 17:13):

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 (Sep 06 2019 at 17:14):

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 (Sep 06 2019 at 18:48):

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

#### Reid Barton (Sep 06 2019 at 18:49):

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 (Sep 06 2019 at 23:37):

So I guess two questions are:

#### Scott Morrison (Sep 06 2019 at 23:38):

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

#### Scott Morrison (Sep 06 2019 at 23:38):

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 (Sep 06 2019 at 23:39):

If either of those is "often", then yes, we need a specialized `is_binary_product`

and all its relatives.

#### Scott Morrison (Sep 06 2019 at 23:39):

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 (Sep 06 2019 at 23:40):

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 (Sep 06 2019 at 23:41):

(I think, Reid, you saw me doing exactly this for both `Type`

and `Top`

during my initial experimentation. :-)

#### Reid Barton (Sep 07 2019 at 12:16):

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 (Sep 07 2019 at 12:21):

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 (Sep 07 2019 at 12:25):

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 (Sep 07 2019 at 12:26):

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

#### Reid Barton (Sep 07 2019 at 12:29):

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 (Sep 07 2019 at 13:15):

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

Last updated: May 12 2021 at 08:14 UTC