Edwin Brady, Conor McBride, James McKinna. Inductive Families Need Not Store Their Indices. In Stefano Berardi, Mario Coppo, Ferruccio Damiani, editors, Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. Volume 3085 of Lecture Notes in Computer Science, pages 115-129, Springer, 2003. [doi]
Abstract is missing.