search

pufferffish / agda-symmetries

MIT License
5 stars 1 forks source link

More constructions of free commutative monoids #56

Closed pufferffish closed 1 year ago

pufferffish commented 1 year ago

Close #54

vikraman commented 1 year ago

This PList looks good to me, might be worth doing another version with the comm relation.

This makes me think if you can abstract out both permutation relations, and define PList for an arbitrary relation with the properties that you need to prove freeness. The harder thing to prove would be, PList is free iff the permutation relation satisfies these properties.

pufferffish commented 1 year ago

This PList looks good to me, might be worth doing another version with the comm relation.

This makes me think if you can abstract out both permutation relations, and define PList for an arbitrary relation with the properties that you need to prove freeness. The harder thing to prove would be, PList is free iff the permutation relation satisfies these properties.

This should be doable, I'll give it a try after I'm done with the analytic functor definition

pufferffish commented 1 year ago

Found out Free's type levels are wrong (some type levels that should've been different were the same) while working on QFreeMon, might worth taking a look