aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2026-08-15Add monoidal structure to system functorJacques Comeaux
2026-08-13Show free semimodule functor is cartesianJacques Comeaux
2026-08-05Show matrix change of base functor is cartesianJacques Comeaux
2026-08-05Show semimodules forgetful functor is cartesianJacques Comeaux
2026-08-05Finish merge and split symmetric monoidal functorsJacques Comeaux
2026-08-04Construct monoidal merge functorJacques Comeaux
2026-08-03Show category of maps is monoidalJacques Comeaux
2026-08-01Upgrade Push + Pull to symmetric monoidal functorsJacques Comeaux
2026-07-31Show wiring diagram braiding is symmetricJacques Comeaux
2026-07-31Update system functorJacques Comeaux
2026-07-31Add braiding to wiring diagram monoidal structureJacques Comeaux
2026-07-30Update missed module to new agda-categoriesJacques Comeaux
2026-07-30Show category of directed wiring diagrams is monoidalJacques Comeaux
2026-07-19Simplify wiring diagrams using semiadditive daggerJacques Comeaux
2026-07-18Simplify semiadditive dagger definitionJacques Comeaux
2026-07-18Define 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