# Commit 2020-04-18 23:47 d76a882d

View on Github →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.