1lab icon indicating copy to clipboard operation
1lab copied to clipboard

Refactor proof that conservative functors reflect limits

Open TOTBWF opened this issue 3 years ago • 0 comments

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.

TOTBWF avatar May 16 '22 19:05 TOTBWF