A Type-Free Theory of Half-Monotone Inductive Definitions

e Theory (Preliminary Report)", LNCS 613 (Springer, 1991) pp. 33-45.19. P. Dybjer, "Universes and a general notion of simultaneous inductive-recursive definitionin type theory", Proc. of the 1992 Workshop on Types for Proofs and Programs,Baastad, eds. B. Nordstrom et al. (1992).20. P. Dybjer, "A general notion of simultaneous inductive-recursive definitionin type theory", Draft paper (available by ftp from cs.chalmers.se at/pub/clics/peterd/Inductive Recursive.dvi.Z) (1993).21. M....