The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Actually the quotients which I use ( setquot from hSet.v in 
https://github.com/vladimirias/Foundations ;) are quite well behaved.

"Subtyping" in the sense of using the notion of an inclusion also works quite 
well.

Vladimir.






On Nov 3, 2011, at 11:19 AM, Bruno Barras wrote:

> On 11/03/2011 01:57 PM, Adam Chlipala wrote:
>> I'd put it this way: when some development is said to be doable in ZF
>> but not CIC, I immediately doubt whether the development has practical
>> value. Not that there's anything wrong with impractical mathematics.... ;)
> 
> Well, it's hard to find something doable in ZF and not in CIC. At least, 
> you need to use replacement at its extreme power, which is probably not the 
> case of "practical mathematics".
> 
> The question is not being able to do something, but rather to do it with 
> limited pain. In the top 2 concepts that are easy in set theory and 
> "awkward" in (Coq's) type theory, I'd put subtyping and quotients.
> The latter being not always easy in ZF (without axiom of choice)...
> 
> Bruno.
> 
> -- 
> Bruno Barras                  Typical team - INRIA Saclay
> LIX - Ecole Polytechnique     91128 Palaiseau Cedex - France
> Tel: +33 1 69 33 40 57                Fax: +33 1 69 33 30 14