agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard

Published 20 hours ago • verified publisher icon agda

Should Modules have raw bundles?

Open Taneb opened this issue 3 years ago • 0 comments

Currently, for each bundle defined in Algebra.Bundles, there is a corresponding raw bundle, consisting of the operations but without the laws. The same is not true for Algebra.Module.Bundles. Should they be added?

Taneb avatar Sep 20 '22 06:09 Taneb