aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2026-03-26Add cocartesian structure to category of matricesJacques Comeaux
2026-03-25Use agda-categories definition of split idempotentJacques Comeaux
2026-03-25Add looped wiring diagrams and merge functorJacques Comeaux
2026-03-25Add pull functor from relations to wiring diagramsJacques 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-24Add split idempotentsJacques Comeaux
2026-03-19Add category of matrices over an arbitary rigJacques Comeaux
2026-03-14Add wiring diagram equalitiesJacques Comeaux
2026-03-14Refactor wiring diagramsJacques 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-14Allow square brackets in circuit lang identifiersJacques Comeaux
2026-03-14Refactor systems and add looped systemsJacques Comeaux
2026-03-12Add semiadditive dagger categoriesJacques Comeaux
2026-03-10Add preliminary category of wiring diagramsJacques Comeaux
2026-03-08Add monoidal category of finite relationsJacques Comeaux
2026-01-13Fix modules broken by addition of strong SymMonCatJacques Comeaux
2026-01-13Remove old multisetof constructionJacques Comeaux
2026-01-13Move values moduleJacques Comeaux
2026-01-13Remove old monoidal functorsJacques Comeaux
2026-01-11Construct SM nat trans from Circ to SysJacques Comeaux
2026-01-10Define Sys functor from Nat to SMCsJacques Comeaux
2026-01-10Extend monoidalize functor to commutative monoidsJacques Comeaux
2026-01-07Add SMP to commutative monoids functorJacques 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 sym. mon. cat to sym. mon. preorder functorJacques Comeaux
2026-01-06Add symmetric monoidal primitive preorder categoryJacques Comeaux
2026-01-06Add monoidal cats to monoidal preorders functorJacques Comeaux
2026-01-06Add monoidal primitive preordersJacques 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 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