The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  Is there a formalization of CiC in Coq?

  I recently stumbled across http://www.lix.polytechnique.fr/~barras/coq_work-eng.html which appears to only formalize CC in Coq.

  I'm wondering if there is something that defines CiC in Coq. (I feel like reading such definitions in Coq would actually deeper my understanding.)

Thanks!