Jacques Carette comments

Results 1199 comments of


                                            Jacques Carette

[ refactor ] Restate, and use, the definitions of `Monotonic` etc. operations

Thanks - these already are easier to understand.

[ refactor ] Restate, and use, the definitions of `Monotonic` etc. operations

Just needs a second reviewer.

[ definition ] characteristic of a `Ring` (etc.)

I would think that the characteristic of a `Ring` is a very property-like thing that shouldn't go right in the definition. There is way too much 'kit' that comes with...

[ definition ] characteristic of a `Ring` (etc.)

Interesting. Seems like it is better constructively. I agree that understanding if this is a better definition would require trying it out. What I was *actually* curious about is `agda-unimath`'s...

[Add] Initial files for Domain theory - Continuation of #2721

I'm going to try to have an in-person discussion (with @TOTBWF and @gabriellisboaconegero ) early next week to try to hash things out. The main thing to discuss will be...

[Add] Properties for DCPOs in `Relation.Binary.Properties.Domain`

Could we get another review? @jamesmckinna ? @MatthewDaggitt ?

[Add] Properties for DCPOs in `Relation.Binary.Properties.Domain`

I've asked @e-mniang to take over this PR.

Functional Relation

The 'design space' of partial algebraic structures in the type theory that `agda-stdlib` chooses to use is... non-trivial. I'll summon @TOTBWF as he's been forced to think about this quite...

Functional Relation

Oh, absolutely, that perspective is all those things (simple, powerful and under explored in stdlib). I think the issue at the top makes sense to deal with. My only comment...

[ draft ] Alternative design for sub- and quotient- `(Abelian)Group`s

I'm sure this alternative design makes a lot of sense to you @jamesmckinna and to @Taneb , but since I don't have the original in mind, your description relative to...