Refactor proof that conservative functors reflect limits #77
Labels
bug
Something isn't working
category-theory
For issues/pull requests relating to the Cat.* namespace
The proof that conservative functors reflect limits that they preserves is quite short and elegant, but unfortunately this comes at the cost of requiring a
subst
(See here). This can cause issues later down the line, as the limits we get out of it won't quite line up with the ones we want. Luckily, the direct proof isn't so bad, so we should probably just do that. See #76 for what that might look like.The text was updated successfully, but these errors were encountered: