Age | Commit message (Collapse) | Author | |
---|---|---|---|
2024-08-24 | Generalize coequalizer result to arbitrary category | Jacques Comeaux | |
2024-06-14 | Finish category of cospans | Jacques 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-11 | Finish -left and -right lemmas for associativity | Jacques Comeaux | |
2024-06-11 | Begin defining category of cospans | Jacques Comeaux | |
2024-04-25 | Define coequalizers and pushouts in Nat | Jacques Comeaux | |
2024-04-24 | Add base case coequalizers in Nat | Jacques Comeaux | |
2024-04-24 | Add more merge and unmerge properties | Jacques Comeaux | |
2024-04-23 | Add merge and unmerge properties | Jacques Comeaux | |
2024-03-18 | Remove with-abstractions | Jacques Comeaux | |
2024-03-09 | Factor out comparison | Jacques Comeaux | |
2024-02-28 | Add coequalizer theorem | Jacques Comeaux | |
2024-02-22 | Fill in omitted proof | Jacques Comeaux | |
2024-02-21 | Create LICENSE | Jacques Comeaux | |
2024-02-21 | Begin correctness proof for glue-iter | Jacques Comeaux | |
2024-02-21 | Add iterative version of glue | Jacques Comeaux | |
2024-02-20 | Prove merge lemmas | Jacques Comeaux | |
2024-02-20 | Simplify merge function | Jacques Comeaux | |
2024-02-19 | Add glue function for finite sets | Jacques Comeaux | |
2024-02-16 | Add helper function for merging finite sets | Jacques Comeaux | |
2022-10-16 | Initial commit | Jacques Comeaux | |