Title: Constructing recursions operators in intuitionistic type theory
First published: 1984