Commit 2020-04-18 23:47 d76a882d

feat(category_theory/limits/over): over category has connected limits (#2438) Show that the forgetful functor from the over category creates connected limits. The key consequence of this is that the over category has equalizers, which we will use to show that it has all (finite) limits if the base category does. I've also moved the connected category examples into category_theory/connected.lean. Also I removed the proof of instance {B : C} [has_pullbacks.{v} C] : has_pullbacks.{v} (over B) which I wrote and semorrison massively improved, as the new instances generalise it. I also added a reassoc for is_limit.fac, which simplified one of the proofs I had.