1lab
1lab copied to clipboard
Refactor proof that conservative functors reflect limits
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.