Limits in wildcats

[Alizter]

We define (co)limits in a wild cat and prove that (co)limits commute with (co)limits. Unfortunately, there are a lot of morphism extensionality assumptions dotted throughout and I am not sure how to avoid them.

Some of these assumptions may not actually be attainable. Take for instance HasMorExt (Fun01 A B). Since the 2-cells are incoherent, will this ever be provable?

[mikeshulman]

Hmm... I would be inclined to say that the incoherence of Fun01 means that this is not even a correct definition of limit.

[Alizter]

@mikeshulman What to do then? :-)

[mikeshulman]

Hmm, okay, I think it is the right definition of limit if J is just a graph, since in that case there is no additional coherence that could even be asked for, and I wouldn't expect there to be problems with morext either. But if J happens to be a category (with some amount of coherence), then the limit over its underlying graph will not in general be a correct definition of the limit over the category. Can you do the whole development never assuming that J is more than a graph?

[Alizter]

I was sorting through some of my old notes and I found the motivation for this. I wanted to have a more mature category theory library for doing some more modern algebraic topology a la topos theory. For example, I have written that I wanted to prove the Eckmann-Hilton splitting for which I needed a notion of descent for which I needed some general facts about limits/colimits in a wildcat. I would like to come back to these ideas eventually, but I don't have the time or the motivation to finish it at the moment. Leaving this here to remind my future self.