aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
39 hoursFix importsJacques Comeaux
39 hoursAdd Hypergraph setoidJacques Comeaux
39 hoursSorted lists with the same elements are equalJacques Comeaux
41 hoursConvert between List and Vector permutationsJacques Comeaux
11 daysFix broken importJacques Comeaux
11 daysAllow arity-0 hyperedges in functional hypergraphsJacques Comeaux
11 daysSplit hypergraph label and edge into separate filesJacques Comeaux
2025-07-03Add S-Expression parser and circuit typecheckerJacques Comeaux
2025-07-03Finish strict total order for hypergraph edgesJacques Comeaux
2025-07-01Begin strict total order for hypergraph edgesJacques Comeaux
2025-06-19Add new hypergraph definitionsJacques Comeaux
2025-05-19Add racket language for labeled hypergraphsmainJacques 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
2024-02-16Add helper function for merging finite setsJacques Comeaux
2022-10-16Initial commitJacques Comeaux
generated by cgit v1.2.3 (git 2.39.1) at 2025-07-20 13:43:57 +0000