aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
10 daysMove FinMerge utilitesJacques Comeaux
10 daysAdd commutative monoid conversionsJacques Comeaux
10 daysMake setoids monoidal structure opaqueJacques Comeaux
12 daysAdd 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
2025-10-29Add Edge functorJacques Comeaux
2025-10-29Add List functorJacques Comeaux
2025-10-29Update hypergraph equivalenceJacques Comeaux
2025-10-29Add Circuit typeJacques Comeaux
2025-10-29Refactor list-based hypergraphsJacques Comeaux
2025-10-28Add second level parameter to Setoids SMCJacques Comeaux
2025-10-28Merge branch 'hypergraph-conversion'Jacques Comeaux
2025-10-28Split System into smaller modulesJacques Comeaux
2025-10-28Add symmetric monoidal structure to Pull and SystemJacques Comeaux
2025-10-27Add inverted unitary rules for strong monoidal functorsJacques Comeaux
2025-10-26Add inverted associativity for strong monoidal functorsJacques Comeaux
2025-10-22Simplify System definition and add System functorJacques Comeaux
2025-10-22Setoid-ify System definitionJacques Comeaux
2025-10-22Add symmetric monoidal structure to Push functorJacques Comeaux
2025-10-16Add Preimage symmetric monoidal functorJacques Comeaux
2025-10-15Improve terminology in commentJacques Comeaux
2025-10-15Add symmetric monoidal versionsJacques Comeaux
2025-10-15Add monoidal categories for Nat and Nat-opJacques Comeaux
2025-10-15Replace proof with new stdlib propertyJacques Comeaux
2025-10-15Use new if-then-else propertyJacques Comeaux
2025-10-15Strengthen permutation sort theoremJacques Comeaux
2025-10-14Add local foldl for VectorsJacques Comeaux
2025-10-10Add Push and Pull functorsJacques Comeaux
2025-08-12Add preliminary setoid of discrete dynamical systemsJacques Comeaux
2025-08-12Add lattice of logical circuit valuesJacques Comeaux
2025-07-19Import missing pattern synonymJacques Comeaux
2025-07-19Show equivalence of old and new Hypergraph setoidsJacques Comeaux
2025-07-18Fix importsJacques Comeaux
2025-07-18Add Hypergraph setoidJacques Comeaux