diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-05 00:09:51 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-05 00:09:51 -0600 |
| commit | e70481cf98eeb00154536e364dec58e79b034cc5 (patch) | |
| tree | c1e160bce301723c1a91044ea706266bb795b4cb /Data/Setoid.agda | |
| parent | 10df4f9f7a64a24c2c74731f9dc49e2d6f008b18 (diff) | |
Add list-of construction for monoidal functors
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]
Diffstat (limited to 'Data/Setoid.agda')
0 files changed, 0 insertions, 0 deletions