aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
3 daysAdd inverted unitary rules for strong monoidal functorsJacques Comeaux
4 daysAdd inverted associativity for strong monoidal functorsJacques Comeaux
8 daysSimplify System definition and add System functorJacques Comeaux
8 daysSetoid-ify System definitionJacques Comeaux
8 daysAdd symmetric monoidal structure to Push functorJacques Comeaux
14 daysAdd 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-15Use new if-then-else propertyJacques 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-05-19Add racket language for labeled hypergraphsJacques Comeaux
2025-05-01Update trivial decoration functorJacques Comeaux
2025-05-01Update graph decoration functorJacques Comeaux
2025-05-01Add labeled hypergraph decoration functorJacques Comeaux
2025-04-29Add hypergraph decoration functorJacques Comeaux
2025-04-23Category of decorated cospans is symmetric monoidalJacques Comeaux
2025-02-08Define tensor product of decorated cospansJacques Comeaux
2025-02-08Add symmetric braiding to category of cospansJacques Comeaux
2025-02-03Show category of cospans is monoidalJacques Comeaux
2025-02-03Add category of finitely-cocomplete categoriesJacques Comeaux
- Objects are categories with all finite colimits - Morphisms are functors preserving finite colimits (i.e. right exact)
2025-02-03Update agda-categories versionJacques Comeaux
2024-11-18Improve namingJacques Comeaux
2024-11-05Add trivial and graph decoration functorsJacques Comeaux
2024-10-16Switch decoration functor from strong to laxJacques Comeaux
2024-10-01Finish category of decorated cospansJacques Comeaux
2024-09-29Prove associativity for decorated cospan compositionJacques Comeaux
2024-09-22Add composition and equality of decorated cospansJacques Comeaux
2024-09-19Add decorated cospansJacques Comeaux
2024-08-24Generalize coequalizer result to arbitrary categoryJacques Comeaux
2024-06-14Finish category of cospansJacques Comeaux
For a category C with all pushouts, Cospans(C) is a category with the same objects as C and with a morphism f : X -> Y for each cospan X -> Z <- Y in C.
2024-06-11Finish -left and -right lemmas for associativityJacques Comeaux
2024-06-11Begin defining category of cospansJacques Comeaux
2024-04-25Define coequalizers and pushouts in NatJacques Comeaux
2024-04-24Add base case coequalizers in NatJacques Comeaux
2024-04-24Add more merge and unmerge propertiesJacques Comeaux
2024-04-23Add merge and unmerge propertiesJacques Comeaux
2024-03-18Remove with-abstractionsJacques Comeaux
2024-03-09Factor out comparisonJacques Comeaux
2024-02-28Add coequalizer theoremJacques Comeaux
2024-02-22Fill in omitted proofJacques Comeaux
2024-02-21Create LICENSEJacques Comeaux
2024-02-21Begin correctness proof for glue-iterJacques Comeaux
2024-02-21Add iterative version of glueJacques Comeaux
2024-02-20Prove merge lemmasJacques Comeaux
2024-02-20Simplify merge functionJacques Comeaux
2024-02-19Add glue function for finite setsJacques Comeaux
generated by cgit v1.2.3 (git 2.39.1) at 2025-10-30 15:32:52 +0000