agda
Pointwise `Algebra`
NB:
- missing structures/bundles (I got bored)
-
isEquivalencemight already be defined somewhere else, but defined in-place here for the time being
Great feedback, thanks!
Regarding naming, I agree that perhaps Pointwise is suboptimal, apart from 'ordinary' mathematical language having 'pointwise lifting' as an informal-but-always-disambiguable term-of-art...? Besides which, we had previously discussed 'pointwise' constructions under #2351 ...
I had even considered calling this Algebra.Construct.Power{Object}, but thought that the categorical notion might cast more heat than light... but definitely would change if you thought it fitted better?
As for proofs, one thing where I was too lazy was in formulating suitable lifting properties for the concepts in Algebra.Definitions, which would make it easier to reuse in the sequel (and fill in the missing structures/bundles...). Your suggestions might also further streamline those!
PowerObject is worse (i.e. even fewer people will find this.) Somehow (from #2351 ) Copower seems less bad.
Current favourite remains PointwiseLift, though it remains a 'placeholder' in my mind for something even better.
I think this construction is worthwhile to add to the library in some form. Further review to follow at some point.
What was the reasoning for the algebraic structures you're defining? Are you planning to define more?
What was the reasoning for the algebraic structures you're defining? Are you planning to define more?
Two things:
- specifically, I need the pointwise lifting of a monoid in order to define
WreathProduct#2351 - generally, pointwise lifting seems ubiquitous in algebra (esp. of spaces of functions), and we didn't have it, so in the end, yes, I guess we want them 'all' (although not all are 'naturally occurring'... at least, not yet, as @JacquesCarette often points out; but the way our hierarchy is built up, so too should be the corresponding lifted versions...)
PowerObjectis worse (i.e. even fewer people will find this.) Somehow (from #2351 )Copowerseems less bad.
But Copower is Σ while Power is Π, surely?
Current favourite remains
PointwiseLift, though it remains a 'placeholder' in my mind for something even better.
Sticking with Pointwise for now, but have 'improved' the CHANGELOG description for the time being...
Final commit: liftRel now follows Function.Relation.Binary.Setoid.Equality in being implicitly quantified, but ahead of possible merge of #2382 it doesn't make sense (to me at least) to try to import that module directly for reuse...? Not least because it would incur an indirection via Func which I'd rather avoid...
You can have one PR depend on another. There is of course a risk in that scheme.
