aboutsummaryrefslogtreecommitdiff
path: root/Category/Dagger/Semiadditive.agda
AgeCommit message (Collapse)Author
2026-07-18Simplify semiadditive dagger definitionJacques Comeaux
2026-07-13Construct Sys functor from wiring diagrams to CatsJacques Comeaux
2026-07-12Derive cartesian from semiadditive daggerJacques Comeaux
2026-07-10Use latest agda-categoriesJacques Comeaux
2026-03-25Define dagger-2-posetsJacques Comeaux
2026-03-24Use new dagger reasoning combinatorJacques Comeaux
2026-03-14Add "idempotent" semiadditive dagger categoriesJacques Comeaux
Semiadditive dagger categories in which the induced commutative monoid on each hom-set is idempotent, or (equivalently), is a join semilattice. I don't know if there is a better name for this concept.
2026-03-12Add semiadditive dagger categoriesJacques Comeaux