The Coq mailing list

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

On 08/29/2012 03:54 PM, psperatto AT adinet.com.uy wrote:

Do you know if there is some paper or book that presents
the definition of the rec, rect, ind (the elimination
and equality rules) from the type former and
construction rules of an inductive set (type, prop)?
  

If I understand your question correctly, then this is the scholarly citation that I use (pulled from the author's web site):

@inproceedings{Moh93,
  author = {C. Paulin-Mohring},
  booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications},
  editor = {M. Bezem and J.-F. Groote},
  institution = {LIP-ENS Lyon},
  note = {LIP research report 92-49},
  number = 664,
  series = {Lecture Notes in Computer Science},
  title = {{Inductive Definitions in the System {Coq} - 
                              Rules and Properties}},
  type = {research report},
  year = 1993
}