Commit 2021-03-16 06:30 6669a285

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.