search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Add Cartesian multicategories #290

Closed laMudri closed 8 months ago

laMudri commented 3 years ago

While general multicategories have proved to be a pain to implement, Cartesian multicategories are easy. We can carry over techniques from simply typed λ-calculus, in particular simultaneous substitution. Indeed, the contents of this pull request give the machinery to derive the category of contexts and substitutions from some basic properties of the actions of substitutions.

Things left to do (along with general cleaning up and responding to comments):

JacquesCarette commented 3 years ago

That's looking really great! Is this still WIP, or is it ready to go?

laMudri commented 3 years ago

I'd like to at least give it a once-over. Do you have any opinions on the things that should be in stdlib rather than here, and getting versions synced up, &c? (Funnily enough, this kind of problem has been a topic in the SPLS pub.)

laMudri commented 3 years ago

Also, I think we should eventually axiomatise all of the required properties about List and _∈_. The only challenge I see there is what to do about prod, ⟨_⟩Π, and π[_], but maybe the literature has an answer (or we just axiomatise everything as-is).

laMudri commented 3 years ago

I suppose I'll need to rebase at some point to turn Structure into Bundle.

JacquesCarette commented 3 years ago

Yes please!

JacquesCarette commented 2 years ago

@laMudri I'm looking back at this now: can you tell me what you think the status is, in your opinion?

laMudri commented 2 years ago

Thanks for the reminder. agda/agda-stdlib#1756 should now be ready, so after that gets merged I should be able to delete those parts from this PR.

JacquesCarette commented 8 months ago

I have a few cycles right now - what can I do to help push this through to completion?

laMudri commented 8 months ago

I think moving the properties about list membership and appending over to stdlib (if they're not there already by now) was the main thing that needed doing.

JacquesCarette commented 8 months ago

I have access to your repo, so I should be able to do this.

JacquesCarette commented 8 months ago

I've pulled it in to a branch so that I can work on it more easily.