SetoidAlgebra with equivalence for tuples of elements of the algebra

[williamdemeo]

Would this be possible/a good thing to do?

If so, it would resolve the use of (weak) function extensionality (i.e., strong well-definedness) used in the proof of hom-unique.

[JacquesCarette]

If you mean that two SetoidAlgebra should be considered "the same" when their arities are pointwise the same, then I agree.

[williamdemeo]

Actually, no, that's not what I mean.

The issue is the following:

Suppose we have an operation of type Op A I, say, f : (I → A) → A.

Suppose u and v are (tuples of) arguments of f. So, u v are functions of type I → A.

Suppose we know u and v are point-wise equal (u ≈ v), that is, ∀ i → u i ≡ v i.

Then we should expect f u ≡ f v, too.

This is not function extensionality, which is why I named the axiom swelldef.

Indeed, we're not dealing with two different functions (say, f and g) here. Rather, we have a single function f and by claiming that, when u and v are point-wise equal, we have f u ≡ f v, we are merely requiring that the function f is well defined.

But one could argue that well definedness here should mean

u ≡ v → f u ≡ f v

and not

u ≈ v → f u ≡ f v

So, that's the issue I'm raising.

Now, how to address this satisfactorily with setoids (or otherwise)...?

[williamdemeo]

In the finite arity case I think we can all agree that well definedness of a function is the assertion that the function gives equal outputs when given two pointwise equal lists of arguments.

[JacquesCarette]

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 like this should be part of the definition of f itself. We wouldn't ever want to accept an "operation" that doesn't satisfy this, right? So it feels like it belongs with f, rather than being some kind of 'postulate' that holds uniformly at some universe level.

[williamdemeo]

Yes, perhaps this is something like cong.

I agree that in principle we wouldn't want to be dealing with operations that do not satisfy this. However, what are the ramifications of including this in our definition of operation? Do we forfeit some "computational content?" I need to understand this better... with examples.

I have some other points to make about this, but would rather move this part of the discussion to email.