aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
12 daysAdd monoidal preorders to monoids functorJacques Comeaux
12 daysAdd strong variants of cats to preorders functorsJacques Comeaux
12 daysDifferentiate lax and strong monoidal monotonesJacques Comeaux
13 daysAdd sym. mon. cat to sym. mon. preorder functorJacques Comeaux
13 daysAdd symmetric monoidal primitive preorder categoryJacques Comeaux
13 daysAdd monoidal cats to monoidal preorders functorJacques Comeaux
13 daysAdd monoidal primitive preordersJacques Comeaux
13 daysAdd functors from categories to preorders to setoidsJacques Comeaux
13 daysAdd non-setoid-based preordersJacques Comeaux
2026-01-04Add category of symmetric monoidal preordersJacques Comeaux
2026-01-04Add category of monoidal preordersJacques Comeaux
2026-01-04Add monoidal monotone maps between preordersJacques Comeaux
2026-01-04Add (weak) monoidal and symmetric monoidal preordersJacques Comeaux
2026-01-04Add category of preordersJacques Comeaux
2026-01-04Update to latest agda-categoriesJacques Comeaux
2026-01-01Update push, pull, and sys functorsJacques Comeaux
2025-12-13Add hypergraph destructor setoid homomorphismJacques Comeaux
2025-12-13Add Monoidalize functorJacques Comeaux
2025-12-13Redefine circuit functorJacques Comeaux
2025-12-13Transport monoid via base category isomorphismJacques Comeaux
2025-12-10Add free/forget multiset adjunctionJacques Comeaux
2025-12-09Add free commutative monoid functorJacques Comeaux
2025-12-09Update Nat propertiesJacques Comeaux
2025-12-09Add shorter name for singleton setoidJacques Comeaux
2025-12-08Update category of cospans monoidal structureJacques Comeaux
2025-12-08Update category of cospansJacques Comeaux
2025-12-06Update free and forgetful monoid functorsJacques Comeaux
2025-12-06Rename One propertiesJacques Comeaux
2025-12-06Update list adjunction for opaquenessJacques Comeaux
2025-12-06Move FinMerge utilitesJacques Comeaux
2025-12-06Add commutative monoid conversionsJacques Comeaux
2025-12-06Make setoids monoidal structure opaqueJacques Comeaux
2025-12-04Add opaqueness to cospans and decorated cospansJacques Comeaux
2025-11-14Generalize ListOf construction to arbitrary monoidJacques Comeaux
2025-11-13Add adjunction between free monoid and forgetJacques Comeaux
2025-11-09Use functional vector in edge definitionJacques Comeaux
2025-11-09Clean up System functorsJacques Comeaux
2025-11-05Add Circ symmetric monoidal functorJacques Comeaux
2025-11-05Adjust universe levelsJacques Comeaux
2025-11-05Add multiset functorJacques Comeaux
2025-11-05Add free commutaive monoid functorJacques Comeaux
2025-11-05Add multiset-of constructionJacques Comeaux
2025-11-05Add category of commutative monoidsJacques 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]
2025-11-03Remove unnecessary importJacques Comeaux
2025-11-03Use permutation for equivalence of hypergraphsJacques Comeaux
2025-10-30Add Circ functorJacques Comeaux
2025-10-30Add free functor from setoids to monoids in setoidsJacques Comeaux
2025-10-30Make list natural transformations level-polymorphicJacques Comeaux
2025-10-30Add empty list and append natural transformationsJacques Comeaux
generated by cgit v1.2.3 (git 2.39.1) at 2026-01-19 07:15:20 +0000