circuits - Tiny circuits DSL

Age	Commit message (Collapse)	Author
2 days	Show category of directed wiring diagrams is monoidal	Jacques Comeaux

13 days	Simplify wiring diagrams using semiadditive dagger	Jacques Comeaux

2026-07-18	Simplify semiadditive dagger definition	Jacques Comeaux

2026-07-18	Define semiadditive category	Jacques Comeaux

2026-07-17	Add categories with all binary biproducts	Jacques Comeaux

2026-07-13	Add split functor	Jacques Comeaux

2026-07-13	Remove use of deprecated name	Jacques Comeaux

2026-07-13	Add cartesian structure to category of semimodules	Jacques Comeaux

2026-07-13	Construct Sys functor from wiring diagrams to Cats	Jacques Comeaux

2026-07-12	Derive cartesian from semiadditive dagger	Jacques Comeaux

2026-07-12	Show category of commutative conoids is cartesian	Jacques Comeaux

2026-07-11	Add boolean lattice	Jacques Comeaux

2026-07-10	Use latest agda-categories	Jacques Comeaux

2026-07-09	Generalize systems to (co)commutative (co)monoids	Jacques Comeaux

2026-07-09	Add semimodules to commutative monoids functor	Jacques Comeaux

2026-07-09	Include missing properties	Jacques Comeaux

2026-07-09	Fix equivalence of rig homomorphisms	Jacques Comeaux

2026-07-09	Add category of commutative monoids	Jacques Comeaux

2026-07-09	Add Nat to category of maps of Mat(Bool) functor	Jacques Comeaux

2026-07-08	Add functional matrices	Jacques Comeaux

2026-07-07	Update circuit values	Jacques Comeaux

2026-07-07	Update circuit typechecker	Jacques Comeaux

2026-07-07	Update matrices and vectors	Jacques Comeaux

2026-04-30	Add monoids / monoid objects in setoids equivalence	Jacques Comeaux

2026-04-29	Simplify construction of matrix endofunctor	Jacques Comeaux

2026-04-29	Add endofunctor for matrices of fixed size	Jacques Comeaux

2026-04-28	Add endofunctor for Vectors of fixed length	Jacques Comeaux

2026-04-27	Add bounded distributive lattices	Jacques Comeaux

2026-04-03	Add free functor from rig-matrices to semimodules	Jacques Comeaux

2026-04-02	Add categories of Rigs, Bisemimodules, and Semimodules	Jacques Comeaux

2026-04-02	Reorganize matrix code	Jacques Comeaux

2026-03-29	Add semimodule of vectors over a commutative rig	Jacques Comeaux

2026-03-29	Add bisemimodule of vectors over a rig	Jacques Comeaux

2026-03-28	Begin separating vector concepts from matrices	Jacques Comeaux

2026-03-27	Build dagger 2-poset Mat(R) for idem. comm. rig R	Jacques Comeaux

2026-03-27	Add commutative rig matrix semiadditive structure	Jacques Comeaux

2026-03-27	Add dagger structure for commutative rig matrices	Jacques Comeaux

2026-03-26	Add cocartesian structure to category of matrices	Jacques Comeaux

2026-03-25	Use agda-categories definition of split idempotent	Jacques Comeaux

2026-03-25	Add looped wiring diagrams and merge functor	Jacques Comeaux

2026-03-25	Add pull functor from relations to wiring diagrams	Jacques Comeaux

2026-03-25	Add category of maps of a dagger 2-poset	Jacques Comeaux

2026-03-25	Define dagger-2-posets	Jacques Comeaux

2026-03-24	Add monoidal structure to category of posets	Jacques Comeaux

2026-03-24	Use new dagger reasoning combinator	Jacques Comeaux

2026-03-24	Add split idempotents	Jacques Comeaux

2026-03-19	Add category of matrices over an arbitary rig	Jacques Comeaux

2026-03-14	Add wiring diagram equalities	Jacques Comeaux

2026-03-14	Refactor wiring diagrams	Jacques Comeaux

2026-03-14	Add "idempotent" semiadditive dagger categories	Jacques 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.