Bhavik Mehta

@urkud Thanks for picking this back up - I should justify why I left it. I ended up finding alternative proofs for this which are both more mathematical and more...

I'm reverting this back to WIP - it's probably easier to review as a series of PRs rather than one monolithic one, especially since I keep thinking of things to...

Oh nice! This looks exactly like what we wanted

Another piece of motivation: we have uniqueness of initial segments but no existence!

For `with_id_l`, here's what the type could look like ```lean lemma pullback.with_id_l' {X Y : C} (f : X ⟶ Y) : is_limit (pullback_cone.mk f (𝟙 X) (show f ≫...