aboutsummaryrefslogtreecommitdiff
path: root/Category
AgeCommit message (Collapse)Author
47 hoursShow category of directed wiring diagrams is monoidalJacques Comeaux
13 daysSimplify wiring diagrams using semiadditive daggerJacques Comeaux
14 daysSimplify semiadditive dagger definitionJacques Comeaux
2026-07-18Define semiadditive categoryJacques Comeaux
2026-07-17Add categories with all binary biproductsJacques Comeaux
2026-07-13Remove use of deprecated nameJacques Comeaux
2026-07-13Add cartesian structure to category of semimodulesJacques Comeaux
2026-07-13Construct Sys functor from wiring diagrams to CatsJacques Comeaux
2026-07-12Derive cartesian from semiadditive daggerJacques Comeaux
2026-07-12Show category of commutative conoids is cartesianJacques Comeaux
2026-07-10Use latest agda-categoriesJacques Comeaux
2026-07-09Fix equivalence of rig homomorphismsJacques Comeaux
2026-07-09Add category of commutative monoidsJacques Comeaux
2026-07-09Add Nat to category of maps of Mat(Bool) functorJacques Comeaux
2026-07-07Update circuit valuesJacques Comeaux
2026-04-30Add monoids / monoid objects in setoids equivalenceJacques Comeaux
2026-04-03Add free functor from rig-matrices to semimodulesJacques Comeaux
2026-04-02Add categories of Rigs, Bisemimodules, and SemimodulesJacques Comeaux
2026-03-25Add looped wiring diagrams and merge functorJacques Comeaux
2026-03-25Add category of maps of a dagger 2-posetJacques Comeaux
2026-03-25Define dagger-2-posetsJacques Comeaux
2026-03-24Add monoidal structure to category of posetsJacques Comeaux
2026-03-24Use new dagger reasoning combinatorJacques Comeaux
2026-03-14Add "idempotent" semiadditive dagger categoriesJacques Comeaux
Semiadditive dagger categories in which the induced commutative monoid on each hom-set is idempotent, or (equivalently), is a join semilattice. I don't know if there is a better name for this concept.
2026-03-12Add semiadditive dagger categoriesJacques Comeaux
2026-01-13Fix modules broken by addition of strong SymMonCatJacques Comeaux
2026-01-10Extend monoidalize functor to commutative monoidsJacques Comeaux
2026-01-07Add monoidal preorders to monoids functorJacques Comeaux
2026-01-07Add strong variants of cats to preorders functorsJacques Comeaux
2026-01-07Differentiate lax and strong monoidal monotonesJacques Comeaux
2026-01-06Add symmetric monoidal primitive preorder categoryJacques Comeaux
2026-01-06Add monoidal cats to monoidal preorders functorJacques Comeaux
2026-01-06Add functors from categories to preorders to setoidsJacques Comeaux
2026-01-05Add 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 category of preordersJacques Comeaux
2026-01-04Update to latest agda-categoriesJacques Comeaux
2025-12-13Transport monoid via base category isomorphismJacques 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-06Rename One propertiesJacques Comeaux
2025-12-06Make setoids monoidal structure opaqueJacques Comeaux
2025-12-04Add opaqueness to cospans and decorated cospansJacques Comeaux
2025-11-05Add category of commutative monoidsJacques Comeaux
2025-10-28Add second level parameter to Setoids SMCJacques Comeaux
2025-10-15Add symmetric monoidal versionsJacques Comeaux
2025-10-15Add monoidal categories for Nat and Nat-opJacques Comeaux
2025-04-23Category of decorated cospans is symmetric monoidalJacques Comeaux