The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 12/26/2012 11:18 AM, Daniel Schepler wrote:
> I'd say that using Coq types as the base for the theory would almost
> always be the way to go, unless somehow your theory is intricately
> tied to ZFC concepts (which should be extremely rare outside model
> theory).  The main advantage of ZFC is a small set of syntax and
> axioms (mostly useful for model theory), while the big disadvantage is
> that it's a fairly artificial model in which to do real mathematics.
> Coq's type theory is a much closer match to how most mathematicians
> think of things on a daily basis, but at the cost of a somewhat more
> complex kernel and metatheory.
>    

Is it true that CIC has more complex metatheory, when we properly 
consider first-order logic as part of the definition of ZFC?