Definition iterate_on_pt_scott_continuous_map {X : dcpo} (n : ℕ) : scott_continuous_map (X × dcpo_funspace X X) X. Proof. induction n as [ | n IHn ]. - exact π₁. - exact (comp_scott_continuous_map ⟨ eval_scott_continuous_map X X , π₂ ⟩ IHn). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Examples.Fixpoints. Require Import UniMath.OrderTheory.DCPOs.Examples.Exponentials. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.