circuits - Tiny circuits DSL

Age	Commit message (Collapse)	Author
8 days	Remove use of deprecated name	Jacques Comeaux

8 days	Add cartesian structure to category of semimodules	Jacques Comeaux

8 days	Construct Sys functor from wiring diagrams to Cats	Jacques Comeaux

9 days	Derive cartesian from semiadditive dagger	Jacques Comeaux

9 days	Show category of commutative conoids is cartesian	Jacques Comeaux

11 days	Add boolean lattice	Jacques Comeaux

11 days	Use latest agda-categories	Jacques Comeaux

12 days	Generalize systems to (co)commutative (co)monoids	Jacques Comeaux

12 days	Add semimodules to commutative monoids functor	Jacques Comeaux

12 days	Include missing properties	Jacques Comeaux

12 days	Fix equivalence of rig homomorphisms	Jacques Comeaux

12 days	Add category of commutative monoids	Jacques Comeaux

13 days	Add Nat to category of maps of Mat(Bool) functor	Jacques Comeaux

13 days	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.
2026-03-14	Allow square brackets in circuit lang identifiers	Jacques Comeaux

2026-03-14	Refactor systems and add looped systems	Jacques Comeaux

2026-03-12	Add semiadditive dagger categories	Jacques Comeaux

2026-03-10	Add preliminary category of wiring diagrams	Jacques Comeaux

2026-03-08	Add monoidal category of finite relations	Jacques Comeaux

2026-01-13	Fix modules broken by addition of strong SymMonCat	Jacques Comeaux