Title: Fixed point operators, inductive definitions and universes in Martin-Lof's type theory (on)