The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Sun, 6 Nov 2011 05:12:33 +0000, David Leduc 
<david.leduc6 AT googlemail.com>
 wrote:
> Thank you for your replies.
> 
> My main motivation for this question is to define equality on
> functions between presets (i.e., a set without equality. See
> http://nlab.mathforge.org/nlab/show/preset.)
> 
> So the idea of eqfun was to define an equality relation on function
> types without relying on an equality on non-functional types. But
> functional extensionality relies on the equality on the domain of the
> function.

eq is leibniz equality, which is, essentially syntactic equality. I
think it is reasonable to treat 'Type's with Leibniz equality as
presets. In particular, one doesn't have quotients or subobjects of
(non-Sort) types. One can then impose equivalence relations to get
setoids, which behave essentially likes sets, with subobjects and
quotients.

  Tom