aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
13 hoursUpdate system functormainJacques Comeaux
20 hoursAdd braiding to wiring diagram monoidal structureJacques Comeaux
42 hoursUpdate missed module to new agda-categoriesJacques Comeaux
42 hoursShow category of directed wiring diagrams is monoidalJacques Comeaux
13 daysSimplify wiring diagrams using semiadditive daggerJacques Comeaux
14 daysSimplify semiadditive dagger definitionJacques Comeaux
14 daysDefine semiadditive categoryJacques Comeaux
2026-07-17Add categories with all binary biproductsJacques Comeaux
2026-07-13Add split functorJacques 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-11Add boolean latticeJacques Comeaux
2026-07-10Use latest agda-categoriesJacques Comeaux
2026-07-09Generalize systems to (co)commutative (co)monoidsJacques Comeaux
2026-07-09Add semimodules to commutative monoids functorJacques Comeaux
2026-07-09Include missing propertiesJacques 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-08Add functional matricesJacques Comeaux
2026-07-07Update circuit valuesJacques Comeaux
2026-07-07Update circuit typecheckerJacques Comeaux
2026-07-07Update matrices and vectorsJacques Comeaux
2026-04-30Add monoids / monoid objects in setoids equivalenceJacques Comeaux
2026-04-29Simplify construction of matrix endofunctorJacques Comeaux
2026-04-29Add endofunctor for matrices of fixed sizeJacques Comeaux
2026-04-28Add endofunctor for Vectors of fixed lengthJacques Comeaux
2026-04-27Add bounded distributive latticesJacques Comeaux
2026-04-03Add free functor from rig-matrices to semimodulesJacques Comeaux
2026-04-02Add categories of Rigs, Bisemimodules, and SemimodulesJacques Comeaux
2026-04-02Reorganize matrix codeJacques Comeaux
2026-03-29Add semimodule of vectors over a commutative rigJacques Comeaux
2026-03-29Add bisemimodule of vectors over a rigJacques Comeaux
2026-03-28Begin separating vector concepts from matricesJacques Comeaux
2026-03-27Build dagger 2-poset Mat(R) for idem. comm. rig RJacques Comeaux
2026-03-27Add commutative rig matrix semiadditive structureJacques Comeaux
2026-03-27Add dagger structure for commutative rig matricesJacques Comeaux
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