search

agda / agda-categories

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

μ-Bialgebras #362

Closed cxandru closed 1 year ago

cxandru commented 1 year ago

I've defined bialgebras for functors. I needed to factor out some definitions in Algebra and Coalgebra, but the changes don't break any existing code. For more details see the commit message of f8a60272a3aff9284cac5a481dab91da932727ea

Taneb commented 1 year ago

We don't currently have any modules with a non-ascii character in the name. Is it OK to add one in this case?

JacquesCarette commented 1 year ago

Good point. I think that's asking for trouble, we shouldn't have file names with unicode in them. Internal modules is fine, but not "file-modules".

cxandru commented 1 year ago

This is looking really good. Is it "ready"?

Almost! I'm currently implementing a final interesting lemma, that initial objects in T-Algs induce initial objs in μ-F-T-Bialgebras (dually, final F-Coalgs are also final in μ-F-T-Bialgebras). I also replied to some of your review comments with questions

JacquesCarette commented 1 year ago

(link to personal Trello board deleted - it was misconfigured, and wasn't supposed to post on here)

cxandru commented 1 year ago

I added some last nice things to round off this MR (see commit descriptions). After review everything should be ready to merge!

JacquesCarette commented 1 year ago

Thanks - at POPL right now, so might not get to do the review until I'm back home. We'll see.

cxandru commented 1 year ago

Thanks - at POPL right now, so might not get to do the review until I'm back home. We'll see.

yes, I saw on Mastodon. No rush!