aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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