Documentation

Mathlib.CategoryTheory.Limits.Shapes.Equivalence

Transporting existence of specific limits across equivalences #

For now, we only treat the case of initial and terminal objects, but other special shapes can be added in the future.