Conal Elliott

I'd like an additional level of customization: set Pandoc options via Gitit page metadata entries. Would override the config settings, which would override the defaults.

Thanks for opening this PR! I see that you’ve introduced an inverse homomorphism, going from *Function* to *C*. I don’t think that inverse homomorphism exists in general. I did pretend...

Here’s some more context, from yesterday’s chat on Discord. Here is how I now think about compiling-to-categories (CtoC) from a correctness perspective. We have a *function* `g`, conveniently expressed in...

> What should the result be in here: https://github.com/conal/denotational-hardware/pull/45/files#diff-79cd0018bfc7213df4b4d8f20fbba17f13d68f7cd8768e998002751efa6587f2R65 ? I don't know how to translate this example either, since we don't have categorical vocabulary to cover it. In this...

Switching from `Vec` to `V` may allow generalizing the `Vector` and `VRouting` families from functions to *any* monoidal category.

> When working on #21 I figured that having `CoCartesian` Categories, hence coproducts and even `BiCartesian` Categories formalized it would be more elegant to express some of the fields and...

> Are laws like: `∨-swap : ∨ ∘ swap ≈ ∨` (commutativity of or, etc) needed? should this be bundled in something like semi-ring? Maybe `BooleanAlgebra` from [`Algebra.Bundles`](https://agda.github.io/agda-stdlib/Algebra.Bundles.html).

I think this task will be fairly simple while raising some interesting nuances about products and homomorphisms.

See `Categorical.Comma.Raw` for examples.

> Is it maybe a naming issue? what if you chose maybe name for the pattern? I'm afraid I don't understand the queston/suggestion.