mathlib3

6669a285 - feat(algebraic_topology/simplicial_object + ...): Add has_limits + has_colimits instances (#6695)

feat(algebraic_topology/simplicial_object + ...): Add has_limits + has_colimits instances (#6695) This PR adds `has_limits` and `has_colimits` instances for the category of simplicial objects (assuming the existence of such an instance for the base category). The category of simplicial sets now has both limits and colimits, and we include a small example of a simplicial set (the circle) constructed as a colimit. This PR also includes the following two components, which were required for the above: 1. A basic API for working with `ulift C` where `C` is a category. This was required to avoid some annoying universe issues in the definitions of `has_colimits` and `has_limits`. 2. A small shim that transports a `has_(co)limit` instance along an equivalence of categories. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>