In a Rezk type, limits and co/limits are in fact unique up to equality (using identity types). The result for colimits can be formalized right away, but the result for limits depends on issue #178.
In a Rezk type, limits and co/limits are in fact unique up to equality (using identity types).
The result for colimits can be formalized right away, but the result for limits depends on issue #178.