Conal Elliott
Conal Elliott
Handy for things like `Int` addition
I'm going to abandon this one, but it may have some historical interest, especially for @sseefried.
I want to simplify circuits so they can only consume and produce bit vectors. High-level algorithms can still be designed in the category of functions and then related to circuits...
Can commutative diagrams (and thus comma categories) somehow capture *refinement*, in which the implementation is more specific than (and thus entails) the specification? If not, is there another category-theoretic notion...
Comma categories allow mixing different categories into a single package of specification, implementation, and correctness proof. For instance, - Functions can implement relations. - Matrices can implement functions. - Mealy...
Set up our project to generate highlighted and hyperlinked source code HTML and deploy on github.io in the manner of [agda-stdlib](https://agda.github.io/agda-stdlib/).
Define a parametrized cartesian category of vectors and vector functions, in which the objects are natural numbers denoting vectors (from `Data.Vec`) of the given length, with the element type given...
... using the helpers in `Categorical.Reasoning`. Doing so will speed up loading and hopefully be easier to read.
This PR adds left-pointing vectors `Vˡ` and renames `V` to “`Vʳ`”. It also changes `Examples.Add` to use `Vˡ` as mentioned in a comment there: > Note for a ⇨ᶜ b...
Given a homomorphism with lawful target, if equivalence of source morphisms is defined via the same homomorphism (`f ≈ g = Fₘ f ≈ Fₘ g`), then the source must...