Jacques Carette
Jacques Carette
Hmm, I'm not quite sure where I should discuss this. Also "any setoid-based reasoning depends on specific implementation details" is not something I believe is true! I'm not going to...
I keep forgetting your main education is all math, so some oft-used CS lingo (like Ack as a short-form for aknowledged, which comes from low-level network protocols) is mysterious. I...
If you mean that two `SetoidAlgebra` should be considered "the same" when their arities are pointwise the same, then I agree.
Finally coming back to this - thanks for the clarification. You are definitely correct that this is not extensionality! If we have setoids, isn't this essentially `cong` ? It feels...
Let me try to address all of the items in turn. Using an abstract interface would not let us escape `funext` on its own, unfortunately. The abstract interface would need...
I'm not sure, as of yet, what there is to 'discuss'. I was expecting you @J1aM1ng to put together some material (where #3717 is merely the data-gathering stage), analyze "where...
Those are really good comments @samm82 . Any suggested redesign should be able to provide 'answers' to these points.
As far as I can see, conjecture ` ⟦_⟧₁ : {X Y : U} → X ⟷₁ Y → ⟦ X ⟧₀ == ⟦ Y ⟧₀`, i.e. line 28-29 of...
To @inexxt : yes, I agree that it is not straightforward to integrate those functions, they are most easily 'ported' rather than reused, sadly. And `c2equiv` is not an equivalence,...
The reason I brought this up as an issue here and didn't really comment on the PR is that I agreed that for v2.2, what was done was best. This...