Prove that Cats is complete

[Taneb]

I'm very close but I can't quite get this proof across the line. Help would be very welcome.

[HuStmpHrrr]

we don't have this already? how surprising!

[JacquesCarette]

I have a (surprisingly long) list of simple category theory that's still not in the library. Planning to get back to it this summer.

[Taneb]

I had another go trying to complete this proof, and I got stuck at about the same point. If anyone has any ideas what I'm missing, please do share.

[HuStmpHrrr]

I think there is an easier way than directly work all the details out, as sometimes details could be too overwhelming.

notice that completeness is just the same as having all products (not just finite) and equalizers. This is proved here by myself:

https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Complete/Properties/Construction.agda

now, what's left is just to show Cats have all products and equalizers. Between two, showing all products doesn't sound difficult. I am not able to say much about equalizers just by running it in my head, but I suppose it shouldn't be too horrible if all we need to show is up to isomorphisms.

[nmvdw]

I think there is an easier way than directly work all the details out, as sometimes details could be too overwhelming.

notice that completeness is just the same as having all products (not just finite) and equalizers. This is proved here by myself:

https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Complete/Properties/Construction.agda

now, what's left is just to show Cats have all products and equalizers. Between two, showing all products doesn't sound difficult. I am not able to say much about equalizers just by running it in my head, but I suppose it shouldn't be too horrible if all we need to show is up to isomorphisms.

Since the equalizer diagram is required to commute up to the setoid equality and since the setoid equality in Cats is natural isomorphism, I think that we can construct the equalizer of F, G : C -> D as follows:

• Objects: pairs x : C with an iso F x -> G x
• Morphisms from h_x : F x -> G x to h_y : F y -> G y: f : x -> y such that h_y o F f = G f o h_x

(if we would look at this from a 2-categorical perspective, this would be the isoinserter (https://ncatlab.org/nlab/show/isoinserter)).

[HuStmpHrrr]

I think there is an easier way than directly work all the details out, as sometimes details could be too overwhelming. notice that completeness is just the same as having all products (not just finite) and equalizers. This is proved here by myself: https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Complete/Properties/Construction.agda now, what's left is just to show Cats have all products and equalizers. Between two, showing all products doesn't sound difficult. I am not able to say much about equalizers just by running it in my head, but I suppose it shouldn't be too horrible if all we need to show is up to isomorphisms.

Since the equalizer diagram is required to commute up to the setoid equality and since the setoid equality in Cats is natural isomorphism, I think that we can construct the equalizer of F, G : C -> D as follows:

* Objects: pairs `x : C` with an iso `F x -> G x`

* Morphisms from `h_x : F x -> G x` to `h_y : F y -> G y`: `f : x -> y` such that `h_y o F f = G f o h_x`

(if we would look at this from a 2-categorical perspective, this would be the isoinserter (https://ncatlab.org/nlab/show/isoinserter)).

I think it might be worth trying out the equalizer first, as the morphism part seems a bit brittle.

[Taneb]

@nmvdw

Since the equalizer diagram is required to commute up to the setoid equality and since the setoid equality in Cats is natural isomorphism, I think that we can construct the equalizer of F, G : C -> D as follows:

* Objects: pairs `x : C` with an iso `F x -> G x`

* Morphisms from `h_x : F x -> G x` to `h_y : F y -> G y`: `f : x -> y` such that `h_y o F f = G f o h_x`

(if we would look at this from a 2-categorical perspective, this would be the isoinserter (https://ncatlab.org/nlab/show/isoinserter)).

I tried to define the equalizer with these definitions, and... I got stuck in the same place, proving that the arrows commute in the natural isomorphism. You can see my attempt here

I'm pretty sure that this definition of equalizer leads to something more or less equivalent with my explicit definition of completeness, so it makes sense that I hit the same problem

[HuStmpHrrr]

I haven't run it myself, but I have a feeling that this kind of "set comprehension"-ish operations tend to fail because we are running setoids. it might imply that the comprehension should be a bit more complex to take into account the proof relevant details, or we have missing predicates in our definitions. I hope it is not the latter.

[nmvdw]

@nmvdw

Since the equalizer diagram is required to commute up to the setoid equality and since the setoid equality in Cats is natural isomorphism, I think that we can construct the equalizer of F, G : C -> D as follows:

* Objects: pairs `x : C` with an iso `F x -> G x`

* Morphisms from `h_x : F x -> G x` to `h_y : F y -> G y`: `f : x -> y` such that `h_y o F f = G f o h_x`

(if we would look at this from a 2-categorical perspective, this would be the isoinserter (https://ncatlab.org/nlab/show/isoinserter)).

I tried to define the equalizer with these definitions, and... I got stuck in the same place, proving that the arrows commute in the natural isomorphism. You can see my attempt here

I'm pretty sure that this definition of equalizer leads to something more or less equivalent with my explicit definition of completeness, so it makes sense that I hit the same problem

There are two ways to understand the statement that Cat is complete:

1. The bicategory Cat is complete. 'Equalizers' (more precisely, iso-inserters) are constructed as follows:

   Equalizer of F, G : C1 -> C2
   - Objects: x : C1 with iso F x -> G x
   - Morphisms from f : F x -> G x to g : F y -> G y: pairs h : x -> y such that F x -> F y -> G y and F x -> G x -> G y are equal

   Let's call this one IsoInserter F G. Note that this construction indeed is similar to how you proved completeness, since every object came with an isomorphism.

2. The category StrictCat is complete. Equalizers are constructed as follows:

   Equalizer of F, G : C1 -> C2
   - Objects: x : C1 such that F x = G x
   - Morphisms: f : x1 -> x2 such that F f = G f

   Let's call this one Equalizer F G. Note that the definition of Equalizer F G speaks about equality of objects.

In mathematical books on category theory, one uses set-theoretic foundations. In that case, the statement Cat is a complete category usually refers to the second of these two variants.

However, the category of categories in Agda-categories is a bit different than the aforementioned StrictCat. In StrictCat, one considers functors up to equality, while Agda-categories considers functors up to natural isomorphism. For that reason, Equalizer F G is too strict to be the equalizer.

In addition, IsoInserter F G satisfies a 2-categorical universal property rather than a 1-categorical universal property. For that property, uniqueness follows under stronger assumptions: the additional assumption being precisely the equality that you are missing in the construction.

For that reason, neither construction gives equalizer in Cats, and I think the current definition of Cat actually might not give rise a complete category. There are two possible fixes:

1. Study at the bicategory of categories instead. In that case, IsoInserter F G would work well.
2. Change the setoid relation on morphisms in Cats (functors up to equality), and then one could use Equalizer F G.