The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

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