Jacques Carette
Jacques Carette
That's looking really great! Is this still WIP, or is it ready to go?
Yes please!
@laMudri I'm looking back at this now: can you tell me what you think the status is, in your opinion?
(Sorry for the slowness, my term was crazy. Slowly emerging now.) Comparing with monoidal functor, I think that `^-homo` would perhaps be an even better name?
Indeed, could you be more precise @Taneb ? `IndexedProduct` is used successfully in proving things around completeness of categories. Yes, it's a very strong assumption, but assuming "all" products is...
We do want the word `Pretopos` to show up. So maybe indeed the longer form is a good idea. In a radical redo of CT, I'd agree that monads and...
I'm kind of warming up to `Agda`. The next question: should we have both `Agda` and `PointwiseAgda` (or a variant thereof)? Sergey Goncharov (@sergey-goncharov) points out that the equality of...
The "each is now a one-liner" is absolutely beautiful! What @Taneb refers to is that I have been reluctant to put too many examples in agda-categories itself. Some examples make...
I'm definitely a taker for helping with this. I'm actively working on related ideas, so that wouldn't be a distraction from what I'm doing (which definitely helps with time allocation)....
Many, many months later, I'm finally able to work on this again. Are you still interested @conal ?