P.J.: Inductive types in constructive languages

Logic grammar is used to partly define a formal mathematical language “ADAM”, that keeps close to informal mathematics and yet is reducible to a foundation of Constructive Type Theory (or Generalized Typed Lambda Calculus). This language is employed in making a study of inductive types and related subjects, as they appear in languages for constructive mathematics and lambda calculi. The naturality property of objects with type parameters is described and employed. Cover diagram Behold the mathematical universe, developing from original unity into categorical duality. The central beam contains the initial and the final type, together with the remaining flat finite types. It is flanked by the dual principles of generalized sum and product, and of initial and final fixed point construction