Commit 2020-06-25 15:51 c6f629bc

feat(category_theory/limits): isos from reindexing limits (#3100) Three related constructions which are helpful when identifying "the same limit written different ways".

1. The categories of cones over F and G are equivalent if F and G are naturally isomorphic (possibly after changing the indexing category by an equivalence).
2. We can prove two cone points (s : cone F).X and (t.cone F).X are isomorphic if

• both cones are limit cones
• their indexing categories are equivalent via some e : J ≌ K,
• the triangle of functors commutes up to a natural isomorphism: e.functor ⋙ G ≅ F.

3. The chosen limits of F : J ⥤ C and G : K ⥤ C are isomorphic, if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.