Circuit category

References

• Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits

class Circuit.CircuitCategory (V : outParam (Type u_1)) [Preorder V] (G : outParam (Type u_2)) [Gate V G] (C : Type u) [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_3, u} C] : Type (max u_2 u_3)

A category of circuits.

• gate (g : G) : OfNat.ofNat (Gate.inputs g) ⟶ OfNat.ofNat (Gate.outputs g)

  Morphism to introduce a gate.

• stub : OfNat.ofNat 0 ⟶ 1

  Morphism to introduce a wire.

• drop : OfNat.ofNat 1 ⟶ 0

  Morphism to eliminate a wire.

• fork : OfNat.ofNat 1 ⟶ 2

  Morphism to fork a wire.

• join : OfNat.ofNat 2 ⟶ 1

  Morphism to join two wires.