Jacques Carette
Jacques Carette
I've thought about it some - and no, no better name, `Strict` seems good. The problem is that `Strict` is overloaded. For example, in category theory, it seems that "having...
That's a fair point. I guess `Strict` it is!
Question indirectly from this: does Agda allow **irrelevant** instance arguments to be filled by 'any' proof? Normally, instance search wants to find a single candidate for a hole.
Wikipedia uses `connex` for that particular relational property.
Can you expand on what you mean by "a middle ground" here?
So `pos-*` and `abs-*` ?
I agree that `g₁, g₂` would already be better. In some ways, the original `mor` suggestions might have been better? I'm glad for the suggestions, but I'm not feeling `witness`...
- don't use `let-in` because that's just syntactic sugar, and it will get expanded out / duplicated everywhere. It might be ok for `open` and giving short names meant for...
I wonder if there might be an opportunity for proving a theorem of the sort "if category X has property P, then sub-category Y of X (as witnesses by relation...