The Coq mailing list

[roconnor AT theorem.ca]

On Fri, 4 Nov 2011, Adam Chlipala wrote:

> Victor Porton wrote:
> > On the contrary in the above mentioned ZF formalization for Coq can be used 
> > together with the rest Coq theories because a set is just a type.
>
> I don't think this is accurate.  CIC and ZF have been proved relatively 
> consistent, but this does not yield a practical way to mix the two in Coq 
> developments.

I am not aware of any interpretation of the axiom of replacement / axiom 
of collection in Coq without the use of additional axioms, specifically 
TTDA_3 (see 
<http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709>).

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''