aboutsummaryrefslogtreecommitdiff
path: root/Functor/Monoidal/Construction
AgeCommit message (Collapse)Author
2025-11-14Generalize ListOf construction to arbitrary monoidmainJacques Comeaux
2025-11-09Use functional vector in edge definitionJacques Comeaux
2025-11-05Adjust universe levelsJacques Comeaux
2025-11-05Add multiset-of constructionJacques Comeaux
2025-11-05Add list-of construction for monoidal functorsJacques Comeaux
If F is a functor from a cocartesian category into Set, then the functor taking n to List (F n) can be made into a monoidal functor. More generally, Set can be replaced with any monoidal category D that has a free monoid functor Free : D -> Monoids[D]