Reed Mullanix

(Co)Limit Reasoning Module

1

It would be nice to have a good API for reasoning about (Co)Limits, much like we have with `Cat.Reasoning` and `Cat.Functor.Reasoning`.

Right now, we have proofs that conservative functors reflect all limits that they preserve, but using this result is a bit annoying as we have to mediate between concrete (co)limits...

In [Cat.Functor.Adjoint.Continuous](https://github.com/plt-amy/1lab/blob/main/src/Cat/Functor/Adjoint/Continuous.lagda.md) we show that left adjoints preserve colimits generally, but don't show that they preserve _specific_ colimits (coproducts, coequalisers, etc). This should be pretty mechanical, and any prospective implementor...

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](https://github.com/plt-amy/1lab/blob/main/src/Cat/Functor/Conservative.lagda.md#L53)). This can...

## Issue Description More or less what the title suggests! This should be pretty easy/mindless, so it would be a good beginner issue. See [this](https://github.com/plt-amy/1lab/blob/main/src/Cat/Diagram/Limit/Pullback.lagda.md) for what it looks like...

## Patch Description This is a little PR that adds a `#debug` directive that toggles the debug mode on and off via `#debug on` and `#debug off`.

## Patch Description This PR adds a first-class notion of telescope, and unifies ## Motivation Right now, we have some Cool tricks for records; namely record patches [#274] and total...

[🚫 🐞] Improved Debugging Output

1

It would be nice to improve the `Debug.print` output a bit, and implement a `#debug` directive (I thought I had done this, but apparently not??)