Definition iter {D : dcpowithbottom} (n : nat) (f : D --> D) : D. Proof. induction n as [ | m IH]. - exact (dcpowithbottom_bottom D). - apply f. exact IH. Defined.
Require Import UniMath.Foundations.All.