Jacques Carette
Jacques Carette
I've got a detailed review incoming. Agree with thoughts 0-4.
> At the risk of being a dissenting opinion, is this something that might be better as a standalone library? I certainly agree that the bar for introducing logics into...
AFAIK you are correct: we've never programmed that one. That's as good a place as any for the proof. Putting the various 'pieces' in their right place may also need...
I was partly hoping you'd complete the (co)end calculus facilities so as to use the 'elegant' proof... but that is perhaps wishful thinking! [I had started doing all the prerequisites,...
> To make (co)end calculus usable, you really need a DSL for writing "functorial forms", EG: the stuff that happens underneath the integral. If you don't have this, then things...
Minor: I personally prefer to put the `begin` on the line above, to use less horizontal space. But that's pure style. As to the syntax, an alternate suggestion would be...
Non-commutative polynomial rings certainly do make sense and are useful. See for examples the [skew polynomials](https://en.wikipedia.org/wiki/Ore_extension) that arise when modeling various kinds of operators. Axiom does allow polynomials over coefficients...
We're looking into the automated tests.
@MatthewDaggitt I can confirm that I can reproduce @benmandrew 's problem. I have Agda 2.6.4.3 and agda-stdlib-2.0 (on top of GHC .6.7 and cabal 3.12.1.0). The symptom that I get...